基于SAT的C程序缓冲区溢出漏洞精确检测与原型工具

本文探讨了一种创新的基于SAT（布尔可满足性）的C程序缓冲区溢出漏洞检测技术。作者陈石坤、李舟军、黄永刚和邢建英来自国防科技大学计算机学院、北京航空航天大学计算机学院以及中国信息安全测评中心，他们共同提出了这种方法来解决C语言编程中常见的安全问题。缓冲区溢出，由于其潜在的严重安全性风险，如允许恶意代码执行，一直是软件安全研究的重要课题。 该检测方法的核心在于，首先通过源代码变换技术在程序源码中添加特定的缓冲区属性刻画语句，这些语句用于描述缓冲区的边界条件。接着，通过构造布尔表达式（布尔可满足性问题），这些语句被转化为断言，用于捕捉缓冲区溢出的逻辑状态。利用现代的SAT工具，这些断言会被系统性地检查，如果存在不符合预期的布尔赋值，即表示可能存在缓冲区溢出漏洞。 通过实施这种方法，研究者开发了一个原型工具，它能接收C源代码作为输入，自动检测其中的缓冲区溢出隐患，实现了无侵入式的静态分析。在对1164个公开基准程序的测试中，这个工具表现出很高的准确度，准确地定位出溢出漏洞，而且没有出现误报，仅有约2.08%的漏报率。这表明该技术在实际应用中具有较高的实用性和有效性。 与传统的动态检测方法相比，静态检测的优势在于无需在运行时增加额外的开销，且能在软件发布前就发现并修复漏洞，有助于提升软件的质量和安全性。此外，SAT技术的应用展示了将复杂的问题转换为符号逻辑求解的潜力，对于自动化和大规模软件安全审计具有重要意义。 总结来说，这篇论文提出了一种基于布尔可满足性理论的C程序缓冲区溢出检测方法，通过源代码分析和逻辑推理，有效地识别并预防了这种常见的安全威胁，为软件开发过程中的安全审查提供了有力支持。