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

使用数字抽象域验证现有 C 程序中的内存处理。

• 批准号: 154707536
• 负责人: Dr. Axel Simon
• 金额: --
• 依托单位: Lehrstuhl Informatik II: Sprachen, und Beschreibungsstrukturen in der Informatik
• 依托单位国家: 德国
• 项目类别: Independent Junior Research Groups
• 财政年份: 2009
• 资助国家: 德国
• 起止时间: 2008-12-31 至 2013-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/154707536?language=en
• 关键词: Verifikation; der; Speicherhandhabung; bestehenden; Programmen

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.

长期以来，一直主张基于规格和逐项合同的正式方法，作为构建可靠软件的一种方式。但是，这种方法的成本和庞大的旧代码触发了对不存在规范的现有软件产品的自动分析的大量研究。鉴于缺乏完整的，特定于程序的规范，分析仪最多可以断言没有某些运行时错误，因为执行环境由执行环境定义了构成运行时错误的原因（例如，例如C语言规范）。有趣的是，消除运行时错误已经消除了最严重的安全性漏洞，这些漏洞允许对外国主机执行任意代码，因为这些漏洞是基于在通常会导致运行时错误的应用程序中利用错误的内存管理。因此，拟议的研究项目旨在构建一个可扩展的分析仪，该分析仪足以证明传统C软件中没有内存管理错误。该项目遵循两条链：首先，寻求检查可执行代码的新技术，这将简化封闭源软件的分析，并允许对并发原始词进行分析。其次，该项目研究了结合形状和数字分析的新型高级抽象。然后将这些抽象应用于函数，从而实现上下文敏感的分析，而无需重复每个呼叫点的分析。