Adaptive Exploit Generation against Security Devices and Security APIs

TL;DR

This paper introduces a formal, automated method for generating proof-of-concept exploits against security APIs by extending ProVerif with a template mechanism, enabling the derivation of configuration-specific attacks.

Contribution

It presents a novel extension to ProVerif that transforms attack traces into executable programs, facilitating exploit generation against security APIs.

Findings

Successfully applied to W3C Web Cryptography API

First formal model of YubiHSM2 created

Automated exploit derivation demonstrated

Abstract

Proof-of-concept exploits help demonstrate software vulnerability beyond doubt and communicate attacks to non-experts. But exploits can be configuration-specific, for example when in Security APIs, where keys are set up specifically for the application and enterprise the API serves. In this work, we show how to automatically derive proof-of-concept exploits against Security APIs using formal methods. We extend the popular protocol verifier ProVerif with a language-agnostic template mechanism. Employing program snippets attached to steps in the model, we can transform attack traces (which ProVerif typically finds automatically) into programs. Our method is general, flexible and convenient. We demonstrate its use for the W3C Web Cryptography API, for PKCS#11 and for the YubiHSM2, providing the first formal model of the latter.