Secondary Content

Contact Person

Automated Verification of Security-Critical Software (VeriSec)

Royal Society Industrial Fellowship with MS Research (50% part-time, 1.10.08-30.09.2012)

Computing Department, The Open University, UK
in cooperation with Andrew D. Gordon, Microsoft Research (MSR) Cambridge (Research Group on Programming Principles and Tools).



Project Description

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.



Related projects



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)