security - 使用定理证明器发现攻击

Question

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

我的问题是有人做过使用类似工具来查找现有或提议系统中的漏洞的工作吗？

艾特:我是 不是 询问如何证明软件系统是安全的。我问的是寻找(最好是以前未知的)漏洞(甚至是它们的类别)。我在想(但不是)这里的黑帽子:描述系统的形式语义，描述我想要攻击的内容，然后让计算机找出我需要使用哪些操作链来接管您的系统。

Answer 1

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

试试 Byron Cook's TERMINATOR project .

Channel9 上至少有两个视频。 Here's one of them

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

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