Automated Analysis of Security Critical Systems

Project Description

This project investigated the application of formal tools to the problem of analysing the APIs of the hardware security modules used in electronic payment systems (i.e. cash machine networks, point of sale devices, etc.).

The project ran from 1st October 2004 to 30th September 2007. You can read a summary of the whole project in the Final Report, submitted to EPSRC in December 2007. The project was rated Outstanding by EPSRC's review panel, and given the top rating in all 7 categories. You can read the EPSRC assessment here.

Results

• The project included some research into finding ways to reason effectively about key-management APIs that use bitwise XOR, like the IBM 4758 CCA API.
  • Early results on rediscovering known attacks in a formal model were presented at CADE-20 in Tallinn. This involved extending the superposition calculus with XOR unification constraints.
  • We proved some theoretical results about the decidability of XOR-based key-management schemes, in collaboration with Véronique Cortier. This work was presented at the FCS-ARSPA workshop in August 2006.
  • We devised an efficient way to implement the decision procedure arising from these results, and obtained some verification results for the revised versions of the IBM CCA API. Details appeared at TACAS 2007.
  • We proposed a formalisation for "Key Conjuring", the process by which the attacker obtains a valid but unknown key for an API. This was published at CSF 2007 in Venice.

• We developed a formal model for PIN-guessing attacks with information leakage, employing the PRISM probabilistic model checker to optimise attacks. Many APIs are vulnerable to these kinds of attacks.
  • An informal introduction to this work appears as a case study on the PRISM webpage.
  • A more formal account appears in the journal Theoretical Computer Science, Vol 367 Nos 1-2 (see below).
  • You can also visit the homepage of the software used to build the PRISM models, AnaBlock.

Collaborators

Our industrial collaborators on the project were nCipher plc., a manufacturer of cryptographic hardware security modules, and CESG, the information assurance arm of GCHQ.

Funding

The project was funded by EPSRC (grant number GR/S98139/01).

People

The project was designed and proposed by Graham Steel, who was the principal R.A.

Alan Bundy was the PI 

Jacques Fleuriot was a Co-Investigator 

Gavin Keighren was an MSc student who carried out the experiments using Cl-Atse.

Publications

Links

AnaBlock homepage.

Other researchers in the field of API analysis include:

• Mike Bond
• Jolyon Clulow
• Ross Anderson
• Vinod Ganapathy
• Ben Adida
• Véronique Cortier
• Judicaël Courant
• Jon Herzog

Related groups and projects in the University of Edinburgh:

• The Mobility and Security Group in LFCS
• XML Security in the Database Group