11

我听说过一些关于使用自动定理证明器试图证明软件系统中不存在安全漏洞的信息。一般来说，这很难做到。

我的问题是，有没有人使用类似的工具来查找现有或拟议系统中的漏洞？

Eidt：我不是要证明软件系统是安全的。我问的是寻找（最好是以前未知的）漏洞（甚至它们的类别）。我在想（但不是）这里的黑帽：描述系统的形式语义，描述我想要攻击的内容，然后让计算机找出我需要使用什么动作链来接管你的系统。

4

8 回答 8

5

是的，在这方面已经做了很多工作。可满足性（SAT 和 SMT）求解器经常用于查找安全漏洞。例如，在 Microsoft 中，一个名为SAGE的工具用于从 Windows 中消除缓冲区溢出错误。SAGE 使用Z3 定理证明器作为其可满足性检查器。如果您使用“智能模糊测试”或“白盒模糊测试”等关键字搜索互联网，您会发现其他几个使用可满足性检查器来查找安全漏洞的项目。高级想法如下：收集程序中的执行路径（您没有设法执行，也就是说，您没有找到使程序执行它的输入），将这些路径转换为数学公式，并将这些公式提供给可满足性求解器。这个想法是创建一个只有当有一个输入可以使程序执行给定路径时才可满足/可行的公式。如果产生的公式是可满足的（即可行的），那么可满足性求解器将产生分配和期望的输入值。白盒模糊器使用不同的策略来选择执行路径。主要目标是找到一个输入，使程序执行导致崩溃的路径。

于 2011-08-26T20:35:50.870 回答
4

因此，至少在某种有意义的意义上，证明某事是安全的反面是找到不安全的代码路径。

试试Byron Cook 的 TERMINATOR 项目。

Channel9 上至少有两个视频。 这是其中之一

他的研究可能是您了解这个极其有趣的研究领域的一个很好的起点。

Spec# 和 Typed-Assembly-Language 等项目也是相关的。为了将安全检查的可能性从运行时移回编译时，它们允许编译器将许多错误的代码路径检测为编译错误。严格来说，它们无助于您陈述的意图，但它们利用的理论可能对您有用。

于 2010-09-09T17:20:16.630 回答
2

我目前正在与其他人一起在 Coq 中编写 PDF 解析器。虽然在这种情况下的目标是生成一段安全的代码，但这样做肯定有助于发现致命的逻辑错误。

一旦您熟悉了该工具，大多数证明就变得容易了。更难的证明会产生有趣的测试用例，有时会触发真实的现有程序中的错误。（对于查找错误，一旦您确定没有错误可找到，您可以简单地将定理假设为公理，无需进行认真的证明。）

大约一个月前，我们在使用多个/较旧的 XREF 表解析 PDF 时遇到了问题。我们无法证明解析终止。考虑到这一点，我在预告片中构建了一个带有循环 /Prev 指针的 PDF（谁会想到这个？:-P），这自然让一些观众永远循环。（最值得注意的是，Ubuntu 上几乎所有基于 poppler 的查看器。让我发笑并诅咒 Gnome/evince-thumbnailer 吃掉了我所有的 CPU。我认为他们现在修复了它。）

使用 Coq 查找较低级别的错误会很困难。为了证明任何事情，您需要一个程序行为模型。对于堆栈/堆问题，您可能必须对 CPU 级或至少 C 级执行进行建模。虽然在技术上是可行的，但我会说这不值得付出努力。

使用 SPLint for C 或用您选择的语言编写自定义检查器应该更有效。

于 2011-07-10T23:57:09.557 回答
2

STACK和KINT使用约束求解器来查找许多 OSS 项目中的漏洞，例如 linux 内核和 ffmpeg。项目页面指向论文和代码。

于 2013-12-20T23:22:43.053 回答
1

它与定理证明并不真正相关，但模糊测试是一种以自动化方式发现漏洞的常用技术。

于 2010-09-09T17:15:34.903 回答
1

有一个经过L4 验证的内核正试图做到这一点。但是，如果您查看利用历史，就会发现全新的攻击模式，然后编写的许多软件非常容易受到攻击。例如，直到 1999 年才发现格式字符串漏洞。大约一个月前，HD Moore 发布了DLL Hijacking，实际上 windows 下的所有东西都是易受攻击的。

我认为不可能证明一个软件可以抵御未知攻击。至少直到一个定理能够发现这样的攻击，据我所知，这还没有发生。

于 2010-09-09T17:20:58.013 回答
0

免责声明：我对自动定理证明器几乎没有经验

一些观察

  • 像密码学这样的东西很少被“证明”，只是被认为是安全的。如果你的程序使用类似的东西，它只会和加密一样强大。
  • 定理证明者不能分析一切（或者他们能够解决停机问题）
  • 您必须非常清楚地定义不安全对证明者意味着什么。这本身就是一个巨大的挑战
于 2010-09-09T17:21:23.783 回答
0

是的。许多定理证明项目通过展示软件中的漏洞或缺陷来展示其软件的质量。为了使其与安全相关，想象一下在安全协议中发现一个漏洞。Carlos Olarte 博士 Ugo Montanari 的论文有一个这样的例子。

它在应用程序中。与安全性或其特殊知识有关的定理证明器本身并不是真正的。

于 2010-09-09T18:12:59.457 回答