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

• Applicant: Dr. Axel Simon
• Subject Area: Software Engineering and Programming Languages
• Term: from 2009 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 154707536

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.

• DFG Programme: Independent Junior Research Groups