Verifikation der Speicherhandhabung in bestehenden C Programmen mit numerischen abstrakten Domänen.

长期以来，基于规范和按合同设计的正式方法一直被认为是构建可靠软件的一种方法。然而，这种方法的成本和大量的遗留代码引发了对现有软件产品的自动分析的大量研究，这些产品没有相应的规范。由于缺乏完整的程序专用规范，分析器最多只能断言不存在某些运行时错误，因为构成运行时错误的是由执行环境定义的(如C语言规范所描述的)。有趣的是，消除运行时错误已经根除了允许在外部主机上执行任意代码的最严重的安全漏洞，因为这些漏洞基于利用应用程序中不正确的内存管理，这通常会导致运行时错误。因此，建议的研究项目旨在构建一个可伸缩的分析器，该分析器足够精确，可以证明传统C软件中没有内存管理错误。该项目遵循两条线索：首先，寻求检查可执行代码的新技术，这些技术将简化对封闭源代码软件的分析，并允许对并发原语的分析。其次，该项目研究了结合了形状分析和数值分析的新的高级抽象。然后将这些抽象应用于函数，从而实现上下文敏感分析，而无需为每个调用点重复分析。

Formal methods based on specifications and design-by-contract have long been advocated as a way to build reliable software. However, the cost of this approach and the sheer amount of legacy code has triggered much research into the automatic analysis of existing software products for which no specification exists. Given the lack of a full, program-specific specification, an analyzer can at most assert the absence of certain run-time errors since what constitutes a run-time error is defined by the execution environment (as described by, e.g., the C language specification). Interestingly, eliminating run-time errors already eradi- cates the most severe security vulnerabilities that allow arbitrary code execution on foreign hosts since these are based on exploiting incorrect memory management in applications which normally leads to run-time errors. Thus, the proposed research project aims to build a scalable analyzer that is precise enough to prove the absence of memory management errors in legacy C software. The project follows two strands: Firstly, new techniques for examining executable code are sought which will simplify the analysis of closed-source software and allow the analysis of concurrency primitives. Secondly, the project investigates into novel highlevel abstractions that combine shape- and numeric analysis. These abstractions are then applied to functions, enabling a context-sensitive analysis without repeating the analysis for each call-site.