Static analysis of string manipulations in critical embedded C programs. (English) Zbl 1225.68064

Allamigeon, Xavier; Godard, Wenceslas; Hymans, Charles

Yi, Kwangkeun (ed.), Static analysis. 13th international symposium, SAS 2006, Seoul, Korea, August 29–31, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37756-6/pbk). Lecture Notes in Computer Science 4134, 35-51 (2006).

Summary: This paper describes a new static analysis to show the absence of memory errors, especially string buffer overflows in C programs. The analysis is specifically designed for the subset of C that is found in critical embedded software. It is based on the theory of abstract interpretation and relies on an abstraction of stores that retains the length of string buffers. A transport structure allows to change the granularity of the abstraction and to concisely define several inherently complex abstract primitives such as destructive update and string copy. The analysis integrates several features of the C language such as multi-dimensional arrays, structures, pointers and function calls. A prototype implementation produces encouraging results in early experiments.
For the entire collection see [Zbl 1120.68011].

MSC:

68N30	Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55	Semantics in the theory of computing

Software:

ASTREE; OCaml; CSSV; Scapy