Validation of Memory Accesses Through Symbolic Analyses

Exposé invité Aric, 12 mars 2015, 10h30

Laure Gonnord, UCBL / Compsys

Résumé:

Joined work with F. Pereira and his collegues @Univ Mineas Gerais,
Bresil. Published at oopsla’14
The C programming language does not prevent out-of-bounds memory
accesses. There exist several techniques to secure C programs;
however, these methods tend to slow down these programs substantially,
because they populate the binary code with runtime checks. To deal
with this problem, we have designed and tested a succession of static
analyses to remove the majority of these guards.

We validate these static analyses by incorporating our findings into
AddressSanitizer : we generate SPEC CINT 2006 code that is 17% faster
and 9% more energy efficient than the code produced originally by this
tool.

In this talk I will present some of the static analyses that we
designed in this paper, focusing on our new “symbolic range” analysis,
and also the techniques we use to be able to scale well.