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

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

• 批准号: 1228765
• 负责人: Cesare Tinelli
• 金额: $ 39.77万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1228765&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）技术的求解器已经成为安全方法的自然选择，因为与更传统的定理证明器相比，SMT技术具有上级性能和自动化程度，并且与ad-hoc工具或命题可满足性求解器相比具有更大的通用性。这个合作项目汇集了安全和SMT领域的专家，以实现两个互补的研究目标：（i）利用SMT求解器的全部功能来改进基于符号分析的当前安全工具;以及（ii）设计和开发新技术以满足预期的未来安全应用的需求。为实现这些目标而开展的具体活动包括：从现有安全分析中收集挑战性基准问题，并为这些基准制定有针对性的SMT优化方案;用SMT语言制定适当的安全抽象，用于表达安全验证条件;制定逻辑理论和算法，用于在此类验证条件下对字符串进行推理;公布一个通用框架，用于扩展验证条件语言;以及开发用于计算SMT约束的符号解集的技术。这些活动预计将（i）显着提高灵活性，性能和推理能力的SMT求解器，以支持安全应用程序;（ii）提高性能和可扩展性，目前的安全分析，通过利用SMT求解器的推理能力;和（iii）提供一个新的，更强大的，更有表现力的安全分析的基础。总的来说，该项目将有助于创建更具可扩展性和表现力的安全应用程序，这可能对社会产生相当大的影响，因为它们使软件的生产更能抵抗安全攻击。