Scalable Program Analysis for Software Verification

近年来，基于程序分析(抽象解释)的进步，自动程序验证出现了复兴。微软的静态驱动程序验证器等工具可以自动验证程序组件之间接口的某些轻量级属性(例如，协议属性)。然而，存在一个根本问题：可扩展的方法缺乏。当前的工具基于封闭的世界假设，其中有完整的程序可用，并且它们在系统的整个全局状态下工作。这种模块化的缺乏阻碍了可扩展性和更广泛的适用性。本研究针对可伸缩性问题提出了一种新的解决方法，即从本地化、隔离化和泛化三个方向进行分析，前两个方向的思想是为了减少对每个组件进行一次分析的成本，而第三个方向的目的是确保一个程序组件的一个分析结果可以在多个不同的上下文中重用。我们将开发一个通用的框架和具体的分析实例来实现这三个目标。我们将通过开发原型工具来测试我们的想法，我们将应用于广泛使用的开源基础设施软件，如网络软件和操作系统组件。可伸缩性是软件自动验证的核心问题。本研究中这些问题的成功将对使用自动化技术分析和验证重要的真实世界代码产生重大影响。

Recent years have seen a renaissance in automatic program verification, based on advances in program analysis (abstract interpretation).Tools such as Microsoft's Static Driver Verifiercan automatically verify certain lightweight properties (e.g., protocol properties)of interfaces between program components.There is, though, a fundamental problem:Scalable methods are lacking.Current tools are based on a closed world assumption,where a complete program is available,and they work over a system's entire global state.This lack of modularity impedes scalability, and wider applicability. This research proposes an attack on the scalability problem.Our thesis is that progress in three directions, localization,isolation and generalization, can lead to much more scalable analyses.The idea of the first two of these isto reduce the cost for analyzing each component once,while the third aims to ensure thatone analysis result of a program component can be reused in manydifferent contexts. We will develop a general framework and concreteinstances of analyses that achieve these three goals.We will test our ideas by developing prototype toolsthat we will apply to widely-used open-source infrastructure software,such as network software and operating system components.Scalability is the core problem in the automatic verification of software.Success on the problems in this research would have a majorimpact on the use of automatic techniques for theanalysis and verification of significant, real-world code.