利用定理证明寻找攻击

因此,至少在某种有意义的意义上,证明某个东西是安全的相反方法是找到它不安全的代码路径。

Byron Cook's TERMINATOR project .

9频道至少有两个视频。 Here's one of them

他的研究很可能是你了解这个非常有趣的研究领域的一个很好的起点。

Spec#和类型化汇编语言等项目也是相关的。为了将安全检查的可能性从运行时移回编译时,他们允许编译器将许多错误代码路径检测为编译错误。严格地说,它们无助于你所陈述的意图,但它们利用的理论可能对你有用。

是的,这方面做了很多工作。可满足性(SAT和SMT)求解器经常被用来发现安全漏洞。 例如,在Microsoft中,一个名为 SAGE Z3 theorem prover 作为它的可满足性检查器。 如果您使用诸如智能模糊或白盒模糊之类的关键字搜索互联网,您将发现其他几个项目使用可满足性检查器来查找安全漏洞。 高层次的思想是:收集程序中的执行路径(您没有设法执行这些路径,也就是说,您没有找到使程序执行它的输入),将这些路径转换为数学公式,并将这些公式提供给可满足性解算器。 其思想是创建一个公式,只有当有一个输入将使程序执行给定的路径时,这个公式才是可满足/可行的。

我正在和其他人一起用Coq编写一个PDF解析器。虽然本例的目标是生成一段安全的代码,但这样做肯定有助于发现致命的逻辑错误。

大约一个月前,我们遇到了一个问题:用多个/旧的外部参照表解析PDF。我们无法证明解析终止。考虑到这一点,我在预告片中构建了一个带有循环/Prev指针的PDF(谁会想到这个?:-P),这自然会让一些观众永远循环。(最值得注意的是,几乎所有基于poppler的Ubuntu浏览器。让我大笑,诅咒Gnome/evince thumbnailer吃掉了我所有的CPU。我想他们现在修好了。)

使用Coq查找低级错误将是困难的。为了证明一切,你需要一个程序行为的模型。对于堆栈/堆问题,您可能需要对CPU级或至少是C级执行进行建模。虽然从技术上讲是可能的,但我认为这不值得付出努力。

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

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

这和定理证明没有关系,但是 fuzz testing 是以自动化方式查找漏洞的常用技术。

L4 verified kernel DLL Hijacking 还有窗户下的一切 is vulnerable

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

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

一些观察

• 像密码学这样的东西很少被“证实”,只是被认为是安全的。如果你的程序使用类似的东西,它只会像加密一样强大。
• 定理证明者不能分析所有的东西(或者他们可以解决停顿问题)
• 您必须非常清楚地定义什么是不安全对验证程序意味着什么。这本身就是一个巨大的挑战

对。许多定理证明项目通过演示软件中的漏洞或缺陷来展示软件的质量。为了使它与安全相关,想象一下在安全协议中发现一个漏洞。卡洛斯·奥拉特在乌戈·蒙塔纳里的博士论文就是这样一个例子。

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