New software security vulnerabilities are discovered on an almost daily basis. Any support to aid secure software development is thus dearly needed. With respect to crypto-based software (such as crypto-protocols), a lot of successful research has been done to analyze abstract specifications against high-level security requirements (such as confidentiality and authenticity). Also, there is much research in program security analysis on verifying secure information flow properties or on detecting low-level weaknesses such as buffer overflows. However, there is so far no approach which analyzes implementations using cryptography against high-level security requirements. It is, however, important to verify both the specifications and the source code of such a system: the specifications, to remove potential security flaws when this is still less costly, and the source code, because additional weaknesses may be introduced when writing the code. The main aims of the project are thus - to develop a formal security verification methodology to verify implementations of cryptographic protocols against high-level security requirements and - to apply the methodology to the implementation of a widely used security protocol (such as the Internet security protocol standard SSL). Both these aims have not yet been attained by the research community. Given the current state of research in formal security verification, the missing link in achieving the aims is finding a practical yet soundly based way to establish correspondence between a software design and its implementation which enforces that security requirements verified at the design level are actually satisfied by the implementation. Given a textual specification of crypto-based software and its implementation, one constructs a precise, compact representation of the specification using the formally founded security extension UMLsec of the Unified Modeling Language (UML) developed by the PI in earlier work (see the PI's list of publications). This model is verified against the security goals using automated theorem provers for first order logic (see the ICSE 2005 paper). The project goal is to ensure that the implementation correctly implements the specification by making use of techniques such as run-time verification, security testing, and local formal verification of the source code (a first step can be found in the ASE 2006 paper).
The following further participants will contribute to the project: Prof. Bashar Nuseibeh (OU) and Charles Haley (OU), both on security requirements, Dr. Yijun Yu (OU) on reverse engineering specifications from code, Dr. Martin Leucker (TUM) on runtime verification, Daniel Ratiu (TUM) on program understanding, and Jorge Fox (TUM) on aspect-oriented security.
The security protocol to be verified, and the tools needed to verify it, as well as the results, are all open-source and free to use by the public, which creates a benefit not only to fellow researchers but also the end-user (the SSL protocol is a protocol widely used in end-user web-browsers to secure web-content transmission). Also, British software industry challenged by globalization will benefit from innovative yet applicable research in the security domain which is inherently non-off-shorable.
The results of the project will include:
Benefits to individuals and institutions:
Tools for Traceable Security VerificationThe Open University will be able to enlarge and deepen its international cooperations. Beyond the collaboration with the host TU Munich, this may include relevant industry in Munich, including Siemens and BMW, also through existing cooperations of TU Munich. This may build the foundation for a joint project within the EU Framework 7 program. The PI would profit since the very challenging project could not be performed without building on and extending previous collaboration with TU Munich.
Benefits to United Kingdom:
Benefits to the overseas country:
A study by the German Federal Office for IT Security (BSI) in 2003 showed that due to the increasing complexity of software, there is a need in the software industry for sound methods and tools to construct security-critical software in a reliable way. Since this is a very challenging goal which cannot be achieved by one research team in isolation, an international cooperation would be very beneficial to both sides in order to jointly reach a solution.
Prof.Dr.Bashar Nuseibeh, Director of Research in Computing (OU), Visiting Professor at Imperial College London. Contribution: Security requirements elicitation for the given security protocol. Relevant Publications:
Dr.Yijun Yu, Senior Lecturer (OU). Contribution: Reverse engineering specification from the protocol source code. Relevant Publications:
Charles Haley, Lecturer (OU). Contribution: Security requirements elicitation for the security protocol. Relevant Publications:
Dr.Martin Leucker, Senior Researcher (TUM). Contribution: Run-time verification of the security protocol. Relevant Publications:
Jorge Fox, Researcher (TUM). Contribution: Aspect-oriented formalization of security requirements on the protocol. Relevant Publications:
Jorge Fox works on aspect-oriented modeling of secure software. His involvement in the project will continue an existing collaboration with the PI on applying his work to security analysis of cryptographic protocols and thereby contribute directly to both his PhD studies and the project results.
Daniel Ratiu, Researcher (TUM). Contribution: Program understanding of the protocol source code. Relevant Publications:
Daniel Ratiu works on program understanding, with applications to security. His involvement in the project will continue an existing collaboration with the PI on applying his work to security analysis of cryptographic protocols and thereby contribute directly to both his PhD studies and the project results.