Automated Verification of Security-Critical Software (VeriSec)
Computing Department, The Open University, UK
in cooperation with Andrew D. Gordon,
Research (MSR) Cambridge (Research Group on Programming
Principles and Tools).
Tools to automatically verify abstract, formal specifications of cryptographic protocols against high-level security
requirements (like confidentiality, privacy, authenticity) are a major scientific success in computer security.
However, this has so far not led to a successful technology transfer to practice: Currently no approach analyses
existing implementations (such as the Internet security protocol standards openSSL and openSSH) against such
requirements, despite recent advances on self-implemented code (cf. background references below). In particular, there
are no tools shown 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 current project aims to
address these challenges.
Some relevant background literature
- J. Jürjens and M. Yampolskiy. Code Security Analysis with Assertions. 20th International Conference on
Automated Software Engineering (ASE 2005), IEEE/ACM, 2005, pp. 392-395. (paper, bibtex)
- J. Goubault-Larrecq, F. Parrennes: Cryptographic Protocol Analysis on Real C Code. Conf. on Verification,
Model-Checking and Abstract Interpretation (VMCAI) 2005, p. 363-379
- J. Jürjens. Code Security Analysis of a Biometric Authentication System Using Automated Theorem Provers.
In 21st Annual Computer Security Applications Conference (ACSAC 2005) IEEE, 2005, pp. 138-149. (paper, slides, bibtex)
- J. Jürjens. Understanding Security Goals Provided by Crypto-Protocol Implementations. 21st International
Conference on Software Maintenance (ICSM 2005), IEEE, 2005, pp. 643-646. (paper, slides, bibtex)
- J. Jürjens. Verification of Low-level Crypto-Protocol Implementations Using Automated Theorem Proving.
Third International Conference on Formal Methods and Models for Codesign (MEMOCODE 2005) ACM/IEEE, 2005, pp. 89-98.
(paper, slides, bibtex)
- J. Jürjens. Security Analysis of Crypto-based Java Programs using Automated Theorem Provers. 21st
International Conference on Automated Software Engineering (ASE 2006), IEEE/ACM, 2006, pages 167-176. (paper, slides, bibtex)
- K. Bhargavan, C. Fournet, A.D. Gordon, Stephen Tse: Verified Interoperable Implementations of Security
Protocols. IEEE Computer Security Foundations Workshop (CSFW) 2006 (p. 139-152)
- K. Bhargavan, C. Fournet, A.D. Gordon: Verified Reference Implementations of WS-Security Protocols. 3rd
Int. Works. on Web Services and Formal Methods (WS-FM) 2006, LNCS 4184, Springer 2006
- A.D. Gordon: Provable Implementations of Security Protocols. Invited talk at IEEE Symposium on Logic in
Computer Science (LICS) 2006, p. 345-346
- Jan Jürjens: Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie
Project. Seventh International Workshop on Automated Verification of Critical Systems (AVOCS 2007), Oxford, Sep.
10-12, 2007. (paper, slides)
- J. Jürjens, Yijun Yu, and A. Bauer: Tools for Traceable Security Verification. BCS Visions of Computer
Science Conference, 2008. (paper, slides)
- Jan Jürjens, A Domain-Specific Language for Cryptographic Protocols based on Streams. To appear, Journal
of Logic and Algebraic Programming, Sep./Oct. 2008, ca. 37 pp. (paper)