skip to content
 

Analysis of Cryptographic Security APIs

Presented by: 
G Steel [ENS Cachan]
Date: 
Tuesday 31st January 2012 - 16:30 to 17:15
Venue: 
INI Seminar Room 1
Abstract: 
In practice, many developers use cryptography via an application program interface (API) either to a software library or a hardware device where keys are stored and all cryptographic operations take place. Designing such interfaces so that they offer flexible functionality but cannot be abused to reveal keys or secrets has proved to be extremely difficult, with a number of published vulnerabilities in widely-used APIs appearing over the last decade. This talk will discuss recent research on the use of formal methods to specify and verify such interfaces in order to either detect flaws or prove security properties. We will focus on the example of RSA PKCS#11, the most widely used interface for cryptographic devices. We will demonstrate a tool, Tookan, which can reverse engineer the particular configuration of PKCS#11 in use on some device under test, construct a model of the device's functionality, and call a model checker to search for attacks. If an attack is found, it can be executed automatically on the device. We will comment on design principles for the next generation of APIs.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons