Geometric Abstractions for Scalable Program Analyzers

可扩展程序分析器的几何抽象

• 批准号: EP/G025177/1
• 负责人: Anthony Cohn
• 金额: $ 6.53万
• 依托单位: University of Leeds
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2008
• 资助国家: 英国
• 起止时间: 2008 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FG025177%2F1
• 关键词: Geometric; Abstractions; 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.

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

项目成果

Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness

• DOI: 10.1007/s10703-009-0073-1
• 发表时间: 2009-12
• 期刊: Formal Methods in System Design
• 影响因子: 0.8
• 作者: Roberto Bagnara;P. Hill;E. Zaffanella

Time-lapse geophysical investigations over known archaeological features using electrical resistivity imaging and earth resistance

使用电阻率成像和接地电阻对已知考古特征进行延时地球物理调查

• 发表时间: 2014
• 作者: Fry Robert James

Assessment of the CMD Mini-Explorer, a New Low-frequency Multi-coil Electromagnetic Device, for Archaeological Investigations

• DOI: 10.1002/arp.1458
• 发表时间: 2013-07-01
• 期刊: ARCHAEOLOGICAL PROSPECTION
• 影响因子: 1.8
• 作者: Bonsall, James;Fry, Robert;Gaffney, Vince
• 通讯作者: Gaffney, Vince