TWC: Medium: Collaborative: Breaking the Satisfiability Modulo Theories (SMT) Bottleneck in Symbolic Security Analysis

TWC：媒介：协作：打破符号安全分析中的可满足性模理论 (SMT) 瓶颈

• 批准号: 1228827
• 负责人: David Brumley
• 金额: $ 39.2万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1228827&HistoricalAwards=false
• 关键词: TWC; Medium; Collaborative; Breaking; Satisfiability

The security of our software is critical for consumer confidence, the protection of privacy and valuable intellectual property, and of course national security. Because of our society's increased reliance on software, security breaches can lead to serious personal or corporate losses, and endanger the privacy, liberties, and even the lives of individuals. As threats to software security have become more sophisticated, so too have the techniques and analyses developed to improve it. Symbolic execution has emerged as a fundamental tool for security applications. Its main idea is to run a program using symbolic instead of concrete values: a set of symbols are assigned to the program inputs, and the outputs are expressed as a set of "verification conditions", logical formulas over the input symbols. A number of successful security analyses use symbolic execution and similar methods to recast security questions about programs as constraint satisfaction problems in some formal logic. Automatic reasoners for that logic can then be used to solve those problems. In the last few years, solvers based on Satisfiability Modulo Theories (SMT) techniques have become a natural choice in such approaches to security because of their superior performance and automation compared to more traditional theorem provers and their greater generality with respect to ad-hoc tools or propositional satisfiability solvers.This collaborative project brings together experts in security and in SMT to pursue two complementary research goals: (i) harness the full power of SMT solvers to improve current security tools based on symbolic analysis; and (ii) design and develop new techniques to address the needs of anticipated future security applications. Specific activities addressing these goals include: collecting challenge benchmark problems from existing security analyses and developing targeted SMT optimizations for these benchmarks; developing appropriate security abstractions in the SMT language used to express security verification conditions; developing logical theories and algorithms for reasoning about character strings in such verification conditions; exposing a general framework for extending the verification condition language; and developing techniques for computing symbolic solution sets for SMT constraints. These activities are expected to (i) significantly increase the flexibility, performance, and reasoning capabilities of SMT solvers in support of security applications; (ii) improve the performance and scalability of current security analyses by leveraging the reasoning power of SMT solvers; and (iii) provide a foundation for new, more powerful, and more expressive security analyses. Overall, this project will help create more scalable and expressive security applications which could have a considerable impact on society as they enable the production of software much more resistant to security attacks.

我们软件的安全对于消费者的信心，保护隐私和有价值的知识产权以及当然是国家安全至关重要。由于我们社会对软件的依赖越来越依赖，因此安全漏洞会导致严重的个人或公司损失，并危害个人的隐私，自由甚至个人的生命。随着对软件安全性的威胁变得越来越复杂，可以改善它的技术和分析。符号执行已成为安全应用程序的基本工具。它的主要思想是使用符号而不是具体值运行程序：将一组符号分配给程序输入，输出表示为一组“验证条件”，在输入符号上表达了逻辑公式。 许多成功的安全性分析都使用符号执行和类似的方法来将有关程序的安全性问题作为某些正式逻辑中的约束满意度问题。然后可以使用该逻辑的自动推理器来解决这些问题。 在过去的几年中，基于满足性模型理论（SMT）技术的求解器已成为这种安全方法的自然选择，因为它们的性能和自动化较高，而与更传统的定理抛弃相比，其更大的一般性及其在宣传工具或求主的可满足性解决方案方面的更大一般性，这是在SMET方面的专家，以提高SMT的专家，以提高SMT的专家，以实现互补的研究（I）（I）（I）（I）（I）（I）（I）（I）（I）（I）（I）（I）基于符号分析的工具； （ii）设计和开发新技术，以满足预期的未来安全应用程序的需求。解决这些目标的具体活动包括：从现有的安全分析中收集挑战基准问题，并为这些基准制定有针对性的SMT优化；用用于表达安全验证条件的SMT语言开发适当的安全摘要；在此类验证条件下开发逻辑理论和算法来推理字符字符串；公开一个通用框架以扩展验证条件语言；并开发用于计算SMT约束的符号解决方案集的技术。预计这些活动将（i）大大提高SMT求解器的灵活性，性能和推理能力，以支持安全应用程序； （ii）通过利用SMT求解器的推理能力来提高当前安全性分析的性能和可扩展性； （iii）为新的，更强大，更具表现力的安全分析提供了基础。总体而言，该项目将有助于创建更可扩展和表现力的安全应用程序，这可能会对社会产生重大影响，因为它们能够生产软件对安全攻击的抵抗力。