Preview

Труды Института системного программирования РАН

Расширенный поиск

Автоматическое доказательство безопасности локальных пустых указателей

https://doi.org/10.15514/ISPRAS-2016-28(5)-2

Полный текст:

Аннотация

Разыменование пустого указателя - это хорошо известная ошибка, встречающаяся в объектно-ориентированных программах. Ее можно избежать путем добавления к языку, на котором пишется программа, специальных правил приложимости. Достаточно ли этих правил для гарантии отсутствия таких исключительных ситуаций? Данная статья посвящена безопасности пустых указателей во внутрипроцедурном контексте, в котором не требуются какие-либо дополнительные аннотации. Правила формализуются в системе автоматического доказательства теорем Isabelle/HOL. Затем доказывается теорема о сохранении безопасности пустых указателей в крупношаговой семантике. Наконец, демонстрируется, что при наличии таких правил семантики с безопасностью пустых указателей и без нее эквивалентны.

Об авторе

А. В. Когтенков
ETH Zürich
Швейцария


Список литературы

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.


Для цитирования:


Когтенков А.В. Автоматическое доказательство безопасности локальных пустых указателей. Труды Института системного программирования РАН. 2016;28(5):27-54. https://doi.org/10.15514/ISPRAS-2016-28(5)-2

For citation:


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

Просмотров: 242


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)