工程化正式验证的自动漏洞发现器
摘要：通过使用符号而不是具体输入的程序分析技术进行符号执行。这个原则允许同时探索许多程序路径。尽管这种技术得到了广泛应用，特别是在程序测试中，但很少有人致力于研究符号执行的语义基础。如果没有这些基础，关于符号执行器正确性的关键问题就无法得到令人满意的答案：报告的错误是否可以重现，还是误报（soundness）？如果让测试工具运行足够长的时间，我们能确保找到所有的错误吗（completeness）？本文提出了一种系统的方法，通过将编程语言的操作语义与符号语义相联系，来工程化可证明正确且完备的基于符号执行的错误查找器。与前期关于符号执行语义的研究不同的是，我们关注符号错误查找器的关键实现细节的正确性，包括搜索策略和约束求解器在剪枝搜索空间方面的作用。我们通过在Coq证明助手中实现WiSE，一个面向命令式语言的验证过的错误查找器原型，并证明其正确和完备性来展示我们的方法。我们证明WiSE的设计原则在交互式证明助手的生态系统之外也适用，这是通过（1）自动提取OCaml实现以及（2）将WiSE转换为PyWiSE，一个功能等效的Python版本实现的。
作者：Arthur Correnson, Dominic Steinhoefel
论文ID：2305.05570
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-10