使用定理证明者寻找攻击
我听说过一些关于使用自动定理证明器来尝试证明软件系统中不存在安全漏洞的消息。一般来说，这是极其困难的。
我的问题是，是否有人使用类似的工具来查找现有或拟议系统中的漏洞？
Eidt：我不是询问如何证明软件系统是安全的。我问的是如何查找（最好是以前未知的）漏洞（甚至是其中的类别）。我在这里思考（但不是）黑帽：描述系统的形式语义，描述我想要攻击的内容，然后让计算机找出我需要使用哪些操作链来接管你的系统。
I've heard a bit about using automated theorem provers in attempts to show that security vulnerabilities don't exist in a software system. In general this is fiendishly hard to do.
My question is has anyone done work on using similar tools to find vulnerabilities in existing or proposed systems?
Eidt: I'm NOT asking about proving that a software system is secure. I'm asking about finding (ideally previously unknown) vulnerabilities (or even classes of them). I'm thinking like (but an not) a black hat here: describe the formal semantics of the system, describe what I want to attack and then let the computer figure out what chain of actions I need to use to take over your system.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（8）
是的，这方面已经做了很多工作。可满足性（SAT 和 SMT）求解器经常用于查找安全漏洞。
例如，在 Microsoft 中，有一个名为 SAGE 用于消除 Windows 中的缓冲区溢出错误。
SAGE 使用 Z3 定理证明器 作为其可满足性检查器。
如果您使用“智能模糊测试”或“白盒模糊测试”等关键字在互联网上搜索，您会发现其他几个使用可满足性检查器来查找安全漏洞的项目。
高级思想如下：收集程序中的执行路径（您没有设法执行的路径，即您没有找到使程序执行它的输入），将这些路径转换为数学公式，并将这些公式输入可满足性求解器。
这个想法是创建一个只有在存在使程序执行给定路径的输入时才可满足/可行的公式。
如果生成的公式是可满足的（即可行的），则可满足性求解器将生成分配和所需的输入值。白盒模糊器使用不同的策略来选择执行路径。
主要目标是找到一个输入，使程序执行导致崩溃的路径。
Yes, a lot of work has been done in this area. Satisfiability (SAT and SMT) solvers are regularly used to find security vulnerabilities.
For example, in Microsoft, a tool called SAGE is used to eradicate buffer overruns bugs from windows.
SAGE uses the Z3 theorem prover as its satisfiability checker.
If you search the internet using keywords such as “smart fuzzing” or “white-box fuzzing”, you will find several other projects using satisfiability checkers for finding security vulnerabilities.
The high-level idea is the following: collect execution paths in your program (that you didn't manage to exercise, that is, you didn't find an input that made the program execute it), convert these paths into mathematical formulas, and feed these formulas to a satisfiability solver.
The idea is to create a formula that is satisfiable/feasible only if there is an input that will make the program execute the given path.
If the produced formula is satisfiable (i.e., feasible), then the satisfiability solver will produce an assignment and the desired input values. White-box fuzzers use different strategies for selecting execution paths.
The main goal is to find an input that will make the program execute a path that leads to a crash.
因此，至少在某种意义上，证明某些东西安全的反面是找到不安全的代码路径。
尝试Byron Cook 的 TERMINATOR 项目。
Channel9 上至少有两个视频。 这是其中之一
他的研究很可能是您了解这个极其有趣的研究领域的良好起点。
Spec# 和 Typed-Assembly-Language 等项目也相关。为了将安全检查的可能性从运行时移回编译时，它们允许编译器将许多错误的代码路径检测为编译错误。严格来说，它们并不能帮助你实现既定的意图，但它们所利用的理论可能对你有用。
So, at least in some meaningful sense, the opposite of proving something is secure is finding code paths for which it isn't.
Try Byron Cook's TERMINATOR project.
And at least two videos on Channel9. Here's one of them
His research is likely to be a good starting point for you to learn about this extremely interesting area of research.
Projects such as Spec# and Typed-Assembly-Language are related too. In their quest to move the possibility of safety checks from runtime back to compile-time, they allow the compiler to detect many bad code paths as compilation errors. Strictly, they don't help your stated intent, but the theory they exploit might be useful to you.
我目前正在与其他人一起用 Coq 编写 PDF 解析器。虽然本例的目标是生成一段安全的代码，但这样做肯定有助于发现致命的逻辑错误。
一旦您熟悉了该工具，大多数证明就会变得容易。更难的证明会产生有趣的测试用例，有时会触发真实的现有程序中的错误。 （为了查找错误，一旦确定没有错误可发现，您就可以简单地将定理假设为公理，无需进行认真的证明。）
大约一个月前，我们在使用多个/较旧的 XREF 表解析 PDF 时遇到了问题。我们无法证明解析已终止。考虑到这一点，我在预告片中构建了一个带有循环 /Prev 指针的 PDF（谁会想到这一点？:-P），这自然会让一些观众永远循环。 （最值得注意的是，Ubuntu 上几乎所有基于 poppler 的查看器。让我大笑并诅咒 Gnome/evince-thumbnailer 吃掉了我所有的 CPU。我想他们现在修复了它。）
使用 Coq 来查找较低级别的错误将是难的。为了证明任何事情，您需要程序行为的模型。对于堆栈/堆问题，您可能必须对 CPU 级或至少 C 级执行进行建模。虽然技术上可行，但我认为这不值得付出努力。
使用 C 语言的 SPLint 或用您选择的语言编写自定义检查器应该会更有效。
I'm currently writing a PDF parser in Coq together with someone else. While the goal in this case is to produce a secure piece of code, doing something like this can definitely help with finding fatal logic bugs.
Once you've familiarized yourself with the tool, most proof become easy. The harder proofs yield interesting test cases, that can sometimes trigger bugs in real, existing programs. (And for finding bugs, you can simply assume theorems as axioms once you're sure that there's no bug to find, no serious proving necessary.)
About a moth ago, we hit a problem parsing PDFs with multiple / older XREF tables. We could not prove that the parsing terminates. Thinking about this, I constructed a PDF with looping /Prev Pointers in the Trailer (who'd think of that? :-P), which naturally made some viewers loop forever. (Most notably, pretty much any poppler-based viewer on Ubuntu. Made me laugh and curse Gnome/evince-thumbnailer for eating all my CPU. I think they fixed it now, tho.)
Using Coq to find lower-level bugs will be difficult. In order to prove anything, you need a model of the program's behavior. For stack / heap problems, you'll probably have to model the CPU-level or at least C-level execution. While technically possible, I'd say this is not worth the effort.
Using SPLint for C or writing a custom checker in your language of choice should be more efficient.
STACK 和 KINT 使用约束求解器来查找许多 OSS 项目中的漏洞，例如 Linux 内核和 ffmpeg。项目页面指向论文和代码。
STACK and KINT used constraint solvers to find vulnerabilities in many OSS projects, like the linux kernel and ffmpeg. The project pages point to papers and code.
它与定理证明并不真正相关，但模糊测试是一种用于查找漏洞的常用技术一种自动化的方式。
It's not really related to theorem-proving, but fuzz testing is a common technique for finding vulnerabilities in an automated way.
L4 验证内核 正试图做到这一点。但是，如果您查看利用历史，就会发现全新的攻击模式，并且在此之前编写的许多软件非常容易受到攻击。例如，格式字符串漏洞直到 1999 年才被发现。大约一个月前，HD Moore 发布了 DLL 劫持 以及 Windows 下的所有内容 容易受到攻击。
我认为不可能证明一个软件能够安全地抵御未知的攻击。至少在定理能够发现这种攻击之前不会，据我所知这还没有发生。
There is the L4 verified kernel which is trying to do just that. However, if you look at the history of exploitation, completely new attack patterns are found and then a lot of software written up to that point is very vulnerable to attacks. For instance, format string vulnerabilities weren't discovered until 1999. About a month ago H.D. Moore released DLL Hijacking and literally everything under windows is vulnerable.
I don't think its possible to prove that a piece of software is secure against an unknown attack. At least not until a theorem is able to discover such an attack, and as far as I know this hasn't happened.
免责声明：我对自动定理证明者几乎没有经验
一些观察
Disclaimer: I have little to no experience with automated theorem provers
A few observations
是的。许多定理证明项目通过展示软件中的漏洞或缺陷来展示其软件的质量。为了使其与安全相关，想象一下在安全协议中发现一个漏洞。卡洛斯·奥拉特博士Ugo Montanari 的论文就有一个这样的例子。
它在应用程序中。定理证明本身并不是与安全性或特殊知识有关的。
Yes. Many theorem proving projects show the quality of their software by demonstrating holes or defects in software. To make it security related, just imagine finding a hole in a security protocol. Carlos Olarte's Ph.D. thesis under Ugo Montanari has one such example.
It is in the application. Not really the theorem prover itself that has anything to do with security or special knowledge thereof.