Mechanically Proved Practical Local Null Safety
https://doi.org/10.15514/ISPRAS-2016-28(5)-2
Abstract
Null pointer dereferencing is a well-known bug in object-oriented programs. It can be avoided by adding special validity rules to a language in which programs are written. Are the rules sufficient to ensure absence of such exceptions? This work focuses on null safety for intra-procedural context where no additional type annotations are needed and formalizes the rules in Isabelle/HOL proof assistant. It then proves null-safety preservation theorem for big-step semantics in a computer-checkable way. Finally, it demonstrates that with such rules null-safe and null-unsafe semantics are equivalent.
References
1. Nada Amin and Tiark Romp. “Type Soundness Proofs with Definitional Interpreters”. In: OOPSLA. 2016. url: https://www.cs.purdue.edu/homes/ rompf/papers/amin-draft2016a.pdf. Submitted.
2. Mike Barnett et al. “Specification and Verification: The Spec# Experience”. In: Commun. ACM 54.6 (June 2011). Ed. by Moshe Y. Vardi, pp. 81–91. issn: 0001-0782. doi: 10.1145/1953122.1953145.
3. Common Vulnerabilities and Exposures. http://cve.mitre.org/. 2016. (Visited on 2016-05-25).
4. Ecma International. ECMA-367: Eiffel analysis, design and programming language. 2nd. Geneva, Switzerland: Ecma International, June 2006. url: http://www.ecma-international.org/publications/standards/Ecma367.htm.
5. Eiffel Software. EiffelStudio 7.3 Releases. https://dev.eiffel.com/ EiffelStudio_7.3_Releases. July 2013. (Visited on 2016-05-14).
6. Eiffel Software. EiffelStudio 16.05 Releases. https://dev.eiffel.com/ EiffelStudio_16.05_Releases. July 2016. (Visited on 2016-09-15).
7. James Gosling et al. The Java Language Specification, Java SE 8 Edition. 1st. Addison-Wesley Professional, 2014. isbn: 9780133900699.
8. Tony Hoare. “Null references: The billion dollar mistake”. In: Presentation at QCon London (2009).
9. Projects – Isabelle Community wiki. https://isabelle.in.tum.de/ community/Projects. Apr. 2016. (Visited on 2016-09-15).
10. ISO. ISO/IEC 14882:2014(E): Information technology — Programming languages — C++. 4th. Geneva, Switzerland: International Organization for Standardization, Dec. 15, 2014.
11. Gerwin Klein. “Verified Java Bytecode Verification”. PhD thesis. Institut für Informatik, Technische Universität München, 2003. url: http://www4.in. tum.de/~kleing/diss/.
12. Gerwin Klein and Tobias Nipkow. “A Machine-checked Model for a Java-like Language, Virtual Machine, and Compiler”. In: ACM Trans. Program. Lang. Syst. 28.4 (July 2006), pp. 619–695. issn: 0164-0925. doi: 10.1145/1146809.1146811.
13. Andreas Lochbihler. “A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler”. PhD thesis. Karlsruher Institut für Technologie, Fakultät für Informatik, July 2012. doi: 10.5445/KSP/1000028867. url: http://digbib.ubka.unikarlsruhe.de/volltexte/1000028867.
14. Bertrand Meyer. Targeted expressions: safe object creation with void safety. http://se.ethz.ch/~meyer/publications/online/targeted.pdf. July 2012. (Visited on 2016-09-24).
15. Bertrand Meyer, Alexander Kogtenkov, and Emmanuel Stapf. “Avoid a Void: The Eradication of Null Dereferencing”. In: Reflections on the Work of C.A.R. Hoare. Ed. by A.W. Roscoe, Cliff B. Jones, and Kenneth R. Wood. History of Computing. Springer London, 2010, pp. 189–211. isbn: 978-1-84882-912-1. doi: 10.1007/978-1-84882-912-1_9.
16. Benjamin Morandi et al. “Prototyping a Concurrency Model”. In: Proceedings of the 2013 13th International Conference on Application of Concurrency to System Design. ACSD ’13. Washington, DC, USA: IEEE Computer Society, 2013, pp. 170–179. isbn: 978-0-7695-5035-0. doi: 10.1109/ACSD.2013.21. url: http://dx.doi.org/10.1109/ACSD.2013.21.
17. Robert Morgan. Building an Optimizing Compiler. Newton, MA, USA: Digital Press, 1998. isbn: 1-55558-179-X.
18. Steven S. Muchnick. Advanced Compiler Design and Implementation. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 1997. isbn: 1-55860320-4.
19. Scott Owens et al. “Functional Big-Step Semantics”. In: Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Ed. by Peter Thiemann. Berlin, Heidelberg: Springer Berlin Heidelberg, 2016, pp. 589–615. isbn: 978-3-662-49498-1. doi: 10.1007/978-3-662-494981_23. url: http://dx.doi.org/10.1007/978-3-662-49498-1_23.
20. Jeremy Siek. Big-step, diverging or stuck? http://siek.blogspot.ch/2012/07/big-step-diverging-or-stuck.html. July 2012. (Visited on 2016-09-15).
21. Jeremy Siek. Type Safety in Three Easy Lemmas. http://siek.blogspot.ch/2013/05/type-safety-in-three-easy-lemmas.html. May 2013. (Visited on 2016-09-15).
22. Alexander J. Summers and Peter Müller. “Freedom Before Commitment: A Lightweight Type System for Object Initialisation”. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications. Ed. by . OOPSLA ’11. Portland, Oregon, USA: ACM,2011,pp.1013–1032.isbn:978-1-4503-0940-0.doi:10.1145/2048066.2048142.
Review
For citations:
Kogtenkov A.V. Mechanically Proved Practical Local Null Safety. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(5):27-54. https://doi.org/10.15514/ISPRAS-2016-28(5)-2
Email this article 