Martin Kellogg
Michael D. Ernst
ABSTRACT
In languages like C, out-of-bounds array accesses lead to security vulnerabilities and crashes. Even in managed languages like Java, which check array bounds at run time, out-of-bounds accesses cause exceptions that terminate the program.
We present a lightweight type system that certifies, at compile time, that array accesses in the program are in-bounds. The type system consists of several cooperating hierarchies of dependent types, specialized to the domain of array bounds-checking. Programmers write type annotations at procedure boundaries, allowing modular verification at a cost that scales linearly with program size.
We implemented our type system for Java in a tool called the Index Checker. We evaluated the Index Checker on over 100,000 lines of open-source code and discovered array access errors even in well-tested, industrial projects such as Google Guava.
- 2002. PLDI 2002: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. Berlin, Germany.Google Scholar
- Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. 2014. The KeY platform for verification and analysis of Java programs. In VSTTE 2014: 6th Working Conference on Verified Software: Theories, Tools, Experiments. Vienna, Austria, 55–71.Google ScholarCross Ref
- Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, and William Pugh. 2008. Using Static Analysis to Find Bugs. IEEE Software 25, 5 (2008), 22–29. Google ScholarDigital Library
- Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K Rustan M Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In International Symposium on Formal Methods for Components and Objects. Springer, 364–387. Google ScholarDigital Library
- Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Marcelo d’Amorim, and Michael D. Ernst. 2015. Static analysis of implicit control flow: Resolving Java reflection and Android intents. In ASE 2015: Proceedings of the 30th Annual International Conference on Automated Software Engineering. Lincoln, NE, USA, 669–679.Google Scholar
- Al Bessey, Ken Block, Benjamin Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson R. Engler. 2010. A few billion lines of code later: Using static analysis to find bugs in the real world. Commun. ACM 53, 2 (2010), 66–75. Google ScholarDigital Library
- Rastislav Bodík, Rajiv Gupta, and Vivek Sarkar. 2000. ABCD: Eliminating Array Bounds Checks on Demand. In PLDI 2000: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation. Vancouver, BC, Canada, 321–333. Google ScholarDigital Library
- Dan Brotherston, Werner Dietl, and Ondřej Lhoták. 2017. Granullar: gradual nullable types for Java. In CC 2017: 26th International Conference on Compiler Construction. Austin, TX, USA, 87–97. Google ScholarDigital Library
- Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. 2005. An overview of JML tools and applications. Software Tools for Technology Transfer 7, 3 (June 2005), 212–232.Google ScholarCross Ref
- Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. 2007. Dependent types for low-level programming. In ESOP 2007: 16th European Symposium on Programming. Braga, Portugal, 520–535. Google ScholarDigital Library
- Patrick Cousot. 1997. Types as abstract interpretations. In POPL ’97: Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Paris, France, 316–331. Google ScholarDigital Library
- Al Danial. Accessed June 7, 2018. cloc. http://cloc.sourceforge.net/.Google Scholar
- Oege De Moor, Damien Sereni, Mathieu Verbaere, Elnar Hajiyev, Pavel Avgustinov, Torbjörn Ekman, Neil Ongkingco, and Julian Tibble. 2007.. ql: Objectoriented queries made easy. In International Summer School on Generative and Transformational Techniques in Software Engineering. Springer, Braga, Portugal, 78–133.Google Scholar
- Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In TACAS 2008: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Budapest, Hungary, 337–340. Google ScholarDigital Library
- David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. 1998. Extended Static Checking. SRC Research Report 159. Compaq Systems Research Center.Google Scholar
- Archibald Samuel Elliott, Andrew Ruef, Michael Hicks, and David Tarditi. {n. d.}. Checked C: Making C safe by extension.Google Scholar
- Michael Ernst. Accessed June 7, 2018. plume-lib. https://github.com/mernst/ plume-lib.Google Scholar
- Michael D. Ernst. 2003. Static and dynamic analysis: Synergy and duality. In WODA 2003: Workshop on Dynamic Analysis. Portland, OR, USA, 24–27.Google Scholar
- David Evans. 1996. Static detection of dynamic memory errors. In PLDI ’96: Proceedings of the SIGPLAN ’96 Conference on Programming Language Design and Implementation. Philadelphia, PA, USA, 44–53. Google ScholarDigital Library
- Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. 2010. Embedded contract languages. In SAC 2010: Proceedings of the 2010 ACM Symposium on Applied Computing. Sierre, Switzerland, 2103–2110. Google ScholarDigital Library
- Manuel Fähndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In International Conference on Formal Verification of Object-Oriented Software. Paris, France, 10–30. Google ScholarDigital Library
- James Finkle and Supriya Kurane. 2014. U.S. hospital breach biggest yet to exploit Heartbleed bug: expert. https://www.reuters.com/article/ us-community-health-cybersecurity-idUSKBN0GK0H420140820.Google Scholar
- Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. 2002. Extended static checking for Java, See { 1 }, 234–245. Google ScholarDigital Library
- Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. 2002. Flow-sensitive type qualifiers, See { 1 }, 1–12. Google ScholarDigital Library
- David Gilbert. Accessed June 7, 2018. JFreeChart. https://github.com/jfree/ jfreechart.Google Scholar
- Alberto Goffi, Alessandra Gorla, Andrea Mattavelli, Mauro Pezzè, and Paolo Tonella. 2014. Search-based synthesis of equivalent method sequences. In FSE 2014: Proceedings of the ACM SIGSOFT 22nd Symposium on the Foundations of Software Engineering. Hong Kong, 366–376. Google ScholarDigital Library
- Google Inc. Accessed June 7, 2018. Google Guava. https://github.com/google/ guava.Google Scholar
- Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang. 2006. Modular checking for buffer overflows in the large. In ICSE 2006, Proceedings of the 28th International Conference on Software Engineering. Shanghai, China, 232–241. Google ScholarDigital Library
- Reed Hastings and Bob Joyce. 1992. Purify: A tool for detecting memory leaks and access errors in C and C++ programs. In USENIX: Proceedings of the Winter 1992 USENIX Conference. San Francisco, CA, USA, 125–138.Google Scholar
- Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP 2015, Proceedings of the 23rd ACM Symposium on Operating Systems Principles. Monterey, CA, USA, 1–17. Google ScholarDigital Library
- Trevor Jim, J. Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A safe dialect of C. In USENIX 2002: Proceedings of the 2002 USENIX Annual Technical Conference. Monterey, CA, USA, 275–288. Google ScholarDigital Library
- Cliff B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 5, 4 (1983), 596–619. Google ScholarDigital Library
- Vincent Laviron and Francesco Logozzo. 2011. SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities. Software Tools for Technology Transfer 13, 6 (2011), 585–601. Google ScholarDigital Library
- Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, Daniel M. Zimmerman, and Werner Dietl. 2013. JML Reference Manual.Google Scholar
- K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In LPAR 2010: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Dakar, Senegal, 348–370. Google ScholarDigital Library
- K. Rustan M. Leino and Greg Nelson. 1998. An extended static checker for Modula-3. In CC ’98: Compiler Construction: 7th International Conference. Lisbon, Portugal, 302–305. Google ScholarDigital Library
- K. Rustan M. Leino and Clément Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV 2016: 28th International Conference on Computer Aided Verification. Toronto, Canada, 361–381.Google Scholar
- Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In SAC 2008: Proceedings of the 2008 ACM Symposium on Applied Computing. Fortaleza, Ceará, Brazil, 184–188. Google ScholarDigital Library
- Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2015. Everything you want to know about pointer-based checking. In SNAPL 2015: the Inaugural Summit oN Advances in Programming Languages. Asilomar, CA, USA, 190–208.Google Scholar
- George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. 2005. CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27, 3 (2005), 477–526. Google ScholarDigital Library
- Nicholas Nethercote and Julian Seward. 2007. Valgrind: A Framework for Heavyweight Dynamic Binary Insrumentation. In PLDI 2007: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. San Diego, CA, USA, 89–100. Google ScholarDigital Library
- Serkan Özkan. 2018. CVE Details. https://www.cvedetails.com/ vulnerabilities-by-types.php. Summary of http://cve.mitre.org/.Google Scholar
- Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. 2008. Practical pluggable types for Java. In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis. Seattle, WA, USA, 201–212. Google ScholarDigital Library
- Frank Pfenning. 1992. Dependent types in logic programming. In Types in Logic Programming, Frank Pfenning (Ed.). MIT Press, Cambridge, MA, Chapter 10, 285–311.Google Scholar
- William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings, Supercomputing ’91. Albuquerque, New Mexico, 4–13. Google ScholarDigital Library
- Feng Qian, Laurie Hendren, and Clark Verbrugge. 2002. A comprehensive approach to array bounds check elimination for Java. In CC 2002: Compiler Construction: 11th International Conference. Grenoble, France, 325–341. Google ScholarDigital Library
- Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In PLDI 2008: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. Tucson, AZ, USA, 159–169. Google ScholarDigital Library
- Joseph Santino. 2016. Enforcing correct array indexes with a type system. In FSE 2016: Proceedings of the ACM SIGSOFT 24th Symposium on the Foundations of Software Engineering. Seattle, WA, USA, 1142–1144. Google ScholarDigital Library
- Norihisa Suzuki and Kiyoshi Ishihata. 1977. Implementation of an array bound checker. In POPL ’77: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages. Los Angeles, CA, 132–143. Google ScholarDigital Library
- David Tarditi. 2016. Extending C with bounds safety. https://github.com/ Microsoft/checkedc/releases/download/v0.6-final/checkedc-v0.6.pdf. Accessed: 2017-05-11. ISSTA’18, July 16–21, 2018, Amsterdam, Netherlands Martin Kellogg, Vlastimil Dort, Suzanne Millstein, and Michael D. ErnstGoogle Scholar
- Shiyi Wei, Piotr Mardziel, Andrew Ruef, Jeffrey S. Foster, and Michael Hicks. 2018. Evaluating design tradeoffs in numeric static analysis for Java. In ESOP 2018: 27th European Symposium on Programming. Thessaloniki, Greece.Google ScholarCross Ref
- Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. ACM SIGPLAN Notices 33, 5 (1998), 249–257. Google ScholarDigital Library
Index Terms
- Lightweight verification of array indexing
Recommendations
Scalability and precision by combining expressive type systems and deductive verification
Type systems and modern type checkers can be used very successfully to obtain formal correctness guarantees with little specification overhead. However, type systems in practical scenarios have to trade precision for decidability and scalability. Tools ...
JavaCOP: Declarative pluggable types for java
Pluggable types enable users to enforce multiple type systems in one programming language. We have developed a suite of tools, called the JavaCOP framework, that allows developers to create pluggable type systems for Java. JavaCOP provides a simple ...
Building and using pluggable type systems
FSE '10: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineeringAre you a practitioner who is tired of null pointer exceptions, unintended side effects, SQL injections, concurrency errors, mistaken equality tests, and other run-time errors that appear during testing or in the field? A pluggable type system can ...
Comments