我已经听过一些关于使用自动化定理证明的尝试，以证明软件系统中不存在安全漏洞。总的来说，这是非常难以做到的。
我的问题是有没有人完成使用类似工具的工作 找 现有或拟议系统中的漏洞？
艾德：我是 不 询问证明软件系统是安全的。我问的是找到（理想情况下以前未知的）漏洞（甚至是它们的类）。我在想这里（但不是）黑帽子：描述系统的形式语义，描述我想要攻击的内容，然后让计算机弄清楚我需要用什么行动来接管你的系统。
我已经听过一些关于使用自动化定理证明的尝试，以证明软件系统中不存在安全漏洞。总的来说，这是非常难以做到的。
我的问题是有没有人完成使用类似工具的工作 找 现有或拟议系统中的漏洞？
艾德：我是 不 询问证明软件系统是安全的。我问的是找到（理想情况下以前未知的）漏洞（甚至是它们的类）。我在想这里（但不是）黑帽子：描述系统的形式语义，描述我想要攻击的内容，然后让计算机弄清楚我需要用什么行动来接管你的系统。
因此，至少在一些有意义的意义上，证明某些东西是安全的相反的是找到它不是的代码路径。
在Channel9上至少有两个视频。 这是其中之一
他的研究可能是您了解这个非常有趣的研究领域的一个很好的起点。
Spec＃和Typed-Assembly-Language等项目也是相关的。为了将安全检查的可能性从运行时转移到编译时，它们允许编译器检测许多错误的代码路径作为编译错误。严格来说，它们并不能帮助您明确的意图，但它们利用的理论可能对您有用。
是的，在这个领域已经做了很多工作。可满足性（SAT和SMT）求解器经常用于发现安全漏洞。 例如，在Microsoft中，一个名为的工具 智者 用于根除窗口中的缓冲区溢出错误。 SAGE使用 Z3定理证明 作为其可满足性检查器。 如果您使用“智能模糊测试”或“白盒模糊测试”等关键字搜索互联网，您会发现其他几个项目使用可满足性检查器来查找安全漏洞。 高级想法如下：收集程序中的执行路径（您没有设法运行，也就是说，您没有找到使程序执行它的输入），将这些路径转换为数学公式，并将这些公式提供给可满足性求解器。 我们的想法是只有在有一个输入使程序执行给定路径时才能创建一个可满足/可行的公式。 如果产生的公式是可满足的（即可行的），那么可满足性求解器将产生分配和所需的输入值。白盒模糊器使用不同的策略来选择执行路径。 主要目标是找到一个输入，使程序执行导致崩溃的路径。
我目前正在与其他人一起在Coq中编写PDF解析器。虽然这种情况下的目标是生成一段安全的代码，但做这样的事情肯定有助于找到致命的逻辑错误。
一旦熟悉了该工具，大多数证据都变得简单。更难的证明会产生有趣的测试用例，有时会触发真实的现有程序中的错误。 （并且为了找到错误，一旦你确定没有找到错误，就没有必要进行严格的证明，你可以简单地将定理假设为公理。）
大约一个月前，我们遇到了一个问题，解析了多个/旧的XREF表格的PDF。我们无法证明解析终止。考虑到这一点，我在预告片中构建了一个带有循环/上一个指针的PDF（谁想到了这个？:-P），这自然使一些观众永远循环。 （最值得注意的是，几乎所有基于poppler的浏览器都在Ubuntu上。让我笑，并诅咒Gnome / evince-thumbnailer吃了我所有的CPU。我认为他们现在修复它了，所以。）
使用Coq查找较低级别的错误将很困难。为了证明什么，你需要一个程序行为的模型。对于堆栈/堆问题，您可能必须建模CPU级别或至少C级执行。虽然技术上可行，但我认为这不值得。
使用SPLint for C或使用您选择的语言编写自定义检查器应该更有效。
它与定理证明无关，但是 模糊测试 是一种以自动方式查找漏洞的常用技术。
有 L4验证内核 这是试图做到这一点。但是，如果你看一下利用历史，就会发现全新的攻击模式，然后很多写到这一点的软件很容易受到攻击。例如，格式字符串漏洞直到1999年才被发现。大约一个月前H.D.摩尔发布了 DLL劫持 而且几乎所有东西都在窗户下 很脆弱。
我不认为有可能证明一块软件可以抵御未知攻击。至少直到一个定理能够发现这样的攻击，并且据我所知这没有发生。
免责声明：我对自动化定理证明器几乎没有经验
一些观察
是。许多定理证明项目通过展示软件中的漏洞或缺陷来展示其软件的质量。为了使其与安全性相关，只需想象在安全协议中找到漏洞。 Carlos Olarte的博士Ugo Montanari的论文有一个这样的例子。
它在应用程序中。并非真正的定理证明本身与安全性或其特殊知识有关。