Shadow state encoding for efficient monitoring of block-level properties - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Access content directly
Conference Papers Year : 2017

Shadow state encoding for efficient monitoring of block-level properties


Memory shadowing associates addresses from an application's memory to values stored in a disjoint memory space called shadow memory. At runtime shadow values store metadata about application memory locations they are mapped to. Shadow state encodings -The structure of shadow values and their interpretation - vary across different tools. Encodings used by the state-of-The-Art monitoring tools have been proven useful for tracking memory at a byte-level, but cannot address properties related to memory block boundaries. Tracking block boundaries is however crucial for spatial memory safety analysis, where a spatial violation such as outof- bounds access, may dereference an allocated location belonging to an adjacent block or a different struct member. This paper describes two novel shadow state encodings which capture block-boundary-related properties. These encodings have been implemented in E-ACSL -A runtime verification tool for C programs. Initial experiments involving checking validity of pointer and array accesses in computationally intensive runs of programs selected from SPEC CPU benchmarks demonstrate runtime and memory overheads comparable to state-of-The-Art memory debuggers.
Not file

Dates and versions

cea-01836510 , version 1 (12-07-2018)



K. Vorobyov, J. Signoles, N. Kosmatov. Shadow state encoding for efficient monitoring of block-level properties. ISMM 2017 Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, Jun 2017, Barcelona, Spain. pp.47-58, ⟨10.1145/3092255.3092269⟩. ⟨cea-01836510⟩
34 View
0 Download



Gmail Facebook Twitter LinkedIn More