2017-rv-vksa.md

plugin: "e-acsl"
authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson"
title: "Runtime detection of temporal memory errors."
book: "International Conference on Runtime Verification (RV)"
link: "https://julien-signoles.fr/publis/2017_rv.pdf"
doi: "10.1007/978-3-319-67531-2_18"
year: 2017
category: other

State-of-the-art memory debuggers have become efficient in detecting spatial memory errors – dereference of pointers to unallocated memory. These tools, however, cannot always detect errors arising from the use of stale pointers to valid memory (temporal memory errors). This paper presents an approach to reliable detection of temporal memory errors during a run of a program. This technique tracks allocated memory tagging allocated objects and pointers with tokens that allow to reason about their temporal properties. The technique further checks pointer dereferences and detects temporal (and spatial) memory errors before they occur. The present approach has been implemented in E-ACSL – a runtime verification tool for C programs. Experimentation with E-ACSL using TempLIST benchmark comprising small C programs seeded with temporal errors shows that the suggested technique detects temporal memory errors missed by state-of-the-art memory debuggers. Further experiments with computationally intensive runs of programs from SPEC CPU indicate that the overheads of the proposed approach are within acceptable range to be used during testing or debugging.