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

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

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.