This Project's

Research Team

Co-ordinators

External Collaborators

  • Andrew Gordon

Automated Verification of Security-Critical Software (VeriSec)

Theme: Security and Privacy
Funding Agency: Royal Society
Period: 01/10/08 - 30/09/11
Jan Jurjens of the OU Department of Computing has been granted a 4 year half-time Industrial Fellowship by the Royal Society to work at Microsoft Research Cambridge on the project Automated Verification of Security-Critical Software (VeriSec), in cooperation with Andrew D. Gordon (MSRC). The overall objective of Jan's research is a soundly based approach to Secure Software Engineering. More specifically, one main current focus is the automated, formally-based analysis of software artefacts against security requirements. This is motivated by the observation that the current state of security engineering in practice is far from satisfactory. The goal is thus to start with the actual industrial engineering methods of security-critical software-based systems, to identify problems which are practically amenable to tool-supported, formally sound analysis methods, and to try to solve these problems using these methods. An important objective is to ensure that these analysis methods can actually be used in practice by keeping the additional overhead in using them bounded: First, they take as input artefacts which are already available in current industrial software development (such as UML models and program source code) and do not have to be constructed just to perform the analysis. Second, the tools should be reasonably easy to use and have a strong emphasis on automation. The VeriSec project will address the challenges of developing tools to analyse pre-existing protocol implementations in C against high-level security requirements, though tools to check lower level properties like memory safety do exist. Inventing tools to verify high-level properties of the code - as opposed to abstract specifications - of security protocols is important: The implementation code is often the first and only place where the full details of a protocol are formalized, and even if there is a detailed formal specification, the implementation may introduce additional vulnerabilities. The work undertaken during the fellowship will build upon the ongoing relationship with Microsoft Research Cambridge where Dr. Jurjens already co-supervises two students working on Verifying Implementations of Security Protocols in C with Andrew Gordon of Microsoft Research.