Flow-insensitive type qualifiers

ABSTRACT

We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming languages with static type systems, such as C and Java. In our system, programmers add a few type qualifier annotations to their program, and automatic type qualifier inference determines the remaining qualifiers and checks the annotations for consistency. We describe a tool CQual for adding type qualifiers to the C programming language. Our tool CQual includes a visualization component for displaying browsable inference results to the programmer. Finally, we present several experiments using our tool, including inferring const qualifiers, finding security vulnerabilities in several popular C programs, and checking initialization data usage in the Linux kernel. Our results suggest that inference and visualization make type qualifiers lightweight, that type qualifier inference scales to large programs, and that type qualifiers are applicable to a wide variety of problems.

REFERENCES

• 1: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 2: Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 3: Ansi 1989. Rationale for American National Standard for Information Systems---Programming Language---C. ANSI. Associated with ANSI standard X3.159-1989.
• 4: Ansi 1999. Programming languages---C. ANSI/ISO/IEC 9899:1999.
• 5: Bailleux, C. 2000. More security problems in bftpd-1.0.12. BugTraq Mailing List. http://www.securityfocus.com/archive/1/149977.
• 6: Thomas Ball , Mayur Naik , Sriram K. Rajamani, From symptom to cause: localizing errors in counterexample traces, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.97-105, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 8: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 9: Bishop, M. and Dilger, M. 1996. Checking for race conditions in file accesses. Comput. Syst. 2, 2, 131--152.
• 10: Broadwell, P., Harren, M., and Sastry, N. 2003. Scrash: A system for generating secure crash information. In Proceedings of the 12th Usenix Security Symposium (Washington, DC).
• 11: 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]
• 12: Cert. 2001. CERT Advisory CA-2001-19 “Code Red” worm exploiting buffer overflow In IIS indexing service DLL. http://www.cert.org/advisories/CA-2001-19.html.
• 13: Satish Chandra , Thomas Reps, Physical type checking for C, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.66-75, September 06-06, 1999, Toulouse, France
• 14: Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 15: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 16: Cowan, C., Barringer, M., Beattie, S., and Kroah-Hartman, G. 2001. FormatGuard: Automatic protection from print format string vulnerabilities. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).
• 17: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: 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
• 19: Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.
• 20: DeKok, A. 2000. PScan: A limited problem scanner for C source files. http://www.striker.ottawa.on.ca/~aland/pscan.
• 21: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 22: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 23: Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Tech. Rep. 159, Compaq Systems Research Center. Dec.
• 24: Dirk Dussart , Fritz Henglein , Christian Mossin, Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time, Proceedings of the Second International Symposium on Static Analysis, p.118-135, September 25-27, 1995
• 25: Eifrig, J., Smith, S., and Trifonov, V. 1995. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier-North Holland, Amsterdam, The Netherlands.
• 26: Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the 4th Symposium on Operating System Design and Implementation (San Diego, CA).
• 27: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 28: Fähndrich, M. 1999. BANE: A library for scalable constraint-based program analysis. Ph.D. thesis, University of California, Berkeley.
• 29: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 30: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 31: Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.23-32, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 32: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 33: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 34: Jeffrey Scott Foster , Alexander S. Aiken, Type qualifiers: lightweight specifications to improve software quality, 2002
• 35: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 36: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 37: Frasunek, P. 2001a. format string vulnerability in mars_nwe 0.99pl19. http://online.securityfocus.com/archive/1/158959.
• 38: Frasunek, P. 2001b. ports/24733: mars_nwe remote format string vulnerability. http://groups.google.com/groups?q=mars_nwe+vulnerability&hl=en&lr=&ie=UTF-8&oe=UTF-8&selm=9566si%24gpv%241%40FreeBSD.csie.NCTU.edu.tw&rnum=1.
• 39: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 40: Gates, B. 2002. Trustworthy computing. Microsoft internal memo. Available at http://www.theregister.co.uk/content/4/23715.html.
• 41: David Gay , Alex Aiken, Language support for regions, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.70-80, June 2001, Snowbird, Utah, United States
• 42: Gifford, D. K., Jouvelot, P., Lucassen, J. M., and Sheldon, M. A. 1987. FX-87 Reference Manual. Tech. Rep. MIT/LCS/TR-407, MIT Laboratory for Computer Science. Sept.
• 43: David Greenfieldboyce , Jeffrey S. Foster, Visualizing type qualifier inference with Eclipse, Proceedings of the 2004 OOPSLA workshop on eclipse technology eXchange, p.57-61, October 24-24, 2004, Vancouver, British Columbia, Canada [doi>10.1145/1066129.1066141]
• 44: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 45: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Cyclone User''s Manual, Version 0.1.3, Cornell University, Ithaca, NY, 2001
• 46: 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
• 47: Harrelson, C. 2001. Program analysis mode. http://www.cs.berkeley.edu/~chrishtr/pam.
• 48: 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
• 49: Fritz Henglein, Efficient Type Inference for Higher-Order Binding-Time Analysis, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.448-472, August 26-30, 1991
• 50: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 51: Henrion, M. 2000. MUH IRC bouncer remote vulnerability. FreeBSD-SA-00:57. http://www.securityfocus.com/advisories/2741.
• 52: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 53: Susan Horwitz , Thomas Reps , Mooly Sagiv, Demand interprocedural dataflow analysis, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.104-115, October 12-15, 1995, Washington, D.C., United States
• 54: Huuskonen, J. 2000a. Possibility for format char errors in syslog call. https://bugzilla.redhat.com/bugzilla/show_bug.cgi?id=17349.
• 55: Huuskonen, J. 2000b. Some possible format string errors. Linux security audit project mailing list. http://www2.merton.ox.ac.uk/~security/security-audit-200009/0118.html.
• 56: Huuskonen, J. 2000c. syslog(prio, buf) in mars_nwe. Linux security audit project mailing list. http://www2.merton.ox.ac.uk/~security/security-audit-200009/0136.html.
• 57: Johnson, R. and Wagner, D. 2004. Finding user/kernel bugs with type inference. In Proceedings of the 13th Usenix Security Symposium (San Diego, CA).
• 58: Nils Klarlund , Michael I. Schwartzbach, Graph types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.196-205, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158628]
• 59: Larochelle, D. and Evans, D. 2001. Statically detecting likely buffer overflow vulnerabilities. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).
• 60: K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
• 61: Ben Liblit , Alexander Aiken, Type systems for distributed data structures, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.199-213, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325717]
• 62: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 63: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 64: Mars Climate Orbiter Mishap Investigation Board. 1999. Phase I Report. ftp://ftp.hq.nasa.gov/pub/pao/reports/1999/MCO_report.pdf.
• 65: Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.
• 66: Mitchell, J. C. 1991. Type inference with simple subtypes. J. Funct. Prog. 1, 3 (July), 245--285.
• 67: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 68: Mossin, C. 1996. Flow analysis of typed higher-order programs. Ph.D. dissertation. DIKU, Department of Computer Science, University of Copenhagen.
• 69: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 70: Newsham, T. 2000. Format string attacks. http://online.securityfocus.com/guest/3342.
• 71: NIST. 2002. The economic impacts of inadequate infrastructure for software testing. NIST Planning Report 02-3. http://www.nist.gov/director/prog-ofc/report02-3.pdf.
• 72: Odersky, M., Sulzmann, M., and Wehr, M. 1997. Type inference with constrained types. In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages, B. Pierce, Ed.
• 73: Ørbæk, P. and Palsberg, J. 1997. Trust in the λ-calculus. J. Funct. Prog. 3, 2, 75--85.
• 74: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 75: PITAC. 1999. President's Information Technology Advisory Committee Report to the President. http://www.ccic.gov/ac/report.
• 76: Polyvios Pratikakis , Jaime Spacco , Michael Hicks, Transparent proxies for java futures, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 77: Vaughan Pratt , Jerzy Tiuryn, Satisfiability of inequalities in a poset, Fundamenta Informaticae, v.28 n.1-2, p.165-182, Nov. 1996
• 78: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 79: Jakob Rehof , Torben Æ. Mogensen, Tractable Constraints in Finite Semilattices, Proceedings of the Third International Symposium on Static Analysis, p.285-300, September 24-26, 1996
• 80: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 81: Robbins, T. J. 2001. Libformat--Protection against format string attacks. http://www.wiretapped.net/~fyre/software/libformat.html.
• 82: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 83: Savola, P. 2000. Very probable remote root vulnerability in cfengine. BugTraq mailing list. http://www.securityfocus.com/archive/1/136751.
• 84: Shankar, U., Talwar, K., Foster, J. S., and Wagner, D. 2001. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).
• 85: Christian Skalka , Scott Smith, Static enforcement of security with types, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.34-45, September 2000
• 86: Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
• 87: Solberg, K. L. 1995. Annotated type systems for program analysis. Ph.D. dissertation. Aarhus University, Denmark, Computer Science Department.
• 88: Stroustrup, B. 2005. C++ style and technique FAQ. http://www.research.att.com/~bs/bs_faq2.html#constplacement.
• 89: J. Viega , J. T. Bloch , Y. Kohno , G. McGraw, ITS4: A static vulnerability scanner for C and C++ code, Proceedings of the 16th Annual Computer Security Applications Conference, p.257, December 11-15, 2000
• 90: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
• 91: Larry Wall , Mike Loukides, Programming Perl, O'Reilly & Associates, Inc., Sebastopol, CA, 2000
• 92: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]
• 93: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 94: Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948153]
• 95: Yelick, K., Semenzato, L., Pike, G., Miyamoto, C., Liblit, B., Krishnamurthy, A., Hilfinger, P., Graham, S., Gay, D., Colella, P., and Aiken, A. 1998. Titanium: A high-performance Java dialect. In Proceedings of the ACM 1998 Workshop on Java for High-Performance Network Computing. ACM, New York.
• 96: Suan Hsi Yong , Susan Horwitz , Thomas Reps, Pointer analysis for programs with structures and casting, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.91-103, May 01-04, 1999, Atlanta, Georgia, United States
• 97: Xiaolan Zhang , Antony Edwards , Trent Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement, Proceedings of the 11th USENIX Security Symposium, p.33-48, August 05-09, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Design, Experimentation, Languages, Reliability, Theory, Verification

Keywords:
Type qualifiers, const, constraints, security, static analysis, taint, types