Finding meaning in cryptographic verification: Methods in the verification of post-quantum cryptography

The research explores different approaches to the problem of functionally verifying complex cryptographic software, and the wider role that formal methods has in creating strong assurance cases for novel cryptography such as post-quantum public-key cryptography. We seek to answer the question of what methodology and approach is likely to result in the most meaningful and useful results in this context, and how meaning can be extracted from the resulting artifacts in a rigorous manner. Much of the work has been based on the technical work of performing such verifications, as well as a review of the literatures in both cryptographic and verification contexts. The focus has been on Classic McEliece, one of the schemes under active consideration by NIST since 2016 under its ongoing post-quantum standardization process.

People. The most obvious impact of RHUL's cyber security CDT will be its production of 50 PhD-level graduates during its lifetime. CDT graduates will be "industry-ready": through industry placements, they will have exposure to real-world cyber security problems and working environments; because of the breadth of our training programme, they will gain exposure to cyber security in all its forms; through involvement of our external partners at all stages of the CDT, the students will be exposed to the language and culture of industry, government and other sectors. At the same time, they will benefit from generic skills training, equipping them with a broad set of skills that will be of use in their subsequent workplaces. They will also engage in PhD-level research projects that will lead to them developing deep topic-specific knowledge as well as general analytical skills. There is a growing demand for graduates with these skill-sets. While RHUL already has demonstrably close relationships with key external players, our CDT represents an opportunity for us to enhance our existing links and develop new ones. Moreover, our own research will be strengthened by working with the best external researchers.

Economy. The nature of our cyber security research and the planned industrial involvement in influencing the selection of research topics means that there will be significant commercialisation opportunities arising from the research produced by this CDT. RHUL cyber security researchers have more than 80 years of experience working in industry, either in research, development or customer-facing environments, and are named inventors on more than 30 patents. We are closely supported by the Royal Holloway Enterprise Centre, who have expertise in business development, securing venture capital funding, and IPR protection. RHUL's Institute for Cyber Security Innovation provides business research and training support. We also have an on-campus incubation centre which has hosted a number of spin-out companies. We are thus thoroughly prepared to identify and exploit commercialisation opportunities arising from the CDT.

Knowledge. The CDT will make substantial and original contributions to knowledge in cyber security. Following institutional policy, all research is made available to the public for free in some form, either through open access publishing,the institution's research repository or via subject-specific on-line archives. The research will also published in conference venues which, by their nature, are regularly attended by large numbers of delegates from outside of academia. Other impact routes for our knowledge include Industry Fora (RHUL is an active academic member of the I4 and ISF organisations, which are influential industry fora), Business Events (RHUL researchers regularly speak at events such as InfoSec London, RSA Conference), Standards Bodies (several staff are active in international standards bodies), Consulting (staff have consulted for more than 100 organisations in the last 30 years), Industry-focused Events (RHUL hosts several external facing events each year, including the annual CDT Showcase, HP Colloquium, and ISG Open Day).

Society. One of the longer-term impacts of our research is to provide mechanisms that help to enhance confidence and trust in the on-line society for ordinary citizens, leading in turn to quality of life enhancement. Our work on the socio-technical dimensions of security and privacy gives us a means to influence government policy to the betterment of society at large. We work closely with government departments such as the Cabinet Office to provide advice on privacy, security and design issues. We also communicate research findings through more widely accessible media, press engagement, speaking at public events, and working with schools (CDT students will take part in the annual Smallpeice Trust Cyber Security residential for Year 9 students).