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.
Fri 24 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Validation of Memory Accesses Through Symbolic Analyses OOPSLA Henrique Nazaré Santos UFMG, Izabela Karennina Travizani Maffra UFMG, Willer Fernandes Santos UFMG, Leonardo Barbosa Oliveira UFMG, Laure Gonnord University of Lyon & LIP, France, Fernando Magno Quintão Pereira UFMG Link to publication | ||
13:52 22mTalk | Abstract Semantic Differencing via Speculative Correlation OOPSLA Link to publication | ||
14:15 22mTalk | Efficient Subcubic Alias Analysis for C OOPSLA Qirun Zhang The Hong Kong University of Science and Technology, A: Xiao Xiao The Hong Kong University of Science and Technology, A: Charles Zhang Hong Kong University of Science and Technology, A: Hao Yuan BOPU Technologies, A: Zhendong Su University of California, Davis Link to publication | ||
14:37 22mTalk | Static Analysis for Independent App Developers OOPSLA Lucas Brutschy ETH Zurich, Pietro Ferrara IBM Thomas J. Watson Research Center, Peter Müller ETH Zurich Link to publication |