我听说过使用自动定理证明器来尝试证明软件系统中不存在安全漏洞。一般来说,这是非常困难的。
我的问题是,是否有人在使用类似的工具来发现现有或提议的系统中的漏洞?
编辑:我不是在询问如何证明软件系统的安全性。我是在询问如何发现(理想情况下是以前未知的)漏洞(甚至是漏洞类别)。我像黑客那样思考:描述系统的形式语义,描述我要攻击的目标,然后让计算机找出我需要使用哪些行动链路来接管你的系统。
我听说过使用自动定理证明器来尝试证明软件系统中不存在安全漏洞。一般来说,这是非常困难的。
我的问题是,是否有人在使用类似的工具来发现现有或提议的系统中的漏洞?
编辑:我不是在询问如何证明软件系统的安全性。我是在询问如何发现(理想情况下是以前未知的)漏洞(甚至是漏洞类别)。我像黑客那样思考:描述系统的形式语义,描述我要攻击的目标,然后让计算机找出我需要使用哪些行动链路来接管你的系统。
在这个领域已经做了很多工作。可满足性(SAT和SMT)求解器通常用于查找安全漏洞。 例如,在微软公司中,一个名为SAGE的工具被用来从Windows中消除缓冲区溢出漏洞。 SAGE使用Z3定理证明器作为其可满足性检查器。 如果您使用“smart fuzzing”或“white-box fuzzing”等关键词在互联网上搜索,您会发现还有其他几个项目使用可满足性检查器来查找安全漏洞。 高层次的想法是:收集程序中的执行路径(即您无法激活的路径,也就是说,您没有找到使程序执行该路径的输入),将这些路径转换成数学公式,并将这些公式提供给可满足性求解器。 目的是创建一个仅在存在输入使程序执行给定路径时才能满足/可行的公式。 如果生成的公式是可满足的(即可行的),则可满足性求解器将生成赋值和所需的输入值。白盒模糊测试器使用不同的策略选择执行路径。 主要目标是找到一个输入,使程序执行导致崩溃的路径。
我目前正在与其他人一起使用Coq编写PDF解析器。虽然这种情况下的目标是生成一个安全的代码,但像这样做肯定有助于发现致命的逻辑错误。
一旦您熟悉了该工具,大多数证明都变得容易。更难的证明会产生有趣的测试用例,有时可以触发现有程序中的bug。(而要找到bug,则可以在确定没有bug需要查找后,将定理作为公理来简化证明过程。)
大约一个月前,我们在解析具有多个/旧版本XREF表的PDF文件时遇到了问题。我们无法证明解析是否终止。考虑到这一点,我构建了一个具有循环/Prev指针的Trailer的PDF文件(谁能想到呢?:-P),这自然使一些查看器永远循环。(尤其是Ubuntu上的几乎任何基于poppler的查看器。让我笑和诅咒Gnome/evince-thumbnailer吃掉我的所有CPU。不过我认为他们现在已经解决了这个问题。)
使用Coq查找低级别的bug将会很困难。为了证明任何事情,您需要程序行为的模型。对于堆栈/堆问题,您可能需要对CPU级别或至少C级别的执行进行建模。虽然从技术上讲这是可能的,但我认为这不值得这样做。
使用C语言的SPLint或编写自定义检查器应该更有效。
有一个L4 verified kernel试图做到这一点。但是,如果您查看攻击历史,就会发现完全新的攻击模式,然后许多软件在那时编写起来很容易受到攻击。例如,格式字符串漏洞直到1999年才被发现。大约一个月前,H.D. Moore发布了DLL劫持,而且在Windows下所有东西都容易受到攻击。
我不认为可以证明一款软件对未知攻击是安全的。至少在定理能够发现此类攻击之前是不可能的,据我所知,这种情况还没有发生。
免责声明:我几乎没有使用自动定理证明器的经验
一些观察
是的。许多定理证明项目通过展示软件中的漏洞或缺陷来展示其软件的质量。要使其与安全相关,只需想象在安全协议中发现漏洞即可。Carlos Olarte在Ugo Montanari的博士论文中就有这样一个例子。
它在应用程序中。与安全或特殊知识无关的定理证明器本身并没有任何关系。