Fast as a shadow, expressive as a tree: hybrid memory monitoring for C

One classical approach to ensuring memory safety of C programs is based on storing block metadata in a tree-like datastructure. However it becomes relatively slow when the number of memory locations in the tree becomes high. Another solution, based on shadow memory, allows very fast constant-time access to metadata and led to development of several highly optimized tools for detection of memory safety errors. However, this solution appears to be insufficient for evaluation of complex memory-related properties of an expressive specification language. In this work, we address memory monitoring in the context of runtime assertion checking of C programs annotated in E-ACSL, an expressive specification language offered by the FRAMA-C framework for analysis of C code. We present an original combination of a tree-based and a shadow-memory-based techniques that reconciles both the efficiency of shadow memory with the higher expressiveness of annotations whose runtime evaluation can be ens...

• Type: Journal
• Year: 2015
• Where: SAC
• Authors: Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
• Keywords: Applied Computing, SAC 2015