Shadow state encoding for efficient monitoring of block-level properties

K. Vorobyov; J. Signoles; N. Kosmatov

Shadow state encoding for efficient monitoring of block-level properties

K. Vorobyov ¹ J. Signoles ¹ N. Kosmatov ¹

1 DILS - Département Ingénierie Logiciels et Systèmes

Abstract : 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.

Keywords : C (programming language) Encoding (symbols) Signal encoding State assignment Efficient monitoring Memory overheads Memory safety Monitoring tools Run-time verification Runtime Monitoring Shadow memory State of the art Program debugging

Document type :

Conference papers

Domain :

Computer Science [cs]

Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01836510
Contributor : Léna Le Roy <>
Submitted on : Thursday, July 12, 2018 - 1:24:30 PM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Shadow state encoding for efficient monitoring of block-level properties

Identifiers

Collections

Citation

Export

Metrics

50

Contact

Shadow state encoding for efficient monitoring of block-level properties

Identifiers

Collections

Citation

Export

Share

Metrics

50

Contact