An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs - Runtime Verification - page 180

way to find the base address of the block, block size and pointer offset required
by memory-related e-acsl clauses.
Our global objective is quite different from these efforts. Unlike these ad-
vanced works focused on detection of memory safety errors, we aim at supporting
runtime checking for memory-related annotations of an expressive specification
language e-acsl. Even if we have already realized several optimizations, per-
formances of our implementation remain below the most advanced proposals
addressing memory safety [26-28, 30, 25]. It must be further studied if the ef-
ficient solutions they implement are compatible with our objective to support
runtime assertion checking for such a rich specification language as e-acsl.On
the other hand, the ambitious objective to perform runtime assertion checking
for C code completely specified in e-acsl and directly compatible with inte-
grated Frama-C tools for proof of programs (where manual analysis of proof
failures can be even more costly) could justify a higher overhead.
Optimizations. Our proposal to record block metadata using Patricia tries is
related to Jones's and Kelly's work [16] that proposed to use Splay trees for this
purpose. Splay trees were also used in several recent tools related to memory
safety [24, 29]. To the best of our knowledge, Patricia tries have never been
used in this context. Static analysis based techniques to reduce memory mon-
itoring have been used in earlier works, for instance, in [27, 28, 24]. Similarly,
our dataflow analysis described in Sec. 6 performs an overapproximation of the
necessary memory monitoring and successfully removes many irrelevant records
and queries. We intend to further improve its precision in our future work.
9 Conclusion and Future Work
We have presented our solution of memory monitoring for runtime assertion
checking with Frama-C. It can be applied on C code annotated in e-acsl,an
executable specification language offering among other features various memory-
related constructs on validity and initialization of memory locations. The advan-
tages of this solution include a very expressive specification formalism, a deep
integration into the Frama-C platform and various possibilities of collaboration
with other analyzers [7]. Thus, runtime assertion checking can benefit from an-
notations automatically generated by other plug-ins (e.g. Value or RTE), help
to understand proof failures (e.g. during program proof with jessie or wp plug-
ins), skip runtime checking of properties already established by other plug-ins
and contribute to consolidated statuses of annotations in Frama-C [5].
We have described the global architecture, instrumentation with e-acsl2c
and particular aspects related to ecient storage of block metadata, ecient
updates and lookups in the store and static analysis based optimization of mon-
itored variables, as well as our initial experimental results. In particular, runtime
assertion checking has indeed found errors in 100% of non-equivalent mutants
for several simple C programs with complete e-acsl contracts.
One future work direction is extending the support of e-acsl language by
e-acsl2c, in particular, for temporal memory safety and advanced memory-
related constructs like \assigns , \freeable or \separated [10]. Even if our main