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