SHF: Small:Collaborative Research: Flexible, Efficient, and Trustworthy Proof Checking for Satisfiability Modulo Theories

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。软件漏洞每年给美国经济造成的损失超过600亿美元。有前途的错误检测技术依赖于可满足模理论（SMT）的高性能逻辑求解器，它采用复杂的算法来有效地检查大型公式。复杂是有代价的：解决方案本身会出现错误，而且对于安全关键型应用程序来说不够可信。为了增加信心，一些SMT求解器可以对有效公式给出形式化的证明。用一个简单的证明检查器检查这些证明，确认解算器的结果。SMT丰富的逻辑为标准化所有SMT解算器的单一证明格式提出了挑战。此外，SMT求解器生成的证明可能长达千兆字节，需要优化的证明检查器。该合作项目正在开发一种经过验证的证明检查器，支持一种称为带侧条件的爱丁堡逻辑框架（LFSC）的灵活格式。LFSC是描述不同证明系统的元语言，因此提供了灵活性。验证技术被应用于证明检查器本身，通过使用一种被称为Guru的经过验证的编程语言编写来验证其优化。支持LFSC证明也被添加到ccv3求解器中。本研究将通过证明大大提高求解器结果的可信度，从而提高bug检测的能力。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).Software bugs cost the U.S. economy over $60 billion each year. Promising bug-detection technology depends on high-performance logic solvers for Satisfiability Modulo Theories (SMT), which employ sophisticated algorithms to check large formulas efficiently. Sophistication has a price: the solvers themselves exhibit bugs, and are not trustworthy enough for safety-critical applications. To increase confidence, some SMT solvers can emit formal proofs for valid formulas. Checking these proofs with a simple proof checker confirms the solver's results. SMT's rich logic poses challenges for standardizing a single proof format for all SMT solvers. Furthermore, proofs produced by SMT solvers can be gigabytes long, requiring an optimized proof checker. This collaborative project is developing a verified proof checker supporting a flexible format called the Edinburgh Logical Framework with Side Conditions (LFSC). LFSC is a meta-language for describing different proof systems, thus providing flexibility. Verification techniques are being applied to the proof checker itself to verify its optimizations, by writing it in a verified programming language called Guru. Support is also being added for LFSC proofs to the CVC3 solver. This research will greatly increase confidence in solver results through proofs, thus increasing the power of bug detection.