SAT驱动的C程序缓冲区溢出漏洞检测方法

"该文介绍了一种基于SAT（布尔可满足性问题）的C程序缓冲区溢出漏洞检测技术，通过源代码变换和断言来检测潜在的安全问题。该方法在1164个公开基准程序上进行了测试，取得了较高的准确性和较低的漏报率。" 在计算机编程中，尤其是C语言编程，缓冲区溢出是一种常见的安全漏洞，可能导致数据丢失、系统崩溃甚至恶意代码执行。缓冲区溢出通常发生在程序员没有正确地管理内存分配和使用时，当向固定大小的缓冲区写入超过其容量的数据时发生。这种错误可以被攻击者利用，执行未授权的指令或获取敏感信息。 本文提出了一种新的检测C语言缓冲区溢出的方法，它基于SAT求解器。SAT（布尔可满足性问题）是逻辑满足问题的一个分支，常用于解决复杂的问题，如软件验证和电路设计。在该方法中，首先通过源代码变换在程序中添加特定的语句，这些语句用于描述缓冲区的属性。接着，使用断言来表达缓冲区溢出的条件，即如果某条件满足，则可能发生溢出。这些断言随后通过SAT工具进行检查，以确定是否存在导致溢出的路径。 该方法的一个关键优点是它可以处理源代码级别的问题，而不需要编译后的二进制代码，这使得分析过程更直接且可能更有效。此外，通过实际应用，该技术成功设计并实现了一个原型工具，该工具能自动检测输入的源代码中可能存在的缓冲区溢出漏洞。在1164个公开的基准程序上进行的实验表明，该工具能够准确地识别出漏洞，没有产生误报，但存在约2.08%的漏报率，这意味着虽然总体表现优秀，但仍有少数漏洞可能被遗漏。 关键词涉及的模型检验是软件验证的一种技术，它通过建立程序执行的数学模型来检查是否满足特定的属性。在本例中，模型检验被用来检查缓冲区溢出的断言是否可满足，即是否存在满足溢出条件的执行路径。布尔可满足性问题（SAT）作为模型检验的一部分，是寻找模型中满足所有约束的解的关键步骤。 这项研究提供了一种基于SAT的高效和准确的C程序缓冲区溢出检测方法，有助于提高软件安全性，减少因缓冲区溢出导致的潜在风险。未来的研究可能关注于优化工具以降低漏报率，或者将这种方法扩展到其他编程语言和更复杂的漏洞类型。