CT-T: Practical Formal Verification By Specification Extraction

对一个系统的信任在很多地方都会受到损害。人们对制定值得信赖的要求和政策进行了广泛的研究，但这些要求和政策只有在正确执行的情况下才有效。通过测试来确保没有实现缺陷是不够的;测试不可能是详尽的，因此可能会遗漏关键的漏洞。正式验证？证明系统正确地实现了其规范并执行了其策略？是一个有吸引力的选择。形式验证的标准方法是强大的，但经验表明，使用它们具有挑战性。规范语言无法描述完整的系统，功能有限的工具无法集成，验证技术难以应用且耗时，验证需要高水平的专业知识。当前的方法还对开发人员施加了限制，使得正式验证难以融入开发周期。我们的方法Echo是一种正式软件验证的新方法，使此类验证易于使用、适用、具有成本效益并且对有需要的社区有用。我们方法的基础与传统方法形成鲜明对比，是转换程序，从低级规范中提取高级规范，并证明它隐含原始规范。所需的分析分为一个强大的通用定理证明系统和一个低级验证系统。Echo将提高重要计算机应用程序的安全性和其他方面的可靠性，从而减少安全攻击和其他故障造成的损失。

Trust in a system can be compromised in many places. Extensive research has been conducted on the development of trustworthy requirements and policies, but those requirements and policies are effective only if they are carried out correctly. Ensuring the absence of implementation flaws by testing is inadequate; testing cannot be exhaustive and thus can miss critical vulnerabilities. Formal verification?proof that the system correctly implements its specification and enforces its policies?is an attractive alternative. Standard approaches to formal verification are powerful, but experience has shown them to challenging to use. Specification languages fail to describe complete systems, tools with limited capabilities cannot be integrated, verification techniques are difficult and time consuming to apply, and verification requires high levels of expertise. Current approaches also impose limitations on developers that make it difficult to fit formal verification into the development cycle.Our approach, Echo, is a new approach to formal software verification that makes such verification readily available, applicable, cost effective, and useful to the community that needs it. The basis of our approach, in stark contrast to traditional methods, is to transform the program, extract a high-level specification from a low-level one, and prove that it implies the original specification. The required analysis is split between a powerful general-purpose theorem-proving system and a low-level verification system.Echo will improve security and other facets of dependability in important computer applications thereby reducing losses resulting from security attacks and other failures.