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

我们软件的安全对消费者信心、隐私和宝贵知识产权的保护至关重要，当然对国家安全也是如此。由于我们的社会越来越依赖软件，安全漏洞可能会导致严重的个人或公司损失，并危及隐私、自由，甚至个人的生命。随着对软件安全的威胁变得更加复杂，为改进它而开发的技术和分析也变得更加复杂。符号执行已经成为安全应用程序的基本工具。它的主要思想是使用符号而不是具体的值来运行程序：一组符号被分配给程序输入，而输出被表示为一组“验证条件”，即在输入符号上的逻辑公式。许多成功的安全分析使用符号执行和类似的方法将程序的安全问题重塑为某些形式逻辑中的约束满足问题。然后，可以使用该逻辑的自动推理器来解决这些问题。在过去的几年里，基于可满足性模理论(SMT)技术的求解器已经成为此类安全方法的必然选择，因为与更传统的定理证明器相比，SMT技术具有更好的性能和自动化，并且相对于自组织工具或命题可满足性求解器具有更大的通用性。这个合作项目汇集了安全领域和SMT领域的专家，以追求两个互补的研究目标：(I)利用SMT求解器的全部能力来改进现有的基于符号分析的安全工具；(Ii)设计和开发新的技术来满足预期的未来安全应用的需求。解决这些目标的具体活动包括：从现有的安全分析中收集挑战基准问题，并为这些基准开发有针对性的SMT优化；用SMT语言开发用于表示安全验证条件的适当安全抽象；开发关于此类验证条件中的字符串的推理的逻辑理论和算法；揭示扩展验证条件语言的一般框架；以及开发用于计算SMT约束的符号解决方案集的技术。这些活动预计将(I)显著提高SMT求解器在支持安全应用程序方面的灵活性、性能和推理能力；(Ii)通过利用SMT求解器的推理能力，提高当前安全分析的性能和可扩展性；以及(Iii)为新的、更强大和更具表现力的安全分析提供基础。总体而言，该项目将有助于创建更具伸缩性和表现力的安全应用程序，这些应用程序可能会对社会产生相当大的影响，因为它们使软件的生产能够更好地抵御安全攻击。

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.