arXiv · 2410.01568
Adaptive Exploit Generation against Security Devices and Security APIs
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.
Explore related subjects
Keep this discovery
Robert Künnemann, Julian Biehl. 2024-10-02. Adaptive Exploit Generation against Security Devices and Security APIs. https://arxiv.org/abs/2410.01568
Cite the original work for its findings. Save a collection to share your selection of sources.