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.