基于动态符号执行的C代码缓冲区溢出检测
缓冲区溢出是C程序中众多安全隐患的根源之一，以C程序代码为目标对象，提出了一个基于底层虚拟机中间代码的缓冲区溢出检测工具PathChecker.该工具基于动态符号执行方法，使用无量词谓词公式刻画缓冲区操作的安全性质，并利用可满足模型理论求解器技术检验缓冲区操作的安全性.实验结果表明，该工具能有效检测C代码中的缓冲区溢出漏洞，且易于推广至其他高级程序语言代码和其他类型安全漏洞的检测.
缓冲区溢出检测、动态符号执行、可满足模型理论求解器、底层虚拟机中间代码插桩
39
TP309(计算技术、计算机技术)
国家自然科学基金项目61170189,61370126;国家高技术研究发展计划863计划项目2015AA016004
2016-08-22（万方平台首次上网日期，不代表论文的发表时间）
共5页
50-54
