Validation of Memory Accesses Through Symbolic Analyses

Abstract : 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 prob- lem, we have designed and tested two static analyses - sym- bolic region and range analysis - which we combine to re- move the majority of these guards. In addition to the analy- ses themselves, we bring two other contributions. First, we describe live range splitting strategies that improve the effi- ciency and the precision of our analyses. Secondly, we show how to deal with integer overflows, a phenomenon that can compromise the correctness of static algorithms that validate memory accesses. We validate our claims 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. Furthermore, our approach is 50% more effective than Pentagons, a state- of-the-art analysis to sanitize memory accesses.
Type de document :
Communication dans un congrès
ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA'14), Oct 2014, Portland, Oregon, United States. pp.791-809, 2014, 〈10.1145/2660193.2660205〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01006209
Contributeur : Laure Gonnord <>
Soumis le : mardi 24 mars 2015 - 14:03:45
Dernière modification le : vendredi 20 avril 2018 - 15:44:25
Document(s) archivé(s) le : mercredi 1 juillet 2015 - 11:40:16

Fichier

oopsla14_memory_author_version...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale 4.0 International License

Identifiants

Collections

Citation

Henrique Nazaré, Izabela Maffra, Willer Santos, Leonardo Oliveira, Fernando Magno Quintão Pereira, et al.. Validation of Memory Accesses Through Symbolic Analyses. ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA'14), Oct 2014, Portland, Oregon, United States. pp.791-809, 2014, 〈10.1145/2660193.2660205〉. 〈hal-01006209〉

Partager

Métriques

Consultations de la notice

319

Téléchargements de fichiers

298