Semantics-Driven Testing of the PKCS11 API

Presented as part of the 2019 HCSS conference.

PKCS11 is an industry standard API for communicating with cryptographic devices such as hardware security modules (HSMs). PKCS11 is a security critical API, and so implementation errors can have serious consequences. However, the PKCS11 standard is large and complex, with 100 pages of documentation for almost 50 functions. As a result, it is very challenging for developers to avoid API implementation errors. This is the problem that our work addresses.

We take a model-driven testing approach. That is, we define a concise and unambiguous formal model of PKCS11, and based on this, we synthesize a high-coverage test suite. Our model is built on the Cryptol verification language which lets us capture the details of the semantics of the PKCS11 API. We developed this approach in collaboration with Amazon Web Services (AWS). Our test suite is integrated into the AWS CI/CD pipeline, preventing new bugs from entering production.

Our synthesis engine uses the model to generate tests across different API use cases. For each case, we use the model to predict the expected result, and test it against the implementation behavior. We use a combination of graph traversal and SMT solving to maximize coverage across different combinations of API calls and states. As a result, our test suite provides total coverage of API paths and return codes, giving a very high degree of assurance.

We have applied our approach to two PKCS11 libraries: the open source OpenCryptoki library, and the closed-source implementation used by AWS. In both cases, our approach discovered high-priority bugs that standard techniques missed. In OpenCryptoki, we discovered incorrectly implemented state machines, incorrect return codes, lossy object copies, segmentation faults and unchecked pointers. The AWS implementation originated with a third-party HSM supplier. Despite a short timescale and a complex legacy codebase, our technique caught multiple errors before deployment.

We see two main contributions from this work. First, our test suite serves as a resource for PKCS11 developers, and will make future implementations more robust and interoperable. Second, we have demonstrated that our test synthesis approach is highly effective for real-world assurance, and we plan to apply it to a range of cryptographic APIs in future.

Matt Bauer is a research engineer at Galois implementing and building trust around cryptographic protocols and algorithms. He has a PhD from UIUC focusing on cryptographic protocol verification. He has extensive experience implementing cross domain and multi-level systems for mission-critical applications.

Mike Dodds is a Principal Scientist at Galois working on industrial applications of formal methods. Until 2017 he was an assistant professor at the University of York, UK. His research interests include automated verification tools, formal logic and reasoning, concurrency verification, and integrating verification tools into software engineering processes. He leads Galois' collaboration with Amazon Web Services.