Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution

使用动态符号执行测试、验证和生成软件补丁

• 批准号: EP/J00636X/1
• 负责人: Cristian Cadar
• 金额: $ 36.59万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2012
• 资助国家: 英国
• 起止时间: 2012 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FJ00636X%2F1
• 关键词: Testing; Verifying; Generating; Software; Patches

A large fraction of the costs of developing and maintaining software is associated with detecting and fixing software errors. As a result, the last decade has seen a sustained research effort directed toward designing and developing techniques for automatically detecting software errors, with some of these techniques making their way into commercial and open-source tools. However, detecting an error is only the first step toward fixing it. In fact, many known errors remain unpatched due to the high cost required to diagnose and repair them, combined with the fear that patches are more likely to introduce failures compared to other types of code changes.The goal of this research project is to address both of these problems, by devising novel techniques based on dynamic symbolic execution for:(1) automatically testing and verifying the correctness of software patches, and(2) (semi-)automatically generating candidate patches for software bugs.The strength of dynamic symbolic execution lies in its ability to precisely model the behaviour of program paths using mathematical constraints. However, the cost associated with this level of precision is poor scalability. The number of paths in a program is usually exponential in the number of branches, which makes it difficult to scale the analysis to very large programs. However, by focusing the analysis on the incremental changes introduced by program patches, we hope to significantly reduce the cost of symbolic execution and significantly increase its applicability in practice. Furthermore, the ability to check software patches opens up the possibility of performing patch generation in an automatic or semi-automatic fashion. In particular, starting from the mathematical constraints gathered from a buggy execution path -- and with the potential addition of a manually-written patch template -- we plan to design techniques for generating a set of candidate patches resembling the ones that would be generated manually by developers.

开发和维护软件的大部分成本与检测和修复软件错误有关。因此，在过去的十年中，人们一直在努力设计和开发自动检测软件错误的技术，其中一些技术已经进入商业和开源工具。然而，检测错误只是修复错误的第一步。事实上，许多已知的错误仍然没有修补，因为诊断和修复它们所需的成本很高，加上担心与其他类型的代码更改相比，补丁更有可能引入故障。本研究项目的目标是通过设计基于动态符号执行的新技术来解决这两个问题：（1）自动测试和验证软件补丁的正确性，以及（2）（半）自动地生成软件错误的候选补丁。动态符号执行的优势在于它能够使用数学约束精确地建模程序路径的行为。然而，与这种精度水平相关联的成本是较差的可扩展性。程序中的路径数通常是分支数的指数，这使得很难将分析扩展到非常大的程序。然而，通过集中分析程序补丁引入的增量变化，我们希望显着降低符号执行的成本，并显着增加其在实践中的适用性。此外，检查软件补丁的能力开启了以自动或半自动方式执行补丁生成的可能性。特别是，从一个错误的执行路径收集的数学约束开始-并有可能添加一个手动编写的补丁模板-我们计划设计技术来生成一组候选补丁类似于那些将由开发人员手动生成。

项目成果

Covrig: a framework for the analysis of code, test, and coverage evolution in real software

Covrig：用于分析实际软件中的代码、测试和覆盖率演变的框架

• DOI: 10.1145/2610384.2610419
• 发表时间: 2014
• 作者: Marinescu P

Shadow Symbolic Execution for Testing Software Patches

用于测试软件补丁的影子符号执行

• DOI: 10.1145/3208952
• 发表时间: 2018
• 期刊: ACM Transactions on Software Engineering and Methodology
• 影响因子: 4.4
• 作者: Kuchta T

Shadow symbolic execution for better testing of evolving software

影子符号执行可以更好地测试不断发展的软件

• DOI: 10.1145/2591062.2591104
• 发表时间: 2014
• 作者: Cadar C

make test-zesti: A symbolic execution solution for improving regression testing

• DOI: 10.1109/icse.2012.6227146
• 发表时间: 2012-06
• 期刊: 2012 34th International Conference on Software Engineering (ICSE)
• 作者: P. Marinescu;Cristian Cadar