Secondary Content

Contact Person

Modelbased Formal Security Analysis of Crypto-Protocol Implementations

General purpose

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.

Scientific aims

  • The results of the project will include:

    • a formal security verification methodology which verifies implementations of cryptographic protocols against high-level security requirements and
    • the results from applying this methodology to the implementation of a widely used security protocol.
  • 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:

    • Today's software insecurity is a problem e.g. for the finance industry and the defense sector which are important to British industry.
    • Given the challenge of globalization, IT security is a promising domain for British software developers since security-critical software development is less likely to be off-shored.
    • For the security domain, the project also contributes to British research efforts targeting the Grand Challenge of developing a verifying compiler identified by EPSRC.
  • 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.

Other project participants

  • 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:

    • R.Crook, D.C.Ince, B.Nuseibeh: On Modelling Access Policies: Relating Roles to their Organisational Context. RE'05
    • L.Lin, B.Nuseibeh, D.C.Ince, M.Jackson: Using Abuse Frames to Bound the Scope of Security Problems. RE'04
    • B. Nuseibeh, Weaving Together Requirements and Architecture , IEEE Computer, 34(3):115-117, March 2001.
  • Dr.Yijun Yu, Senior Lecturer (OU). Contribution: Reverse engineering specification from the protocol source code. Relevant Publications:

    • Y.Yu, Y.Wang, J.Mylopoulos, S.Liaskos, A.Lapouchnian, J.C.S.P.Leite. Reverse engineering goal models from legacy code. RE'05
    • Y.Yu, J.Mylopoulos, Y.Wang, S.Liaskos, A.Lapouchnian, Y.Zou, M.Liiou, J.C.S.P.Leite. RETR: Reverse Engineering to Requirements. WCRE'05
    • Y.Yu, J.C.S.P.Leite, J.Mylopoulos. From Goals to Aspects: Discovering Aspects from Requirements Goal Models. RE'04
  • Charles Haley, Lecturer (OU). Contribution: Security requirements elicitation for the security protocol. Relevant Publications:

    • C.B.Haley, R.C.Laney, J.D.Moffett, B.Nuseibeh. Using Trust Assumptions with Security Requirements, Requirements Engineering Journal, 11, 2, 2006.
    • C.B.Haley, R.C.Laney, J.D.Moffett, B.Nuseibeh: The Effect of Trust Assumptions on the Elaboration of Security Requirements. RE'04
    • C.B.Haley, R.C.Laney, B.Nuseibeh. Deriving Security Requirements from Crosscutting Threat Descriptions, AOSD'04
  • Dr.Martin Leucker, Senior Researcher (TUM). Contribution: Run-time verification of the security protocol. Relevant Publications:

    • O.Grumberg, M.Lange, M.Leucker, S.Shoham: When Not Losing is Better than Winning: Abstraction and Refinement for the Full mu-Calculus. Accepted for Information and Computation
    • A.Bauer, M.Leucker, C.Schallhart: Model-based runtime analysis of distributed reactive systems. ASWEC'06
    • T.Berg, O.Grinchtein, B.Jonsson, M.Leucker, H.Raffelt, B.Steffen: On the Correspondence Between Conformance Testing and Regular Inference. FASE'05
  • Jorge Fox, Researcher (TUM). Contribution: Aspect-oriented formalization of security requirements on the protocol. Relevant Publications:

    • H.Mouratidis, J.Jurjens, J.Fox, Towards a Comprehensive Framework for Secure Systems Development, CAiSE'06
    • J.Fox, J.Jurjens, Introducing Security Aspects with Model Transformation, ECBS'05

    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:

    • D.Ratiu, F.Deissenboeck, How Programs Represent Reality (and how they don't), WCRE'06
    • D.Ratiu, F.Deissenboeck, Programs are Knowledge Bases, ICPC'06

    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.