Geometric Abstractions for Scalable Program Analyzers

人们普遍认为，软件中相对较小的缺陷可能会给生产者和消费者带来巨大的成本。例如，编程错误经常导致系统漏洞，如允许对缓冲区的越界访问、本机整数操作中的溢出以及与内存管理相关的其他错误。当然，可能还有其他原因，如系统设计缺陷，但找到并证明没有低级错误是构建安全可靠的软件的重要前提。我们用来检测和定位编程错误或证明没有这样的错误的方法是静态分析的方法；也就是说，确定关于每个程序步骤的程序值的正确而近似的信息。静态分析植根于编译器优化，其中分析时间必须保持在非常低的水平，而感兴趣的属性相对于编译器是固定的。最近已经开发了用于程序验证的程序分析器；然而，这些分析器也考虑可能的运行时错误的固定集合，并以使它们能够处理非常大的程序的可扩展性和性能为目标。静态分析使用抽象域来表示需要收集的信息。因此，这些域必须提供在程序的抽象评估期间积累的信息的方便但近似的表示。观察到，静态分析器的抽象域组件不仅必须包括感兴趣的逻辑属性的计算机表示，而且还必须包括从程序的组件中提取该信息所需的操作、用于在程序内向前和/或向后传播该信息的原语、以及用于加速分析过程和确保循环迭代实际终止的运算符。问题是要在效率/精度之间取得适当的平衡，这是很困难的，因为这显然取决于应用程序。因此，人们提出并研究了许多几何域，其中大多数是由线性(即平面)边界定义的，如多面体、八角形、长方体(也称为间隔)和网格(其简单形式也称为网格)。这样的范围是需要的，因为像多面体这样的域虽然非常精确，但具有高的复杂性和指数级的空间要求(相对于维度的数量)，而更简单的域如八角形和网格是多项式的，而非相关的长方体域具有线性复杂性。解决这个可伸缩性问题是本项目的主要动机；在这里，我们将研究新的技术来构建可以由几个原子域构造的复合几何域，例如上面讨论的那些。为了能够改变效率/精度之间的权衡，它不仅将在组件域上参数化，而且还将具有高度可调的策略，用于改变它们之间的通信类型和通信量。因此，一个成功的项目将提供为应用程序量身定做的域，允许验证属性的类型以及分析软件的大小和复杂性。

It is widely acknowledged that relatively small defects in software can have a substantial cost both for producers and consumers. For example, system vulnerabilities are frequently introduced by programming mistakes such as allowing out of bounds accesses to buffers, overflows in operations on native integers and other errors related to memory management. Of course, there can be other causes, such as system design flaws, but finding and certifying the absence of the low-level bugs is an important prerequisite to building secure and reliable software. The approach we use to detect and locate programming errors or certify the absence of such bugs is that of static analysis; that is, the determination of correct though approximate information about the program's values at each program step. Static analysis has its roots in compiler optimization where the analysis time has to be kept very low while the properties of interest are fixed with respect to the compiler. More recently program analyzers have been developed for program verification; however these also consider a fixed set of possible run-time errors and aim for a scalability and performance that enables them to tackle very large programs.Static analysis uses abstract domains for representing information that needs to be collected. Thus these domains have to provide a convenient but approximate representation of the accumulated information during the abstract evaluation of a program. Observe that the abstract domain component of a static analyzer has to include, not only a computer representation of the logical properties of interest, but also the operations needed to extract this information from the program's components, primitives for propagating this information forward and/or backward within the program, and operators for accelerating the analysis process and ensuring loop iterations actually terminate.Since, many program properties of interest are intrinsically numeric, there has been a considerable amount of research on how this kind of information can be represented efficiently and precisely by means of geometric domains. The problem being to get the right efficiency/precision trade-off, which is difficult since this is clearly dependent on the application. Thus many geometric domains have been proposed and researched, the majority being defined by linear (i.e., planar) bounds such as polyhedra; octagons; boxes, also known as intervals; and grids, simple forms of which are also called lattices. Such a range is needed since domains such as polyhedra, although very precise, have high complexity and exponential space requirements (relative to the number of dimensions) while simpler domains such as octagons and grids are polynomial and the non-relational domain of boxes has linear complexity.Solving this scalability problem is the main motivation for this project; here we will research new techniques for building compound geometric domains that can be constructed from several atomic ones such as those discussed above. In order to allow for varying the efficiency/precision trade-off, not only will it be parametrized on the component domains but it will also have a highly adjustable strategy for varying the kind and amount of communication between them. Thus a successful project will provide bespoke domains that are tailored for the application, allowing for both the type of property being verified and the size and complexity of the software being analyzed.