Paper Info
Title
Proving the Absence of Stack Overflows
Abstract
In safety-critical embedded systems the stack typically is the only dynamically allocated memory area. However, the maximal stack usage must be statically known: at configuration time developers have to reserve enough stack space for each task. Stack overflow errors are often hard to find but can cause the system to crash or behave erroneously. All current safety standards, e.g., ISO-26262, require upper estimations of the storage space; due to its dynamic behavior the stack is an especially critical storage area. Typically neither testing and measuring nor static source code analysis can provide safe bounds on the worst-case stack usage. A safe upper bound can be computed by whole-program static analysis at the executable code level. When an Abstract Interpretation based static analyzer is used, it can be formally proven that the maximal stack usage will never be underestimated. The challenge for binary-code level analyzers is to minimize the necessary amount of user interactions, e.g., for function pointer calls. To minimize user interaction, the analysis has to be precise, and the annotation mechanism has to be flexible and easy-to-use. The analyzer configuration has to be done once for each software project; afterwards the analysis can be run automatically, supporting continuous verification. In this article we describe the principles of Abstract Interpretation based stack analysis. We present an annotation language addressing all properties of typical automotive and avionics software and report on practical experience.
Year
DOI
Venue
2014
10.1007/978-3-319-10506-2_14
SAFECOMP
Field
DocType
Volume
Avionics software,Function pointer,Source code,Computer science,Abstract interpretation,Static analysis,Call stack,Stack trace,Reliability engineering,Executable,Embedded system
Conference
8666
ISSN
Citations 
PageRank 
0302-9743
6
0.60
References 
Authors
9
2
Name
Order
Citations
PageRank
Daniel Kästner17913.39
Christian Ferdinand223821.61