Analysis of Cryptographic Security APIs

During the last session of the first day of the workshop "Is Cryptographic Theory Practically Relevant?", Graham Steel (ENS Cachan) gave a talk titled ``Analysis of Cryptographic Security APIs``.

The talk focused on the security analysis of RSA public key Cryptography Standard (PKCS)#11 which is the most popular used standard for designing cryptographic device interfaces. Tamper-resistant devices such as USB keys and smartcards are often employed in insecure environments to carry out secure operations such as enabling authentication, protect sensitive data or facilitate secure login.  

Graham first gave a brief introduction to PKCS#11-based API. In a PKCS#11-based API, an host machine interacts with a cryptographic device and the sensitive cryptographic keys stored on the tamper-resistant support are supposed to remain protected  even when the host machine is compromised. Any application is supposed to access the objects stored on the device in a guarded way. Indeed, an object is referenced by means of an handle whose 

value does not reveal any information about the object. Objects also come with attributes

describing properties of the object. Moreover, new objects can be created by calling a key generation command and attributes may be set by calling a set attribute command.

When a function is called to use a given object,  the device first checks that the attributes of the object allow the function to be executed. Two further functionalities are considered: Wrap and Unwrap keys. Those functionalities are fundamental for the way PKCS#11 deals with key management, indeed they are used for secure transport of keys between devices or to protect them while in untrusted storage. 

Subsequently, Graham outlined the few hints the standard provides about PKCS#11 security. The standard states that in order to provide protection to the secret keys there are some special attributes: ``sensitive`` and ``extractable`` attributes. The standard requires that to protect a key from being revealed, the attribute sensitive must be set to true. Moreover, once an attribute sensitive is set to true, it cannot be reset to false.  Objects whose extractable attribute is set to false cannot be revealed out of the device even when encrypted. Also, once set to false the extractable attribute cannot be set to true.

Unfortunately, such an informal formulation of the security requirements allows to set key attributes in such a way that sensitive keys become compromised as shown by the attacks  proposed by Clulow in Ches 2003  and those reported by Delaune et al in CSF 2008.

Graham told to the audience that his team contacted manufacturers with the hope of cooperating on analyzing real implementations, but the responses were pretty disappointing. Basically, manufacturers answered that there was no need to be worried since despite the fact that PKCS#11 may be insecure if implemented in a naive way, they have expert working on this issues.  Graham's team at this point had two possible choices: drop the subject or try to make a tool in order to find vulnerabilities on real devices. Obviously, they made the second choice and built the tool called ``Tookan``.

Tookan first extracts the functionalities of the device by means of a reverse engineering process. The results is written in a meta-language for PKCS#11 models that Tookan uses to generate the input for a model-checker. Finally, the model-checker output is sent back to Tookan for testing it directly on the device. 

In the second part of the talk Graham showed a demo of Tookan. He run the tool on an Aladdin eToken PRO. 

While waiting for the tool to process, he pointed out that the reverse engineering process is not complete. On some instances, it could result in a too restrictive model to be able of finding an attack. However, experimental results show that Tookan performs pretty well. Indeed, it was able to find several real attacks on flawed devices. As for the possibility of proving that a configuration is indeed secure, Tookan also provides the option of performing an over-approximation for the generation of fresh handles and keys (whose number may be unbounded). This over-approximation allows Tookan to show some configurations to be actually secure but there are other configurations for which the tool was not able to show correctness.  

Afterwards, Graham showed experimental results from using Tookan to find attacks on commercially available devices. For each device he shows a summary of the configuration information obtained by means of the reverse engineering module and a collection of attacks found. From the results can be noticed that every device providing the wrapping of sensitive keys  functionality, is also vulnerable to attacks while all the other devices avoid such attacks at the price of removing such functionality. 

Finally, Graham reported about manufacturer reactions. RSA registered vulnerability with Mitre and issued security advising the same day Graham was presenting the work at CCS 2010. Alladin and Gemalto sent responses for website. They, essentially, claim that the vulnerabilities found, are not relevant for their costumers. Anyone else sent minimal responses such as requesting to know who else has vulnerabilities. On the positive side, Tookan is now being used by Boeing and a major UK-based bank. 

Recently, Tookan has been deployed in testing PKCS#11-compatible HSMs that have a more sophisticated attribute policies than other devices. Still Tookan found many attacks. 

After thanking the speaker, the audience raised several very interesting questions that yield discussions ranging from the limitations due to the kind of abstraction Tookan performs, the possibility of using theorem provers and the amount of effort needed to generalize Tookan in order to verify different APIs. Such discussions along with the entire talk can be listened online at http://www.newton.ac.uk/programmes/SAS/seminars/013116301.html.