BCS*_*BCS 11 security theorem-proving
我已经听过一些关于使用自动化定理证明的尝试,以证明软件系统中不存在安全漏洞.总的来说,这是非常难以做到的.
我的问题是,是否有人使用类似工具来查找现有或建议系统中的漏洞？
Eidt:我不是要问证明软件系统是安全的.我问的是找到(理想情况下以前未知的)漏洞(甚至是它们的类).我在想这里(但不是)黑帽子:描述系统的形式语义,描述我想要攻击的内容,然后让计算机弄清楚我需要用什么行动来接管你的系统.
是的,在这个领域已经做了很多工作.可靠性(SAT和SMT)解算器经常用于查找安全漏洞.例如,在Microsoft中,使用名为SAGE的工具来消除来自Windows的缓冲区溢出错误.SAGE使用Z3定理证明器作为其可满足性检查器.如果您使用"智能模糊测试"或"白盒模糊测试"等关键字搜索互联网,您会发现其他几个项目使用可满足性检查器来查找安全漏洞.高级想法如下:收集程序中的执行路径(您没有设法运行,也就是说,您没有找到使程序执行它的输入),将这些路径转换为数学公式,并将这些公式提供给可满足性求解器.我们的想法是只有在有一个输入使程序执行给定路径时才能创建一个可满足/可行的公式.如果生成的公式是可满足的(即可行的),则可满足性求解器将产生分配和期望的输入值.白盒模糊器使用不同的策略来选择执行路径.主要目标是找到一个输入,使程序执行导致崩溃的路径.
因此，至少在某种有意义的意义上，证明某些东西安全的反面是找到不安全的代码路径。
Channel9 上至少有两个视频。 这是其中之一
他的研究可能是您了解这个极其有趣的研究领域的良好起点。
Spec# 和 Typed-Assembly-Language 等项目也相关。为了将安全检查的可能性从运行时移回编译时，它们允许编译器将许多错误的代码路径检测为编译错误。严格来说，它们并不能帮助您实现既定的意图，但它们所利用的理论可能对您有用。