NDLI: Validation of memory accesses through symbolic analyses

Content Provider	ACM Digital Library
Author	Barbosa, Leonardo Santos, Willer Nazaré, Henrique Quintão Pereira, Fernando Magno Maffra, Izabela Gonnord, Laure
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 problem, we have designed and tested two static analyses - symbolic region and range analysis - which we combine to remove the majority of these guards. In addition to the analyses themselves, we bring two other contributions. First, we describe live range splitting strategies that improve the efficiency 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.
Starting Page	791
Ending Page	809
Page Count	19
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2714064.2660205
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	49
Issue Number	10
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Static analysis Buffer overflow Security
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Validation of memory accesses through symbolic analyses

Compiler analysis of irregular memory accesses

CSSV:towards a realistic tool for statically detecting all buffer overflows in C

ARCHER:using symbolic, path-sensitive analysis to detect memory access errors

Memory access coalescing:a technique for eliminating redundant memory accesses

Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Symbolic execution for memory consumption analysis

Archipelago:trading address space for reliability and security (SIGP, Vol. 43, Issue. 3)

Optimizing off-chip accesses in multicores

Validation of memory accesses through symbolic analyses

Similar Documents

Validation of memory accesses through symbolic analyses

Compiler analysis of irregular memory accesses

CSSV:towards a realistic tool for statically detecting all buffer overflows in C

ARCHER:using symbolic, path-sensitive analysis to detect memory access errors

Memory access coalescing:a technique for eliminating redundant memory accesses

Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Symbolic execution for memory consumption analysis

Archipelago:trading address space for reliability and security (SIGP, Vol. 43, Issue. 3)

Optimizing off-chip accesses in multicores

Validation of memory accesses through symbolic analyses