核心概念
本文提出了一種自動生成針對安全API的概念性漏洞利用的方法,利用形式化方法將攻擊痕跡轉換為可執行的程式碼。
摘要
本文提出了一種自動生成概念性漏洞利用(PoC)的方法,針對安全API進行攻擊。作者擴展了流行的協議驗證工具ProVerif,加入了一種語言無關的模板機制。通過在模型中附加程式碼片段到步驟上,可以將ProVerif自動找到的攻擊痕跡轉換為程式碼。這種方法是通用的、靈活的且方便使用的。作者在三個案例研究中演示了這種方法的使用,包括W3C Web Cryptography API、PKCS#11和YubiHSM2 API。這種方法可以在合理的時間內(通常在5分鐘內)找到攻擊,並生成相應的PoC。生成的PoC程式碼具有良好的可讀性和可維護性,因為它們是從模型中自動生成的,而不是手動編寫的。
統計資料
在Web Cryptography API的實驗中,生成PoC的時間從1分45秒到5分10秒不等,與密鑰數量成正比。
在PKCS#11的實驗中,生成PoC的時間非常快,在0.025到0.037秒之間。
在YubiHSM2的實驗中,生成PoC的時間從0.5秒到2分鐘不等,與密鑰數量和複雜度成正比。
引述
"PoCs are communication tools.. The biggest argument is that PoCs help non-experts understand security-relevant issues."
"PoCs make analysis results accessible.. Our case studies analyze hardware and software configuration using formal methods, but the generated PoCs are accessible to system operators even if they are unfamiliar with formal methods."
"PoCs are trivially sound.. Taking communication aside, such evidence can be useful to bridge the gap between the model and the actual system."