PICO: A Presburger In-bounds Check Optimization for Compiler-based Memory Safety Instrumentations
Article No.: 45, Pages 1 - 27
Abstract
Memory safety violations such as buffer overflows are a threat to security to this day. A common solution to ensure memory safety for C is code instrumentation. However, this often causes high execution-time overhead and is therefore rarely used in production.
Static analyses can reduce this overhead by proving some memory accesses in bounds at compile time. In practice, however, static analyses may fail to verify in-bounds accesses due to over-approximation. Therefore, it is important to additionally optimize the checks that reside in the program.
In this article, we present PICO, an approach to eliminate and replace in-bounds checks. PICO exactly captures the spatial memory safety of accesses using Presburger formulas to either verify them statically or substitute existing checks with more efficient ones. Thereby, PICO can generate checks of which each covers multiple accesses and place them at infrequently executed locations.
We evaluate our LLVM-based PICO prototype with the well-known SoftBound instrumentation on SPEC benchmarks commonly used in related work. PICO reduces the execution-time overhead introduced by SoftBound by 36% on average (and the code-size overhead by 24%). Our evaluation shows that the impact of substituting checks dominates that of removing provably redundant checks.
References
[1]
Periklis Akritidis, Manuel Costa, Miguel Castro, and Steven Hand. 2009. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In SSYM’09. 51–66. https://dl.acm.org/citation.cfm?id=1855772.
[2]
Olaf Bachmann, Paul S. Wang, and Eugene V. Zima. 1994. Chains of recurrences—A method to expedite the evaluation of closed-form functions. In ISSAC’94. 242–249.
[3]
E. T. Bell. 1938. The iterated exponential integers. Ann. Math. 39, 3 (1938), 539–557. http://www.jstor.org/stable/1968633.
[4]
Rastislav Bodík, Rajiv Gupta, and Vivek Sarkar. 2000. ABCD: Eliminating array bounds checks on demand. In PLDI’00. Association for Computing Machinery, New York, NY, 321–333.
[5]
Derek Bruening and Qin Zhao. 2011. Practical memory checking with Dr. Memory. In CGO’11. IEEE Computer Society, 213–223.
[6]
M. G. Burke, J.-D. Choi, S. Fink, D. Grove, M. Hind, V. Sarkar, M. J. Serrano, V. C. Sreedhar, H. Srinivasan, and J. Whaley. 1999. The jalapeño dynamic optimizing compiler for Java. In JAVA’ 99. ACM, 129–141.
[7]
Dinakar Dhurjati and Vikram Adve. 2006. Backwards-compatible array bounds checking for C with very low overhead. In ICSE’06. 162–171.
[8]
Thomas Dillig, Isil Dillig, and Swarat Chaudhuri. 2014. Optimal guard synthesis for memory safety. In Computer-aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 491–507.
[9]
Johannes Doerfert, Tobias Grosser, and Sebastian Hack. 2017. Optimistic loop optimization. In CGO’17. IEEE, 292–304.
[10]
Gregory J. Duck and Roland H. C. Yap. 2016. Heap bounds protection with low fat pointers. In CC’16. 132–142.
[11]
Dietmar Ebner, Bernhard Scholz, and Andreas Krall. 2009. Progressive spill code placement. In CASES’09. ACM, New York, NY, 77–86.
[12]
Robert van Engelen. 2001. Efficient symbolic analysis for optimizing compilers. In CC’01. Springer, London, UK, 118–132. http://dl.acm.org/citation.cfm?id=647477.727776.
[13]
Manuel Fähndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In FoVeOOS’10. Springer, Berlin, 10–30. https://doi.org/10.1007/978-3-642-18070-5_2
[14]
Alain Finkel and Jérôme Leroux. 2002. How to compose Presburger-accelerations: Applications to broadcast protocols. In FST TCS’02. Springer, Berlin, 145–156.
[15]
Michael J. Fischer and Michael O. Rabin. 1998. Super-exponential complexity of presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 122–135.
[16]
Tobias Grosser, Armin Größlinger, and Christian Lengauer. 2012. Polly—Performing polyhedral optimizations on a low-level intermediate representation. Parallel Proc. Lett. 22, 4 (2012), 27.
[17]
Tobias Grosser, Sven Verdoolaege, and Albert Cohen. 2015. Polyhedral AST Generation is more than scanning polyhedra. ACM Trans. Prog. Lang. Syst. 37, 4 (July 2015).
[18]
Dan Grossman, Michael Hicks, Trevor Jim, Greg Morrisett, James Cheney, and Yanling Wang. 2005. Cyclone: A type-safe dialect of C. C/C++ Users J. 23, 1 (2005), 112–139.
[19]
John L. Henning. 2006. SPEC CPU2006 benchmark descriptions. ACM SIGARCH Comput. Archit. News 34, 4 (Sept. 2006), 1–17.
[20]
Richard W. M. Jones and Paul H. J. Kelly. 1997. Backwards-compatible bounds checking for arrays and pointers in C programs. In AADEBUG’97. 13–26.
[21]
Tina Jung. 2015. A Hybrid Approach for Parametric Memory Dependence Analysis. Bachelor’s Thesis. Saarland University.
[22]
Taddeus Kroes, Koen Koning, Erik van der Kouwe, Herbert Bos, and Cristiano Giuffrida. 2018. Delta pointers: Buffer overflow checks without the checks. In EuroSys’18. ACM.
[23]
Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In CGO’04. IEEE Computer Society, 75–88.
[24]
LLVM. 2020. LLVM Block Frequency Analysis. https://llvm.org/doxygen/classllvm_1_1BlockFrequ encyInfoImpl.html#details.
[25]
Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In SAC’08. ACM, New York, NY, 184–188.
[26]
Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, and Martin Rinard. 2014. Sound input filter generation for integer overflow errors. In POPL’14. ACM, New York, NY, 439–452.
[27]
T. J. McCabe. 1976. A complexity measure. IEEE Trans. Softw. Eng.4 (1976), 308–320.
[28]
MITRE Corporation. 2019. Top 25 Most Dangerous Software Errors 2019, Common Weakness Enumeration CWE. https://cwe.mitre.org/top25/archive/2019/2019_cw e_top25.html.
[29]
Santosh Nagarakatte. 2016. SoftBound + CETS for LLVM-3.9. https://github.com/santoshn/SoftBoundCETS-3.9.
[30]
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2015. Everything you want to know about pointer-based checking. In SNAPL’15, Vol. 32. Dagstuhl, Germany, 190–208.
[31]
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. 2009. SoftBound: Highly compatible and complete spatial memory safety for C. In PLDI’09. ACM, 245–258.
[32]
H. Nazaré, I. Maffra, W. Santos, L. Barbosa, L. Gonnord, and F. M. Q. Pereira. 2014. Validation of memory accesses through symbolic analyses. In OOPSLA’14. ACM, New York, NY, 791–809.
[33]
George C. Necula, Scott McPeak, and Westley Weimer. 2002. CCured: Type-safe retrofitting of legacy code. In POPL’02. 128–139.
[34]
Nicholas Nethercote and Julian Seward. 2007. Valgrind: A framework for heavyweight dynamic binary instrumentation. ACM Sigplan Not. 42, 6 (2007), 89–100.
[35]
Sebastian Pop, Albert Cohen, and Georges-André Silber. 2005. Induction variable analysis with delayed abstractions. In HiPEAC’05. Springer, Berlin, 218–232.
[36]
Corneliu Popeea, Dana N. Xu, and Wei-Ngan Chin. 2008. A practical and precise inference and specializer for array bound checks elimination. In PEPM’08. ACM, New York, NY, 177–187.
[37]
William Pugh. 1994. Counting solutions to Presburger formulas: How and why. In PLDI’94. ACM, New York, NY, 121–134.
[38]
Rust. 2020. Rust language manual. https://www.rust-lang.org/.
[39]
Olatunji Ruwase and Monica S. Lam. 2004. A practical dynamic buffer overflow detector. In NDSS’04. 159–169.
[40]
D. Song, J. Lettner, P. Rajasekaran, Y. Na, S. Volckaert, P. Larsen, and M. Franz. 2019. SoK: Sanitizing for security. In SP’19. IEEE, 1275–1295.
[41]
Standard Performance Evaluation Corporation SPEC. 2000. SPEC CPU 2000 benchmarks. https://www.spec.org/cpu2000/.
[42]
Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Xiaodong Song. 2013. SoK: Eternal war in memory. In S&P’13. 48–62.
[43]
David Tarditi, Archibald Samuel Elliott, Andrew Ruef, and Michael Hicks. 2018. Checked C: Making C safe by extension. In SecDev’18. IEEE, 53–60.
[44]
Sid-Ahmed-Ali Touati, Julien Worms, and Sébastien Briais. 2013. The Speedup-Test: a statistical methodology for programme speedup analysis and computation. Concurr. Comp. Pract. Exp. 25, 10 (2013), 1410–1426.
[45]
Sven Verdoolaege. 2010. isl: An integer set library for the polyhedral model. In ICMS’10. Springer, Berlin, 299–302.
[46]
Jingling Xue and Jens Knoop. 2006. A fresh look at PRE as a maximum flow problem. In Compiler Construction, Alan Mycroft and Andreas Zeller (Eds.). Springer, Berlin, 139–154.
[47]
Ding Ye, Yu Su, Yulei Sui, and Jingling Xue. 2014. WPBOUND: Enforcing spatial memory safety efficiently at runtime with weakest preconditions. In ISSRE’14. IEEE, Washington, DC, 88–99.
Index Terms
- PICO: A Presburger In-bounds Check Optimization for Compiler-based Memory Safety Instrumentations
Recommendations
SoftBound: highly compatible and complete spatial memory safety for c
PLDI '09The serious bugs and security vulnerabilities facilitated by C/C++'s lack of bounds checking are well known, yet C and C++ remain in widespread use. Unfortunately, C's arbitrary pointer arithmetic, conflation of pointers and arrays, and programmer-...
Instrew: leveraging LLVM for high performance dynamic binary instrumentation
VEE '20: Proceedings of the 16th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution EnvironmentsDynamic binary instrumentation frameworks are popular tools to enhance programs with additional analysis, debugging, or profiling facilities or to add optimizations or translations without requiring recompilation or access to source code. They analyze ...
Model checking C++ programs with exceptions
We present an extension of the DIVINE software model checker to support programs with exception handling. The extension consists of two parts, a language-neutral implementation of the LLVM exception-handling instructions, and an adaptation of the C++ ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
December 2021
497 pages
Copyright © 2021 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 17 July 2021
Accepted: 01 April 2021
Revised: 01 February 2021
Received: 01 September 2020
Published in TACO Volume 18, Issue 4
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 892Total Downloads
- Downloads (Last 12 months)313
- Downloads (Last 6 weeks)47
Reflects downloads up to 24 Nov 2024
Other Metrics
Citations
Cited By
View allView Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatLogin options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in