ASA on Wednesday, July 21st

09:15‑10:00 Session 1
Location: IF G.03
09:15 Opening remarks
09:30 Robert Watson and Jonathan Anderson
Connecting the Dot-Dots: Model Checking Concurrency in a Security API

Capsicum is a lightweight operating system capability sandbox framework planned for inclusion in FreeBSD 9. While developing the system, we discovered a concurrency vulnerability in which colluding sandboxed applications could manipulate the file system lookup API to escape from sandboxing. To explore the problem further, we employed model checking to determine the minimum requirements for the semantics of file system access via UNIX APIs, and various strategies for limiting API semantics in order to close the vulnerability. We also discovered that near-identical vulnerabilities are present in at least one other piece of existing sandboxing technology.

10:30‑12:30 Session 2
Location: IF G.03
10:30 Graham Steel
Abstractions for Verifying Key Management APIs

Key management APIs are used to control the use of tamper-resistant cryptographic hardware devices such as smartcards. Such APIs are designed to preserve some security properties, such as secrecy of sensitive keys, no matter what sequence of API calls are made. Multiset rewriting has been used successfully to model and analyse APIs such as the RSA standard PKCS\#11 \cite{delaune08pkcs11} and the SeVeCoM API for cryptographic devices on vehicles \cite{steel09sevecom}. A challenge for such formal modelling is that APIs typically contain commands that generate fresh keys and fresh pointers to keys on the device (known as handles). It is not clear a priori whether a proof of security for $n$ keys and handles is valid if $n+1$ fresh keys are generated.

In a previous paper \cite{froeschle09pkcs11}, we proposed an abstraction for keys and key handles for the PKCS\#11 API that permits proofs of security for unbounded fresh handles and keys to be found by automatic tools. Since that paper, we have experimented with several commercial PKCS\#11 devices, and discovered that in fact they almost exclusively implement the standard in a quite different way to the one we considered. We had assumed that the device would allow keys to be generated and their attributes or metadata set by subsequent commands, as is described in the standard. The setting of the attributes for a key governs which commands in the API can be used with that key, and a careful regulation of these attributes is vital for the security of the interface. In fact, most devices disable the commands for changing the attributes of a key, but instead allow the key generation command to be called with a variety of different templates, which set the attributes for the key. We can adapt our abstraction to this scenario, but the number of possible templates is typically very large, resulting in a model that is impractical for automated tools.

In this talk I will describe a new abstraction algorithm that computes a set of templates that is sufficient for proving security for a given API model. The abstraction applies to PKCS\#11 and other similar APIs. I will explain the proof of soundness, and demonstrate the abstraction in action on some models of real devices. Using the abstraction we are able to prove security for some new PKCS\#11 configurations which, unlike those previously proposed \cite{cachin09secure,froeschle09pkcs11}, do not require any new mechanisms to be added to the standard.

11:00 Sibylle Froeschle and Nils Sommer
When is a PKCS#11 configuration secure?

We propose to present work in progress on the verification of PKCS#11 configurations.

11:30 Matteo Bortolozzo, Matteo Centenaro, Riccardo Focardi and Graham Steel
CryptokiX: a cryptographic software token with security fixes

PKCS#11 defines a widely adopted API for cryptographic tokens, it provides access to cryptographic functionalities and should preserve certain security properties. For example, PKCS#11 is intended to protect its sensitive cryptographic keys even when connected to a compromised host, however it is known to be vulnerable to various attacks that break this property. This paper presents a software token implementing different security patches to PKCS#11 which prevent the leakage of sensitive keys. This offers a proof-of-concept that secure, fully fledged tokens could be realized in practice and might constitute a reference and testing framework for hardware producers.

12:00 François Dupressoir, Andrew D. Gordon and Jan Jürjens
Verifying Authentication Properties of C Security Protocol Code Using General Verifiers

Implementing security protocols in low-level languages such as C often introduces logical vulnerabilities that may not be present in the protocol's specification. Some effort has been made to verify security properties of implementations directly, but we believe they offer unsatisfactory results in practice. We present a new verification method for security properties of real C implementations of security protocols, that relies on a general C verification tool. We define an attacker model on C programs that is parametrised by the program's exported annotated API.

14:00‑15:00 Session 3
Location: IF G.03
14:00 Ronald Toegl
Construction of a Trusted Virtual Security Module

Cryptographic key material needs to be protected. Currently, this is achieved by either pure software based solutions or by more expensive dedicated hardware security modules. We report on an architecture that combines virtualization and Trusted Computing mechanisms to enable commodity personal computer hardware to offer integrity protection and strong isolation. Based on this, we present a security module that offers a compact security API designed for verifiability.

14:30 Mike Bond and George French
Hidden Semantics: why? how? and what to do?

This paper describes the authors’ experience working with security APIs which have been “patched” to prevent vulnerabilities – that is, APIs which have been minimally modified t prevent an attack rather than being subject to a redesign. We survey the patches to the API attacks of the last 10 years and observe the trend toward the pragmatic fix which does not substantially change the API but encodes ever more hidden semantics in the behavior of each ide. Vendor-specific implementations of APIs also add hidden semantics. Hidden semantics is important to the API analysis community because it may limit the applicability of results based on API messages alone, indeed it has driven the creation of tools such as [7] and a lot of work surround analysis of variants of PKCS#11 which all exist within the same framework [6] . Furthermore it raises the question whether the adaptation of standard protocol notation to Security APIs presents a full enough picture to be useful; while formal analysis has yielded new notations well suited to model checkers and other tools, what is the most appropriate way of expressing hidden semantics in a way which bridges the gap between formal and applied communities?

15:30‑17:00 Session 4
Location: IF G.03
15:30 Andrew Gordon, Reiner Hähnle, Cliff Jones, Mark Ryan, Riccardo Focardi, Johann Schumann
Panel Session; Formal Methods as/in/for industry

Joint panel session with the VERIFY workshop.