logo标签列表

使用定理证明器查找攻击

securitytheorem-proving
11

我听说过使用自动定理证明器来尝试证明软件系统中不存在安全漏洞。一般来说，这是非常困难的。

我的问题是，是否有人在使用类似的工具来发现现有或提议的系统中的漏洞？

编辑：我不是在询问如何证明软件系统的安全性。我是在询问如何发现（理想情况下是以前未知的）漏洞（甚至是漏洞类别）。我像黑客那样思考：描述系统的形式语义，描述我要攻击的目标，然后让计算机找出我需要使用哪些行动链路来接管你的系统。

我认为谷歌的原生客户端可以方便地实现这一点；他们通过要求特殊编译器（将代码编译成目标指令集的某个子集，使得验证代码更加“容易”）来作弊。请参阅http://www.chromium.org/nativeclient/reference/research-papers上的NaCl。 - sehe
8个回答
6

在这个领域已经做了很多工作。可满足性（SAT和SMT）求解器通常用于查找安全漏洞。 例如，在微软公司中，一个名为SAGE的工具被用来从Windows中消除缓冲区溢出漏洞。 SAGE使用Z3定理证明器作为其可满足性检查器。 如果您使用“smart fuzzing”或“white-box fuzzing”等关键词在互联网上搜索，您会发现还有其他几个项目使用可满足性检查器来查找安全漏洞。 高层次的想法是：收集程序中的执行路径（即您无法激活的路径，也就是说，您没有找到使程序执行该路径的输入），将这些路径转换成数学公式，并将这些公式提供给可满足性求解器。 目的是创建一个仅在存在输入使程序执行给定路径时才能满足/可行的公式。 如果生成的公式是可满足的（即可行的），则可满足性求解器将生成赋值和所需的输入值。白盒模糊测试器使用不同的策略选择执行路径。 主要目标是找到一个输入，使程序执行导致崩溃的路径。

4
所以，至少在某种有意义的意义上，证明某个东西是安全的相反是找到不安全的代码路径。 尝试看看 Byron Cook's TERMINATOR 项目。 还有至少两个 Channel9 上的视频。这是其中一个。 他的研究很可能是你学习这个极其有趣的研究领域的良好起点。 像 Spec# 和 Typed-Assembly-Language 这样的项目也与此相关。在他们的追求中，将安全检查的可能性从运行时转移到编译时，使编译器能够将许多错误的代码路径检测为编译错误。严格来说，它们不能帮助您所声明的意图，但它们利用的理论可能对您有用。
2

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

一旦您熟悉了该工具，大多数证明都变得容易。更难的证明会产生有趣的测试用例，有时可以触发现有程序中的bug。(而要找到bug，则可以在确定没有bug需要查找后，将定理作为公理来简化证明过程。)

大约一个月前，我们在解析具有多个/旧版本XREF表的PDF文件时遇到了问题。我们无法证明解析是否终止。考虑到这一点，我构建了一个具有循环/Prev指针的Trailer的PDF文件(谁能想到呢？:-P)，这自然使一些查看器永远循环。(尤其是Ubuntu上的几乎任何基于poppler的查看器。让我笑和诅咒Gnome/evince-thumbnailer吃掉我的所有CPU。不过我认为他们现在已经解决了这个问题。)

使用Coq查找低级别的bug将会很困难。为了证明任何事情，您需要程序行为的模型。对于堆栈/堆问题，您可能需要对CPU级别或至少C级别的执行进行建模。虽然从技术上讲这是可能的，但我认为这不值得这样做。

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

2

STACK和KINT使用约束求解器来查找许多开源项目（如Linux内核和ffmpeg）中的漏洞。 项目页面指向论文和代码。

STACK 论文第 1 页的代码片段是一个看起来非常坚固但实际上并非如此的绝佳例子。它也是一份极好的材料，可以提醒语言标准作者们如何定义“未定义行为”可能会出现意外反效果。 - j_random_hacker
1

这与定理证明实际上没有太大的关系，但模糊测试是一种常见的自动化查找漏洞的技术。

1

有一个L4 verified kernel试图做到这一点。但是，如果您查看攻击历史，就会发现完全新的攻击模式，然后许多软件在那时编写起来很容易受到攻击。例如，格式字符串漏洞直到1999年才被发现。大约一个月前，H.D. Moore发布了DLL劫持，而且在Windows下所有东西都容易受到攻击。

我不认为可以证明一款软件对未知攻击是安全的。至少在定理能够发现此类攻击之前是不可能的，据我所知，这种情况还没有发生。

通过安全性，我认为你指的是在已知硬件上运行的某段代码保持一组不变量。如果是这种情况，我相信可以证明这些不变量成立。随着软件规模的增大，这变得更加困难，但根据我所读到的，我们正在变得更加聪明。 - Jason Kleban
@uosɐſ 让我换个说法，这些年来我写了很多漏洞利用程序，我已经失去了对我发行的CVE编号数量的追踪，而且我认为这是无法证明的。至少目前还不行。 - rook
@uosɐſ 这是未知的问题。如果一个定理能够证明它可以抵御未知，那么就可以使用一个定理来发现先前未知的模式。即使是非常简单的程序，“hello world”，也非常复杂。即使您假设它正在正确执行，也要记住处理器中会发现漏洞。在任何数学证明中，您都必须做出假设，这些证明是否假定处理器正常运行？(http://www.engadget.com/2009/03/19/new-smm-exploit-targets-intel-cpu-caching-vulnerability/) - rook
@uosɐſ：是的，你可以证明在给定的机器上选择的程序不易受到外部攻击。http://en.wikipedia.org/wiki/Cyrix_coma_bug - BCS
@BCS，太令人欣慰了！但我不明白你提到的维基百科参考是什么意思。你能解释一下吗？还是这是讽刺？ - Jason Kleban
显示剩余5条评论
0

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

一些观察

  • 像加密这样的东西很少被“证明”，只是被认为是安全的。如果您的程序使用了这样的东西，它的强度只能与加密本身一样强。
  • 定理证明器无法分析所有内容（否则它们将能够解决停机问题）
  • 您必须非常清楚地定义对于证明者而言什么是不安全的。这本身就是一个巨大的挑战
我不确定这个问题是否百分之百正确，但我非常肯定密码学的大部分已经被证明是基于公理的（特别是随着提出的P！=NP），只是经常被错误地应用。正如你在第三点中指出的那样，重要的是严格定义你所依赖机制的内容——只有这样才能证明你的使用是正确的应用。 - Jason Kleban
@uosɐſ 大部分的密码分析都涉及到减少破解密码/哈希所需的轮数。此外，我相当确定“因式分解是困难的”这一事实尚未被证明（不可靠的来源：http://en.wikipedia.org/wiki/Integer_factorization）。 - cobbal
再次声明，我并非专家，但请您考虑以下内容：整数分解并不是唯一的“困难”机制。此外，最近的P！=NP（待审核）将证明存在困难问题。而且我认为已经证明了如果困难问题存在，那么整数分解或其某些相关问题也属于这一类别。 - Jason Kleban
此外，Byron Cook的链接涉及停机问题。简而言之：是的，停机问题仍然存在，但这只是说，正如您所说，您无法静态分析每个程序以进行终止，但这并不意味着没有各种类型的程序可以进行静态分析以进行终止。 - Jason Kleban
让我想到了静态可分析性和图灵完备性的某种交集，可能已经被探索过了。 - Jason Kleban
显示剩余2条评论
0

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

它在应用程序中。与安全或特殊知识无关的定理证明器本身并没有任何关系。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接