Обзор подходов к моделированию памяти в инструментах статической верификации
https://doi.org/10.15514/ISPRAS-2017-29(1)-12
Аннотация
В статье приведен обзор существующих подходов к моделированию памяти Си-программ в инструментах статической верификации. Обозначены основные проблемы, возникающие при разработке моделей памяти для языка Си. В обзоре рассматриваются две основные группы моделей памяти в зависимости от полноты поддержки областей памяти наперед не ограниченного размера. Среди моделей для ограниченных областей памяти рассматриваются модель, использующая результаты предварительного анализа алиасов, и модель на основе слабейших предусловий, использующая теорию неинтерпретируемых функций и логику первого порядка. Среди моделей для областей памяти наперед не ограниченного размера рассматривается типизированная модель, модель Бурсталла-Борната, модель с регионами и полная модель памяти для теории интерпретируемых множеств элементов списков, использованная ранее в инструменте дедуктивной верификации HAVOC.
Список литературы
1. Leonardo de Moura, Nikolaj Bjørner. Satisfiability modulo theories: An appetizer. In Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods (SBMF 2009). Gramado, Brazil, August 19–21, 2009. Revised Selected Papers, Lecture Notes in Computer Science, vol. 5902, pp. 23–36. Springer, 2009.
2. Sascha Böhme, Michał Moskal. Heaps and Data Structures: A Challenge for Automated Provers. In Nikolaj Børner, Viorica Sofronie-Stokkermans, eds. Automated Deduction. Lecture Notes in Computer Science, vol. 6803, pp. 177–191. Springer, 2011.
3. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith. Counterexample-Guided Abstraction Refinement. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV '00), E. Allen Emerson, A. Prasad Sistla (Eds.). Springer-Verlag, London, UK, pp. 154–169, 2000.
4. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS, vol. 1579, pp. 193–207. Springer-Verlag, 1999.
5. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar. The software model checker Blast: Applications to software engineering. International Journal on Software Tools for Technology Transfer, October 2007, vol. 9, issue 5, pp. 505–525.
6. Mary Sheeran, Satnam Singh, Gunnar Stålmarck. Checking Safety Properties Using Induction and a SAT-Solver. Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1954, pp. 127–144.
7. Susanne Graf, Hassen Saïdi. Construction of abstract state graphs with PVS. Proceedings of International Conference on Computer Aided Verification, 1997. LNCS, vol. 1254, pp. 72–83. Springer, Berlin Heidelberg, 1997.
8. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '04). SIGPLAN Notes, vol. 39, no. 1, pp. 232–244. ACM, New York, NY, USA. 2004.
9. Aaron R. Bradley. SAT-based model checking without unrolling. In Proceedings of the 12th International conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11), Ranjit Jhala, David Schmidt (Eds.), Springer-Verlag, Berlin, Heidelberg, pp. 70–87, 2011.
10. Corina S. Păsăreanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, Neha Rungta. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, 2013, vol. 20, no. 3, pp. 391–425.
11. В. К. Кошелев, В. Н. Игнатьев, А. И. Борзилов. Инфраструктура статического анализа программ на языке C#. Труды ИСП РАН, том 28, вып. 1, стр. 21–40. 2016. DOI: 10.15514/ISPRAS-2016-28(1)-2.
12. Hoare C. A. R. An Axiomatic Basis for Computer Programming. Commun. ACM., 1969, vol. 12, no. 10, pp. 576–580.
13. Robert W. Floyd. Assigning meanings to programs. In Proceedings of the Symposium in Applied Mathematics, vol. XIX, pp. 19–32. American Mathematical Society, April 1967.
14. Edsger W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation of programs. Communications of the ACM. 1975, vol. 18, no. 8, pp. 453–457.
15. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. LICS ’02. Washington, DC, USA: IEEE Computer Society, 2002, pp. 55–74.
16. François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Why3: Shepherd Your Herd of Provers. Boogie 2011: First International Workshop on Intermediate Verification Languages. Wrocław, Poland. 2011, pp. 53 – 64.
17. K. Rustan M. Leino. Dafny: an automatic program verifier for functional correctness. In Proceedings of the 16th international conference on Logic for programming, artificial intelligence, and reasoning (LPAR'10). Edmund M. Clarke, Andrei Voronkov (Eds.). Springer-Verlag, Berlin, Heidelberg, pp. 348–370, 2010.
18. Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Tiu. Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006, LNCS, vol. 3920, pp. 167–181. Berlin, Heidelberg: Springer-Verlag, 2006.
19. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Thery, Benjamin Werner. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. Proceedings of the First International Conference on Certified Programs and Proofs. CPP’11. Berlin, Heidelberg: Springer-Verlag, pp. 135–150, 2011.
20. Benjamin C. Pierce. Types and Programming Languages. Chapter I. Untyped Systems. The MIT Press, 2002.
21. Robert D. Tennent. The denotational semantics of programming languages. Commun. ACM 19, vol. 8 (August 1976), pp. 437–453, 1976.
22. Мандрыкин М. У. Моделирование памяти Си-программ для инструментов статической верификации на основе SMT-решателей. Диссертация на соискание ученой степени кандидата физико-математических наук. Институт системного программирования РАН, октябрь, 2016.
23. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar. Lazy abstraction. Symposium on Principles of Programming Languages, pp. 58–70, ACM Press, 2002.
24. Pavel Shved, Mikhail Mandrykin, Vadim Mutilin. Predicate Analysis with BLAST 2.7. Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2012 (TACAS’12), LNCS, vol. 7214,. pp. 525–527.
25. Pavel Shved, Vadim S. Mutilin, Mikhail U. Mandrykin. Experience of improving the Blast static verification tool. Programming and Computer Software, vol. 38, issue 3, pp. 134–142, June 2012. DOI: 10.1134/S0361768812030061.
26. Мутилин В.С. Верификация драйверов операционной системы Linux при помощи предикатных абстракций. Диссертация на соискание ученой степени кандидата физико-математических наук. Институт системного программирования РАН. 2012. ноябрь.
27. Lars O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, University of Copenhagen, DIKU, 1994.
28. Marc Berndl, Ondřej Lhoták, Feng Qian, Laurie Hendren, Navindra Umanee. Points-to Analysis using BDDs. SIGPLAN Notes, vol. 38, no. 5, pp. 103–114. ACM. New York, NY, USA. May 2003.
29. Edsger W. Dijkstra, Carel S. Schölten. Predicate Calculus and Program Semantics. The strongest postcondition, pp. 209–215. Springer New York. 1990.
30. Alexey Khoroshilov, Vadim Mutilin, Eugene Novikov, Pavel Shved, Alexander Strakh. Towards An Open Framework for C Verification Tools Benchmarking. Proceedings of the 8th international conference on Perspectives of System Informatics (PSI’11), LNCS, vol. 7162, pp. 179–192, 2011.
31. Thomas Ball, Ella Bounimova, Vladimir Levin, Leonardo de Moura. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. March 2010. MSR TR-2010-24.
32. Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin. SLAM2: Static driver verification with under 4% false alarms. Formal Methods in Computer-Aided Design (FMCAD), 2010, pp. 35–42.
33. Thomas Ball, Todd Millstein, Sriram K. Rajamani. Polymorphic Predicate Abstraction. ACM Trans. Program. Lang. Syst., vol. 27, no. 2, March 2005, pp. 314–343. ACM, New York, NY, USA. 2005.
34. Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner. Thorough Static Analysis of Device Drivers. Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006. (EuroSys '06) Leuven, Belgium, pp. 73–85. ACM. New York, NY, USA. 2006.
35. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies. VCC: A Practical System for Verifying Concurrent C. Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pp. 23–42. Springer-Verlag. Berlin, Heidelberg. 2009.
36. Ernie Cohen, Michał Moskal, Stephan Tobies, Wolfram Schulte. A Precise Yet Efficient Memory Model For C. Electron. Notes Theor. Comput. Sci., October, 2009, vol. 254, pp. 85–103. Elsevier Science Publishers B. V., Amsterdam, The Netherlands. 2009.
37. Gordon D. Plotkin. A structural approach to operational semantics. Computer Science Department, Aarhus University. Aarhus, Denmark. Internal Report DAIMI FN-19. 1981.
38. Мандрыкин М. У., Хорошилов А. В. Анализ регионов для дедуктивной верификации Си-программ. Программирование, 2016, № 5, стр. 3–29.
39. Rodney M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine intelligence, vol. 7, no. 3, pp. 23–50, 1972.
40. Richard Bornat. Proving Pointer Programs in Hoare Logic. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC '00), pp. 102–126. Springer-Verlag. London, UK, 2000.
41. Thierry Hubert, Claude Marché. Separation Analysis for Deductive Verification. Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007, pp. 81–93.
42. Yannick Moy. Union and Cast in Deductive Verification. Proceedings of the C/C++ Verification Workshop. Technical Report ICIS-R07015, pp. 1–16. Radboud University Nijmegen, July, 2007.
43. Мандрыкин М.У., Хорошилов А.В. Высокоуровневая модель памяти промежуточного языка Jessie с поддержкой произвольного приведения типов указателей. Программирование, 2015, т. 41, № 4, стр. 23–29.
44. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski. Frama-C: A Software Analysis Perspective. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. SEFM'12. Thessaloniki, Greece. 2012. Lecture Notes in Computer Science, vol. 7504, pp. 233–247. Springer-Verlag. Berlin, Heidelberg. 2012.
45. Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis. Université Paris-Sud. January, 2009.
46. Jean-Christophe Filliâtre, Claude Marché. Multi-prover Verification of C Programs. In Proceedings of Formal Methods and Software Engineering: 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8–12, 2004. LNCS, vol. 3308, pp. 15–29. Springer Berlin Heidelberg. 2004.
47. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, vol. 17, no. 3, pp. 348–375. December, 1978.
48. Jean-Christophe Filliâtre, Andrei Paskevich. Why3: Where Programs Meet Provers. Proceedings of the 22Nd European Conference on Programming Languages and Systems. ESOP'13. Rome, Italy. LNCS, vol. 7792, pp. 125–128. Springer-Verlag.
49. https://www.microsoft.com/en-us/research/project/havoc/
50. Shuvendu Lahiri, Shaz Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '08), pp. 171–182. ACM, New York, NY, USA. 2008.
51. Aharon Abadi, Alexander Rabinovich, Mooly Sagiv. Decidable fragments of many-sorted logic. Journal of Symbolic Computation, vol. 45, issue 2, pp. 153–172, February 2010.
52. Yeting Ge, Leonardo Moura. Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV '09). LNCS, vol. 5643, pp. 306–320. Springer-Verlag, Berlin, Heidelberg, 2009.
Рецензия
Для цитирования:
Мандрыкин М.У., Мутилин В.С. Обзор подходов к моделированию памяти в инструментах статической верификации. Труды Института системного программирования РАН. 2017;29(1):195-230. https://doi.org/10.15514/ISPRAS-2017-29(1)-12
For citation:
Mandrykin M.U., Mutilin V.S. Survey of memory modeling methods in static verification tools. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(1):195-230. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(1)-12
Послать статью по эл. почте 