Hua Yan
Yulei Sui
Jingling Xue
ABSTRACT
Zero-day Use-After-Free (UAF) vulnerabilities are increasingly popular and highly dangerous, but few mitigations exist. We introduce a new pointer-analysis-based static analysis, CRed, for finding UAF bugs in multi-MLOC C source code efficiently and effectively. CRed achieves this by making three advances: (i) a spatio-temporal context reduction technique for scaling down soundly and precisely the exponential number of contexts that would otherwise be considered at a pair of free and use sites, (ii) a multi-stage analysis for filtering out false alarms efficiently, and (iii) a path-sensitive demand-driven approach for finding the points-to information required.
We have implemented CRed in LLVM-3.8.0 and compared it with four different state-of-the-art static tools: CBMC (model checking), Clang (abstract interpretation), Coccinelle (pattern matching), and Supa (pointer analysis) using all the C test cases in Juliet Test Suite (JTS) and 10 open-source C applications. For the ground-truth validated with JTS, CRed detects all the 138 known UAF bugs as CBMC and Supa do while Clang and Coccinelle miss some bugs, with no false alarms from any tool. For practicality validated with the 10 applications (totaling 3+ MLOC), CRed reports 132 warnings including 85 bugs in 7.6 hours while the existing tools are either unscalable by terminating within 3 days only for one application (CBMC) or impractical by finding virtually no bugs (Clang and Coccinelle) or issuing an excessive number of false alarms (Supa).
- Juliet Test Suite 1.2. https://samate.nist.gov/SRD/testsuite.php.Google Scholar
- Periklis Akritidis. 2010. Cling: A memory allocator to mitigate dangling pointers. In USENIX Security'10. 177--192. Google ScholarDigital Library
- Clang Static Analyzer. http://clang-analyzer.llvm.org/.Google Scholar
- Lars Ole Andersen. 1994. Program analysis and specialization for the C programming language. Ph.D. Dissertation. DIKU, University of Copenhagen.Google Scholar
- George Balatsouras and Yannis Smaragdakis. 2016. Structure-Sensitive Points-To Analysis for C and C++. In SAS'16. 84--104.Google ScholarCross Ref
- Thomas Ball and Sriram K Rajamani. 2002. The SLAM project: Debugging system software via static analysis. In POPL'02. 1--3. Google ScholarDigital Library
- Emery D. Berger and Benjamin G. Zorn. 2006. DieHard: Probabilistic memory safety for unsafe languages. In PLDI'06. 158--168. Google ScholarDigital Library
- Dirk Beyer, Thomas A Henzinger, Ranjit Jhala, and Rupak Majumdar. 2007. The software model checker Blast. International Journal on Software Tools for Technology Transfer 9, 5--6 (2007), 505--525. Google ScholarDigital Library
- Derek Bruening and Qin Zhao. 2011. Practical memory checking with Dr. Memory. In CGO'11. 213--223. Google ScholarDigital Library
- Juan Caballero, Gustavo Grieco, Mark Marron, and Antonio Nappa. 2012. Undangle: Early detection of dangling pointers in use-after-free and double-free vulnerabilities. In ISSTA'12. 133--143. Google ScholarDigital Library
- Sigmund Cherem, Lonnie Princehouse, and Radu Rugina. 2007. Practical memory leak detection using guarded value-flow analysis. In PLDI'07. 480--491. Google ScholarDigital Library
- Thurston HY Dang, Petros Maniatis, and David Wagner. 2017. Oscar: A practical page-permissions-based scheme for thwarting dangling pointers. In USENIX Security'17. 815--832. Google ScholarDigital Library
- Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In TACAS'08. 337--340. Google ScholarDigital Library
- Isil Dillig, Thomas Dillig, and Alex Aiken. 2008. Sound, complete and scalable path-sensitive analysis. In PLDI'08. 270--280. Google ScholarDigital Library
- Isaac Evans, Fan Long, Ulziibayar Otgonbaatar, Howard Shrobe, Martin Rinard, Hamed Okhravi, and Stelios Sidiroglou-Douskos. 2015. Control Jujutsu: On the weaknesses of fine-grained control flow integrity. In CCS'15. 901--913. Google ScholarDigital Library
- Manuel Fähndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In FoVeOOS'10. 10--30. Google ScholarDigital Library
- Xiaokang Fan, Yulei Sui, Xiangke Liao, and Jingling Xue. 2017. Boosting the Precision of Virtual Call Integrity Protection with Partial Pointer Analysis for C++. In ISSTA'17. 329--340. Google ScholarDigital Library
- Josselin Feist, Laurent Mounier, and Marie-Laure Potet. 2014. Statically detecting use after free on binary code. Journal of Computer Virology and Hacking Techniques 10, 3 (2014), 211--217.Google ScholarCross Ref
- Ben Hardekopf and Calvin Lin. 2011. Flow-sensitive pointer analysis for millions of lines of code. In CGO'11. 289--298. Google ScholarDigital Library
- Nevin Heintze and Olivier Tardieu. 2001. Demand-Driven Pointer Analysis. In PLDI'01. 24--34. Google ScholarDigital Library
- Julien Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival. 2011. Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Software Engineering Notes 36, 1 (2011), 1--8. Google ScholarDigital Library
- Daniel Kroening and Michael Tautschnig. 2014. CBMC-C Bounded model checker. In TACAS'14. 389--391.Google ScholarCross Ref
- William Landi and Barbara G Ryder. 1992. A safe approximate algorithm for interprocedural aliasing. In PLDI'92. 235--248. Google ScholarDigital Library
- Wei Le and Mary Lou Soffa. 2008. Marple: A demand-driven path-sensitive buffer overflow detector. In FSE'08. 272--282. Google ScholarDigital Library
- Byoungyoung Lee, Chengyu Song, Yeongjin Jang, Tielei Wang, Taesoo Kim, Long Lu, and Wenke Lee. 2015. Preventing use-after-free with dangling pointers nullification.. In NDSS'15.Google ScholarCross Ref
- Ondrej Lhoták and Kwok-Chiang Andrew Chung. 2011. Points-to analysis with efficient strong updates. In POPL'11. 3--16. Google ScholarDigital Library
- Lian Li, Cristina Cifuentes, and Nathan Keynes. 2010. Practical and effective symbolic analysis for buffer overflow detection. In FSE'10. 317--326. Google ScholarDigital Library
- Lian Li, Cristina Cifuentes, and Nathan Keynes. 2011. Boosting the performance of flow-sensitive points-to analysis using value flow. In FSE'11. 343--353. Google ScholarDigital Library
- Ravichandhran Madhavan and Raghavan Komondoor. 2011. Null dereference verification via over-approximated weakest pre-conditions analysis. In OOSPLA'11. 1033--1052. Google ScholarDigital Library
- Santosh Nagarakatte, Jianzhou Zhao, Milo MK Martin, and Steve Zdancewic. 2010. CETS: Compiler enforced temporal safety for C. In ISMM'10. 31--40. Google ScholarDigital Library
- Nicholas Nethercote and Julian Seward. 2007. Valgrind: A framework for heavyweight dynamic binary instrumentation. In PLDI '07. 89--100. Google ScholarDigital Library
- Gene Novark and Emery D Berger. 2010. DieHarder: Securing the heap. In CCS'10. 573--584. Google ScholarDigital Library
- Mads Chr Olesen, René Rydhof Hansen, Julia L Lawall, and Nicolas Palix. 2014. Coccinelle: Tool support for automated CERT C secure coding standard certification. Science of Computer Programming 91 (2014), 141--160.Google ScholarCross Ref
- Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL'95. 49--61. Google ScholarDigital Library
- Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. 2012. AddressSanitizer: A fast address sanity checker. In USENIX ATC'12. 309--318. Google ScholarDigital Library
- Lei Shang, Xinwei Xie, and Jingling Xue. 2012. On-demand dynamic summary-based points-to analysis. In CGO'12. 264--274. Google ScholarDigital Library
- Fabio Somenzi. CUDD: CU Decision Diagram Package (3.0.0). http://vlsi.colorado.edu/~fabio/CUDD/cudd.pdf.Google Scholar
- Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. 2016. Boomerang: Demand-driven flow-and context-sensitive pointer analysis for Java. In ECOOP'16. 22:1--22:26.Google Scholar
- Manu Sridharan and Rastislav Bodík. 2006. Refinement-based context-sensitive points-to analysis for Java. In PLDI'16. 387--400. Google ScholarDigital Library
- Yulei Sui, Peng Di, and Jingling Xue. 2016. Sparse flow-sensitive pointer analysis for multithreaded programs. In CGO'16. 160--170. Google ScholarDigital Library
- Yulei Sui, Yue Li, and Jingling Xue. 2013. Query-directed adaptive heap cloning for optimizing compilers. In CGO'13. 1--11. Google ScholarDigital Library
- Yulei Sui and Jingling Xue. 2016. On-demand strong update analysis via value-flow refinement. In FSE'16. 460--473. Google ScholarDigital Library
- Yulei Sui and Jingling Xue. 2016. SVF: Interprocedural static value-flow analysis in LLVM. https://github.com/unsw-corg/SVF. In CC'16. 265--266. Google ScholarDigital Library
- Yulei Sui, Ding Ye, and Jingling Xue. 2012. Static memory leak detection using full-sparse value-flow analysis. In ISSTA'12. 254--264. Google ScholarDigital Library
- Yulei Sui, Ding Ye, and Jingling Xue. 2014. Detecting memory leaks statically with full-sparse value-flow analysis. IEEE Transactions on Software Engineering 40, 2 (2014), 107--122. Google ScholarDigital Library
- Yulei Sui, Sen Ye, Jingling Xue, and Pen-Chung Yew. 2011. SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA. In APLAS'11. 155--171. Google ScholarDigital Library
- Erik van der Kouwe, Vinod Nigade, and Cristiano Giuffrida. 2017. DangSan: Scalable use-after-free detection.. In EuroSys'17. 405--419. Google ScholarDigital Library
- Kostyantyn Vorobyov and Padmanabhan Krishnan. 2010. Comparing model checking and static program analysis: A case study in error detection approaches. In SSV'10. 1--7.Google Scholar
- National vulnerability database. http://nvd.nist.gov/.Google Scholar
- Yichen Xie and Alex Aiken. 2007. Saturn: A scalable framework for error detection using boolean satisfiability. ACM Transactions on Programming Languages and Systems 29, 3 (2007), 16. Google ScholarDigital Library
- Wei Xu, Daniel C DuVarney, and R Sekar. 2004. An efficient and backwards-compatible transformation to ensure memory safety of C programs. In FSE'12. 117--126. Google ScholarDigital Library
- Sen Ye, Yulei Sui, and Jingling Xue. 2014. Region-based selective flow-sensitive pointer analysis. In SAS'14. 319--336.Google ScholarCross Ref
- Yves Younan. 2015. FreeSentry: Protecting against use-after-free vulnerabilities due to dangling pointers. In NDSS'15.Google ScholarCross Ref
- Hongtao Yu, Jingling Xue, Wei Huo, Xiaobing Feng, and Zhaoqing Zhang. 2010. Level by level: Making flow-and context-sensitive pointer analysis scalable for millions of lines of code. In CGO'10. 218--229. Google ScholarDigital Library
- Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In POPL'12. 427--440. Google ScholarDigital Library
- Xin Zheng and Radu Rugina. 2008. Demand-driven alias analysis for C. In POPL'08. 197--208. Google ScholarDigital Library
Index Terms
- Spatio-temporal context reduction: a pointer-analysis-based static approach for detecting use-after-free vulnerabilities
Recommendations
Machine-Learning-Guided Typestate Analysis for Static Use-After-Free Detection
ACSAC '17: Proceedings of the 33rd Annual Computer Security Applications ConferenceTypestate analysis relies on pointer analysis for detecting temporal memory safety errors, such as use-after-free (UAF). For large programs, scalable pointer analysis is usually imprecise in analyzing their hard "corner cases", such as infeasible paths, ...
Tracking pointers with path and context sensitivity for bug detection in C programs
This paper proposes a pointer alias analysis for automatic error detection. State-of-the-art pointer alias analyses are either too slow or too imprecise for finding errors in real-life programs. We propose a hybrid pointer analysis that tracks actively ...
Interprocedural pointer alias analysis
We present practical approximation methods for computing and representing interprocedural aliases for a program written in a language that includes pointers, reference parameters, and recursion. We present the following contributions: (1) a framework ...
Comments