Stack bounds analysis for microcontroller assembly code
Jörg Bräuer, Bastian Schlich, Thomas Reinbacher, Stefan Kowalewski · 2009
An important criterion for correctness of embedded software is stack safety, which requires that the stack must never overflow. This paper presents a static analysis for assembly code that determines upper and lower bounds of the stack. These bounds serve two purposes. First, they can be used to verify stack safety. Second, they can be used to increase the precision of several other static analyses, which are used in the context of model checking. Interrupts play an important role in embedded software, but they are a major challenge for the static analysis of stack bounds. In different micro--controller architectures, the handling of interrupts varies. In some architectures, interrupt handlers are executed atomically, while in others, they are interruptible. Therefore, we applied this analysis to two different microcontrollers, namely the ATMEL ATmega16 and the Intel MCS-51. In a case study, we show the applicability and efficiency of this analysis.