Towards a type-based analysis of real PKCS#11 devices
Riccardo Focardi, Flaminia L. Luccio · ARCA (Università Ca' Foscari Venezia) · 2012
PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In [7] we have presented a type-based analysis to prove, on abstract API specifications, that the secrecy of sensitive keys is preserved under a certain policy. In this paper we discuss how this type system might be extended to type-check a real security policy implemented in the opencryptoki PKCS#11 software token. This is a first step towards a type-based analysis of real PKCS#11 devices.