Context-sensitive program analysis as database queries

ABSTRACT

Program analysis has been increasingly used in software engineering tasks such as auditing programs for security vulnerabilities and finding errors in general. Such tools often require analyses much more sophisticated than those traditionally used in compiler optimizations. In particular, context-sensitive pointer alias information is a prerequisite for any sound and precise analysis that reasons about uses of heap objects in a program. Context-sensitive analysis is challenging because there are over 10¹⁴ contexts in a typical large program, even after recursive cycles are collapsed. Moreover, pointers cannot be resolved in general without analyzing the entire program.

This paper presents a new framework, based on the concept of deductive databases, for context-sensitive program analysis. In this framework, all program information is stored as relations; data access and analyses are written as Datalog queries. To handle the large number of contexts in a program, the database represents relations with binary decision diagrams (BDDs). The system we have developed, called bddbddb, automatically translates database queries into highly optimized BDD programs.

Our preliminary experiences suggest that a large class of analyses involving heap objects can be described succinctly in Datalog and implemented efficiently with BDDs. To make developing application-specific analyses easy for programmers, we have also created a language called PQL that makes a subset of Datalog queries more intuitive to define. We have used the language to find many security holes in Web applications.

REFERENCES

• 1: Brad Arkin , Scott Stender , Gary McGraw, Software Penetration Testing, IEEE Security and Privacy, v.3 n.1, p.84-87, January 2005 [doi>10.1109/MSP.2005.23]
• 2: Dzintars Avots , Michael Dalton , V. Benjamin Livshits , Monica S. Lam, Improving software security with a C pointer analysis, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062520]
• 3: I. Balbin , K. Ramamohanarao, A generalization of the differential approach to recursive query evaluation, Journal of Logic Programming, v.4 n.3, p.259-262, Sept. 1987 [doi>10.1016/0743-1066(87)90004-5]
• 4: T. Ball and S. Rajamani. SLIC: A specification language for interface checking (of C). Technical Report MSR-TR-2001-21, Microsoft Research, Jan. 2002.
• 5: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 6: Francois Bancilhon , David Maier , Yehoshua Sagiv , Jeffrey D Ullman, Magic sets and other strange ways to implement logic programs (extended abstract), Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.1-15, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15399]
• 7: Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: F. Besson and T. Jensen. Modular class analysis with Datalog. In Proceedings of the 10th International Static Analysis Symposium, pages 19--36, June 2003.
• 9: Dirk Beyer , Andreas Noack , Claus Lewerentz, Simple and Efficient Relational Querying of Software Structures, Proceedings of the 10th Working Conference on Reverse Engineering, p.216, November 13-17, 2003
• 10: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 11: B. Buege, R. Layman, and A. Taylor. Hacking Exposed: J2EE and Java: Developing Secure Applications with Java Technology. McGraw-Hill/Osborne, 2002.
• 12: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 13: Stefano Ceri , Georg Gottlob , Letizia Tanca, Logic programming and databases, Springer-Verlag New York, Inc., New York, NY, 1990
• 14: A. Chandra and D. Harel. Horn clauses and generalizations. Journal of Logic Programming, 2(1):1--15, 1985.
• 15: Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996 [doi>10.1145/227595.227597]
• 16: Brian Chess , Gary McGraw, Static Analysis for Security, IEEE Security and Privacy, v.2 n.6, p.76-79, November 2004 [doi>10.1109/MSP.2004.111]
• 17: H. Cohen. BuDDy - a Binary Decision Diagram package. http://buddy. sourceforge.net/.
• 18: S. Cook. A Web developer's guide to cross-site scripting. http://www.giac.org/practical/GSEC/Steve_Cook_GSEC. pdf, 2003.
• 19: Marc-Michel Corsini , Kaninda Musumbu , Antoine Rauzy , Baudouin Le Charlier, Efficient Bottom-up Abstract Interpretation of Prolog by Means of Constraint Solving over Symbolic Finite Domains, Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, p.75-91, August 25-27, 1993
• 20: Manuvir Das , Ben Liblit , Manuel Fähndrich , Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, Proceedings of the 8th International Symposium on Static Analysis, p.260-278, July 16-18, 2001
• 21: Maryam Emami , Rakesh Ghiya , Laurie J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.242-256, June 20-24, 1994, Orlando, Florida, United States
• 22: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 23: Russell Greiner , Adam J. Grove , Dan Roth, Learning cost-sensitive active classifiers, Artificial Intelligence, v.139 n.2, p.137-174, August 2002 [doi>10.1016/S0004-3702(02)00209-6]
• 24: J. Grossman. WASC activities and U.S. Web application security trends. http://www.whitehatsec.com/presentations/WASC_WASF_1.02.pdf, 2004.
• 25: O. Grumberg, S. Livne, and S. Markovitch. Learning to order BDD variables in verification. Journal of Artificial Intelligence Research, 18:83--116, 2003.
• 26: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 27: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.254-263, June 2001, Snowbird, Utah, United States
• 28: G. Hulme. New software may improve application security. http://www.informationweek.com/story/IWK20010209S0003, 2001.
• 29: Mizuho Iwaihara , Yusaku Inoue, Bottom-Up Evaluation of Logic Programs Using Binary Decision Diagrams, Proceedings of the Eleventh International Conference on Data Engineering, p.467-474, March 06-10, 1995
• 30: R. Johnson and D. Wagner. Finding user/kernel pointer bugs with type inference. In Proceedings of the 2004 Usenix Security Conference, pages 119--134, 2004.
• 31: A. Klein. Divide and conquer: HTTP response splitting, Web cache poisoning attacks, and related topics. http://www.sanctuminc.com/pdf/Whitepaper_HTTPResponse.pdf, 2004.
• 32: William Landi , Barbara G. Ryder , Sean Zhang, Interprocedural modification side effect analysis with pointer aliasing, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.56-67, June 21-25, 1993, Albuquerque, New Mexico, United States
• 33: O. Lhoták and L. Hendren. Scaling Java points-to analysis using Spark. In Proceedings of the 12th International Conference on Compiler Construction, pages 153--169, April 2003.
• 34: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 35: Yanhong A. Liu , Scott D. Stoller, From datalog rules to efficient programs with time and space guarantees, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.172-183, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888268]
• 36: Roman Manevich , G. Ramalingam , John Field , Deepak Goyal , Mooly Sagiv, Compactly Representing First-Order Structures for Static Analysis, Proceedings of the 9th International Symposium on Static Analysis, p.196-212, September 17-20, 2002
• 37: J. F. Naughton and R. Ramakrishnan. Bottom-up evaluation of logic programs. In Computational Logic - Essays in Honor of Alan Robinson, pages 640--700, 1991.
• 38: Open Web Application Security Project. The ten most critical Web application security vulnerabilities. http://umn.dl.sourceforge.net/sourceforge/owasp/OWASPTopTen2004.pdf, 2004.
• 39: Raghu Ramakrishnan , Divesh Srivastava , S. Sudarshan, Rule Ordering in Bottom-Up Fixpoint Evaluation of Logic Programs, Proceedings of the 16th International Conference on Very Large Data Bases, p.359-371, August 13-16, 1990
• 40: Raghu Ramakrishnan , Divesh Srivastava , S. Sudarshan , Praveen Seshadri, Implementation of the CORAL deductive database system, Proceedings of the 1993 ACM SIGMOD international conference on Management of data, p.167-176, May 25-28, 1993, Washington, D.C., United States
• 41: T. Reps. Demand interprocedural program analysis using logic databases. Applications of Logic Databases, pages 163--196, 1994.
• 42: Thomas W. Reps, Solving Demand Versions of Interprocedural Analysis Problems, Proceedings of the 5th International Conference on Compiler Construction, p.389-403, April 07-09, 1994
• 43: O. Ruwase and M. S. Lam. A practical dynamic buffer overflow detector. In Proceedings of the 11th Annual Network and Distributed System Security Symposium, pages 159--169, 2004.
• 44: Joel Scambray , Stuart McClure , George Kurtz, Hacking Exposed, McGraw-Hill Professional, 2000
• 45: U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 2001 Usenix Security Conference, pages 201--220, 2001.
• 46: M. Sharir and A. Pnueli. Two approaches to interprocedural data-flow analyis. In S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--234. Prentice-Hall, 1981.
• 47: N. J. A. Sloane. The on-line encyclopedia of integer sequences: A000670. http://www.research.att.com/as/sequences, 2003.
• 48: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 49: Hisao Tamaki , Taisuke Sato, OLD Resolution with Tabulation, Proceedings of the Third International Conference on Logic Programming, p.84-98, July 14-18, 1986
• 50: J. D. Ullman, Bottom-up beats top-down for datalog, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.140-149, March 1989, Philadelphia, Pennsylvania, United States [doi>10.1145/73721.73736]
• 51: Jeffrey D. Ullman, Principles of Database and Knowledge-Base Systems: Volume II: The New Technologies, W. H. Freeman & Co., New York, NY, 1990
• 52: M. Vernon. Top five threats. ComputerWeekly.com (http://www.computerweekly.com/Article129980.htm), Apr. 2004.
• 53: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of Network and Distributed Systems Security Symposium, pages 3--17, 2000.
• 54: WebCohort, Inc. Only 10% of Web applications are secured against common hacking techniques. http://www.imperva.com/company/news/2004-feb-02.html, 2004.
• 55: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 56: John Whaley , Monica S. Lam, An Efficient Inclusion-Based Points-To Analysis for Strictly-Typed Languages, Proceedings of the 9th International Symposium on Static Analysis, p.180-195, September 17-20, 2002
• 57: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 58: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 59: Tuba Yavuz-Kahveci , Tevfik Bultan, Automated Verification of Concurrent Linked Lists with Counters, Proceedings of the 9th International Symposium on Static Analysis, p.69-84, September 17-20, 2002
• 60: Jianwen Zhu, Symbolic pointer analysis, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.150-157, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774594]
• 61: Jianwen Zhu , Silvian Calman, Symbolic pointer analysis revisited, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA