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的经过验证的编程语言编写。CVC3解算器还增加了对LFSC校样的支持。这项研究将通过证明大大增加求解器结果的置信度，从而增加漏洞检测的能力。

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.