A security API is an Application Program Interface that allows untrusted code to access sensitive resources in a secure way. It is the interface between processes running with different levels of trust. Examples of security APIs include the interface between the tamper-resistant chip on a smartcard (trusted) and the code running on the client application (untrusted), the interface between a cryptographic Hardware Security Module (or HSM, trusted) and the host machine (untrusted), and web service APIs (an interface between a server, trusted by the service provides, and the rest of the Internet).
The crucial aspect of a security API is that it is designed to enforce a policy, i.e. no matter what sequence of commands in the interface are called, and no matter what the parameters, certain security properties should continue to hold. This means that if the less trusted code turns out to be malicious (or just faulty), the carefully designed API should prevent compromise of critical data. Designing such an interface is extremely tricky and error prone, and over the last ten years, serious vulnerabilities in the security APIs deployed in HSMs in the ATM (cash machine) network and in commodity security devices like smartcards and USB keys have come to light.
A number of formal methods researchers have turned their attention to security APIs over the last five years. While significant advances have been made and notable results achieved, such as the discovery of several new attacks, the process of specifying and verifying the security policy for such APIs still lacks both satisfactory foundations and efficient algorithms. At the same time, the security API paradigm is being proposed as a solution for more and more applications, from social networks to smartphones, with more complicated and less well understood security goals.
The objective of the seminar was to bring together researchers in academia and industry around the topic of security APIs and their analysis. There were three main aims:
- To address the shortcomings of current API analysis techniques as applied to the relatively well explored domains of cryptographic key management and HSMs, in particular in their ability to deal with global mutable state and their models of cryptography.
- To identify the security API requirements arising from the new generation of applications, in mobile device applications and web services, and map out the research problems that need to be solved in order that formal API analysis can be applied here.
- To find ways to include the process and results of formal API analysis into the standards and certification procedures.
Some progress was made on all these points in the talks and the discussions late into the evening that followed in the conducive environment of Schloss Dagstuhl. On the first point, several talks presented models specifically aimed at modelling state in a more satisfactory way, and we had a tutorial on the verification methods used in program analysis. Several new application areas for API analysis were presented, including car to car communication and password protection. Some highly enlightening talks on the standards process helped to improve understanding of the problem, if not providing steps to an easy solution. The variety of open problems identified (see summary below) shows that this is a vibrant area of computer security research with much promise for the future.
- Pedro Adao (IST - Lisbon, PT)
- Ross Anderson (University of Cambridge, GB) [dblp]
- Daniel Angermeier (Fraunhofer AISEC - München, DE)
- David R. Aspinall (University of Edinburgh, GB)
- Romain Bardou (INRIA - Paris, FR)
- Mike Bond (University of Cambridge, GB)
- Véronique Cortier (LORIA - Nancy, FR) [dblp]
- Marion Daubignard (Direction Generale de l'Armement, FR)
- Stéphanie Delaune (ENS - Cachan, FR) [dblp]
- Riccardo Focardi (University of Venezia, IT)
- Sibylle Fröschle (OFFIS - Oldenburg, DE) [dblp]
- Steve Kremer (INRIA Lorraine - Nancy, FR) [dblp]
- Robert Künnemann (ENS - Cachan, FR)
- Ralf Küsters (Universität Trier, DE) [dblp]
- Flaminia L. Luccio (University of Venezia, IT)
- Matteo Maffei (Universität des Saarlandes, DE) [dblp]
- Sebastian Mödersheim (Technical University of Denmark - Lyngby, DK)
- Benjamin Morin (ANSSI - Paris, FR)
- Andreas Philipp (Utimaco Safeware AG, DE)
- Markus N. Rabe (Universität des Saarlandes, DE)
- Phillip Rogaway (University of California - Davis, US) [dblp]
- Mark D. Ryan (University of Birmingham, GB) [dblp]
- Stefanie Schlegel (OFFIS - Oldenburg, DE)
- Jörg-Cornelius Schneider (Deutsche Bank - Eschborn, DE)
- Laurent Simon (University of Cambridge, GB)
- Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE & MPI für Informatik, Saarbrücken, DE) [dblp]
- Marco Squarcina (University of Venezia, IT) [dblp]
- Graham Steel (ENS - Cachan, FR)
- Petr Svenda (Masaryk University - Brno, CZ)
- Susan Thompson (MasterCard Worldwide, Warrington, GB)
- Frank Thunig (Utimaco Safeware AG, DE)
- Ronald Toegl (TU Graz, AT)
- security / cryptography
- security APIs
- key management
- software verification
- security protocols