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

我们软件的安全性对消费者信心、保护隐私和宝贵的知识产权，当然还有国家安全都至关重要。由于我们的社会越来越依赖软件，安全漏洞可能导致严重的个人或公司损失，并危及隐私，自由，甚至个人的生命。随着对软件安全的威胁变得越来越复杂，改进它的技术和分析也越来越成熟。符号执行已经成为安全应用程序的基本工具。它的主要思想是使用符号而不是具体值来运行程序：将一组符号分配给程序输入，并将输出表示为一组“验证条件”，即输入符号上的逻辑公式。许多成功的安全性分析使用符号执行和类似的方法将有关程序的安全性问题重新定义为某种形式逻辑中的约束满足问题。这种逻辑的自动推理器可以用来解决这些问题。在过去的几年中，基于可满足模理论（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.