Type checking beyond type checkers, via slice & run
Authors: 
Justus Adam, 
Stephen KellAuthors Info & Claims
Pages 23 - 29
Abstract
Type checkers are the most commonly used form of static analysis, but their design is coupled to the rest of the language, making it hard or impossible to bring new kinds of reasoning to existing, unmodified code. We propose a novel approach to checking advanced type invariants and properties in unmodified source code, while approaching the speed and ease of simple, syntax directed type checkers.
The insight is that by combining a deep program analysis (symbolic execution) with a cheaper program abstraction (based on program slicing), it appears possible to reconstitute type-checking in the context of an underapproximate analysis. When the program's 'type level' can be opportunistically disentangled from the 'value level', this is done by the program abstraction step, in some cases removing the underapproximation.
We implement a simple prototype that demonstrates this idea by checking the safety of generic pointers in C, pointing to benefits such as safe homogeneous and heterogeneous generic data structures.
References
[1]
Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamarić, and Leonid Ryzhyk. 2017. System Programming in Rust: Beyond Safety. In Proceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS '17). Association for Computing Machinery, New York, NY, USA, 156-161. htps: //doi.org/10.1145/3102980.3103006
[2]
Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. 2007. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Computer Aided Veriifcation (Lecture Notes in Computer Science), Werner Damm and Holger Hermanns (Eds.). Springer, Berlin, Heidelberg, 504-518. htps: //doi.org/10.1007/978-3-540-73368-3_51
[3]
Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, W. Rance Cleaveland (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 193-207.
[4]
Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT: a Formal System for Testing and Debugging Programs by Symbolic Execution. In Proceedings of the International Conference on Reliable Software. Association for Computing Machinery, New York, NY, USA, 234-245. htps://doi.org/10.1145/800027.808445
[5]
Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, USA, 209-224.
[6]
L. A. Clarke. 1976. A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering 2, 3 (May 1976 ), 215-222. htps://doi.org/10.1109/TSE. 1976.233817
[7]
Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. 2007. Dependent Types for Low-Level Programming. In Programming Languages and Systems, Rocco De Nicola (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 520-535.
[8]
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C. Lecture Notes in Computer Science ( 2012 ), 233-247. htps://doi.org/10.1007/978-3-642-33826-7_16
[9]
Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O'Hearn. 2019. Scaling Static Analyses at Facebook. Commun. ACM 62, 8 ( July 2019 ), 62-70. htps://doi.org/10.1145/3338112
[10]
Brian Hackett and Alex Aiken. 2011. Inferring Data Polymorphism in Systems Code. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE '11). Association for Computing Machinery, Szeged, Hungary, 332-342. htps://doi.org/10.1145/2025113.2025159
[11]
Mark Harman, David Binkley, and Sebastian Danicic. 2003. Amorphous Program Slicing. Journal of Systems and Software 68, 1 (Oct. 2003 ), 45-64. htps://doi.org/10.1016/S0164-1212 ( 02 ) 00135-8
[12]
Trevor Jim, J Gregory Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In USENIX Annual Technical Conference, General Track. 275-288.
[13]
Stefan Kahrs. 1992. Polymorphic Type Checking by Interpretation of Code. Technical Report. University of Edinburgh, Laboratory for Foundations of Computer Science.
[14]
Stephen Kell. 2015. Towards a Dynamic Object Model within Unix Processes. In 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) (Onward! 2015 ). Association for Computing Machinery, New York, NY, USA, 224-239. htps://doi.org/10.1145/2814228.2814238
[15]
Stephen Kell. 2016. Dynamically Diagnosing Type Errors in Unsafe Code. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016 ). Association for Computing Machinery, New York, NY, USA, 800-819. htps://doi.org/10.1145/2983990.2983998
[16]
Yit Phang Khoo, Bor-Yuh Evan Chang, and Jefrey S. Foster. 2010. Mixing Type Checking and Symbolic Execution. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '10). Association for Computing Machinery, New York, NY, USA, 436-447. htps://doi.org/10.1145/1806596.1806645
[17]
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 ( July 1976 ), 385-394. htps://doi.org/10.1145/360248. 360252
[18]
Amit Levy, Bradford Campbell, Branden Ghena, Pat Pannuto, Prabal Dutta, and Philip Levis. 2017. The Case for Writing a Kernel in Rust. In Proceedings of the 8th Asia-Pacific Workshop on Systems (APSys '17). Association for Computing Machinery, New York, NY, USA, Article 1. htps://doi.org/10.1145/3124680.3124717
[19]
Luis Mastrangelo, Matthias Hauswirth, and Nathaniel Nystrom. 2019. Casting about in the Dark: An Empirical Study of Cast Operations in Java Programs. Proceedings of the ACM on Programming Languages 3, OOPSLA (Oct. 2019 ), 158 : 1-158 : 31. htps://doi.org/10.1145/3360584
[20]
George C. Necula, Scott McPeak, and Westley Weimer. 2002. CCured: Type-Safe Retrofitting of Legacy Code. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '02). Association for Computing Machinery, New York, NY, USA, 128-139. htps://doi.org/10.1145/503272.503286
[21]
Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08). Association for Computing Machinery, Tucson, AZ, USA, 159-169. htps: //doi.org/10.1145/1375581.1375602
[22]
Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael Hicks. 2019. Achieving Safety Incrementally with Checked C. In Principles of Security and Trust, Flemming Nielson and David Sands (Eds.). Springer International Publishing, Cham, 76-98.
[23]
Yan Shoshitaishvili, Ruoyu Wang, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. 2015. Firmalice-Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware. In Proceedings 2015 Network and Distributed System Security Symposium. Internet Society, San Diego, CA. htps://doi.org/10.14722/ndss. 2015.23294
[24]
Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. Lecture Notes in Computer Science ( 2007 ), 2-27. htps://doi.org/10.1007/978-3-540-73589-2_2
[25]
Jiri Slaby, Jan Strejček, and Marek Trtík. 2013. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution. In Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A. Smolka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 630-632.
[26]
Alexander J. Summers, Sophia Drossopoulou, and Peter Müller. 2009. The Need for Flexible Object Invariants. In International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO '09). Association for Computing Machinery, New York, NY, USA, Article 6. htps://doi.org/10.1145/1562154.1562160
[27]
Frank Tip. 1994. A Survey of Program Slicing Techniques. Technical Report. CWI (Centre for Mathematics and Computer Science), Netherlands.
[28]
Mark Weiser. 1984. Program Slicing. IEEE Transactions on Software Engineering SE-10, 4 ( July 1984 ), 352-357. htps://doi.org/10.1109/tse. 1984.5010248
[29]
Dengping Zhu and Hongwei Xi. 2005. Safe Programming with Pointers Through Stateful Views. In Practical Aspects of Declarative Languages (Lecture Notes in Computer Science), Manuel V. Hermenegildo and Daniel Cabeza (Eds.). Springer, Berlin, Heidelberg, 83-97. htps://doi. org/10.1007/978-3-540-30557-6_8
Index Terms
- Type checking beyond type checkers, via slice & run
Recommendations
Unifying type checking and property checking for low-level code
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type ...
Type inference and strong static type checking for Promela
The Spin model checker and its specification language Promela have been used extensively in industry and academia to check the logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an ...
Unifying type checking and property checking for low-level code
POPL '09We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2020 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 November 2020
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- National Cyber Security Centre
Conference
SPLASH '20
Sponsor:
SPLASH '20: Conference on Systems, Programming, Languages, and Applications, Software for Humanity
November 17, 2020
Virtual, USA
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 337Total Downloads
- Downloads (Last 12 months)85
- Downloads (Last 6 weeks)9
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in