Preview

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

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

Использование инвариантов функции высокого уровня для дедуктивной верификации машинного кода

https://doi.org/10.15514/ISPRAS-2019-31(3)-10

Аннотация

Существующие на сегодняшний день инструменты дедуктивной верификации позволяют успешно доказывать корректность функций, написанных на высокоуровневых языках, таких как C или Java. Однако для критического ПО этого может быть недостаточно, поскольку даже полностью верифицированный код не может гарантировать корректной генерации машинного кода компилятором. На данный момент разработчикам таких систем приходится принимать предположение о корректности компилятора, что, однако, является крайне нежелательным, но неизбежным поступком в силу отсутствия полноценных систем формальной верификации машинного кода. Стоит также отметить, что верификация машинного кода человеком напрямую является крайне трудоёмкой задачей из-за высокой сложности и больших объёмов машинного кода. Одним из подходов, позволяющих упростить верификацию машинного кода – является автоматическая дедуктивная верификация с переиспользованием формальной спецификации функции языка высокого уровня. Формальная спецификация функции состоит из спецификации пред- и постусловия, а также инвариантов циклов, позволяющих определить какие условия сохраняются на каждой итерации цикла. При компиляции программы в машинный код пред- и постусловия сохраняются что, однако нельзя сказать об инвариантах циклов. Этот факт является одной из основных проблем автоматической верификации машинного кода с циклами. Другой немаловажной проблемой является то, что локальные переменные функций высокого уровня могут иметь ‘позиции’ как на регистры, так и на память на уровне машинного кода. Если абстрагироваться от конкретного компилятора, то не существует строгих правил сопоставления локальных переменных их позициям, а процедура верификации инвариантов циклов, тем не менее требует того, чтобы локальным переменным были сопоставлены конкретные позиции. В данной работе приводится подход к решению этих проблем, а также рассматриваются альтернативные пути решения, предложенные в аналогичных исследованиях.

Об авторе

Павел Андреевич Путро
Институт системного программирования им. В.П. Иванникова РАН; Национальный исследовательский университет “Высшая школа экономики”
Россия


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

1. . R.W. Floyd. Assigning Meanings to Programs. Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, 19, 1967. P. 19-32. DOI: 10.1090/psapm/019/0235771.

2. . C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 1969. P. 576-585. DOI: 10.1145/363235.363259.

3. . C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, (A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, eds.), IOS Press, Feb. 2009, pp. 825885.

4. . C. Sun, V. Le, Q. Zhang, Z. Su Toward understanding compiler bugs in gcc and llvm. ISSTA 2016, pp. 294-305.

5. . Putro P.A. Combining ACSL Specifications and Machine Code. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 4, 2018. pp. 95-106. DOI: 10.15514/ISPRAS-2018-30(4)-6

6. . M.O. Myreen. Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge, 2009. 131 p.

7. . K. Slind, M. Norrish. A Brief Overview of HOL4. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (LNCS), 5170, 2008. P. 28-32. DOI: 10.1007/978-3-540-71067-7 6.

8. . A. Fox. Formal Specification and Verification of ARM6. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (LNCS), 2758, 2003. P. 25-40. DOI: 10.1007/10930755 2.

9. . K. Crary, S. Sarkar. Foundational Certified Code in a Metalogical Framework. Technical Report CMU-CS-03-108. Carnegie Mellon University, 2003. 19 p.

10. . X. Leroy. Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant. Principles of Programming Languages (POPL), 2006. P. 42-54, DOI: 10.1145/1111037.1111042.

11. . Y. Bertot. A Short Presentation of Coq. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, 5170, 2008. P. 12-16. DOI: 10.1007/978-3-540-71067-7 3.

12. . P. Baudin, P. Cuoq, J.-C. Filliˆatre, C. March´e, B. Monate, Y. Moy, V. Prevosto. ACSL: ANSI/ISO C Specification Language. Version 1.13, 2018. 114 p.

13. . T.M.T. Nguyen, C. March´e. Hardware-Dependent Proofs of Numerical Programs. Certified Programs and Proofs (CPP), 2011. Lecture Notes in Computer Science 7086. P. 314-329. DOI: 10.1007/978-3-642-25379-9 23.

14. . G. Barthe, T. Rezk, A. Saabas. Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust (FAST), 2005. Lecture Notes in Computer Science 3866. P. 112-126. DOI: 10.1007/11679219 9.

15. . MicroTESK Framework – http://www.microtesk.org

16. . M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993. 47 p.

17. . C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard Version 2.6. Release 2017-07-18. 104 p.

18. . JavaScript Object Notation – https://www.json.org/

19. . R. E. Tarjan, Dep-first search and linear graph algorithms SIAM J. Comput., vol. 1, no. 2, pp. 146-160, June 1972.

20. . ocaml-containers library – https://github.com/c-cube/ocaml-containers


Рецензия

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


Путро П.А. Использование инвариантов функции высокого уровня для дедуктивной верификации машинного кода. Труды Института системного программирования РАН. 2019;31(3):123-134. https://doi.org/10.15514/ISPRAS-2019-31(3)-10

For citation:


Putro P.A. Applying High-Level Function Loop Invariants for Machine Code Deductive Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(3):123-134. https://doi.org/10.15514/ISPRAS-2019-31(3)-10



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


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