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.

翻译：概念验证型漏洞利用有助于明确展示软件漏洞，并向非专业人士传达攻击方式。然而，漏洞利用可能具有配置特异性，例如在安全API场景中，密钥需针对API服务的具体应用与企业进行专门设置。本研究提出一种基于形式化方法的自动化概念验证漏洞利用生成技术。我们通过引入与编程语言无关的模板机制，扩展了主流协议验证工具ProVerif。通过在模型步骤中附加程序片段，可将攻击轨迹（通常由ProVerif自动发现）转化为可执行程序。该方法具有通用性、灵活性与便捷性。我们以W3C Web加密API、PKCS#11及YubiHSM2为例进行验证，其中YubiHSM2首次建立了形式化模型。