Архитектура системы дедуктивной верификации машинного кода
Илья Владимирович ГЛАДЫШЕВ,
Александр Сергеевич КАМКИН,
Артем Михайлович КОЦЫНЯК,
Павел Андреевич ПУТРО,
Алексей Владимирович ХОРОШИЛОВ https://doi.org/10.15514/ISPRAS-2020-32(3)-1
Аннотация
В последние годы ИСП РАН разрабатывает систему дедуктивной верификации машинного (бинарного) кода. Мотивация понятна: современные компиляторы, такие как GCC и Clang/LLVM, не застрахованы от ошибок; тем самым, проверка корректности сгенерированного кода (хотя бы для компонентов с повышенными требованиями к надежности и безопасности) не является лишней. Ключевая особенность предлагаемого подхода состоит в возможности переиспользования формальных спецификаций (пред- и постусловий, инвариантов циклов, лемм и т.п.) уровня исходного кода для верификации машинного кода. Инструмент основан на формальной спецификации системы команд и обеспечивает высокий уровень автоматизации: он дизассемблирует машинный код, извлекая его семантику, адаптирует высокоуровневые спецификации для машинного кода и генерирует условия верификации. Система использует ряд сторонних компонентов, включая анализатор исходного кода (Frama-C), анализатор машинного кода (MicroTESK) и SMT-решатель (СVC4). Модульная архитектура позволяет заменять один компонент другим при изменении формата входных данных или используемой техники верификации. В работе рассматривается архитектура инструмента, описывается наша реализация и демонстрируется пример верификации библиотечной функции memset.
Ключевые слова
формальные методы,
дедуктивная верификация,
анализ бинарного кода,
проверка эквивалентности,
архитектура системы команд,
машинный код,
тестирование компиляторов
При поддержке: Работа поддержана грантом Минобрнауки РФ RFMEFI60719X0295.
Об авторах
Илья Владимирович ГЛАДЫШЕВ
Национальный исследовательский университет «Высшая школа экономики»
Россия
Студент магистратуры по направлению «Системное программирование»
Россия
Студент магистратуры по направлению «Системное программирование»
Александр Сергеевич КАМКИН
Институт системного программирования им. В.П. Иванникова РАН,
Московский государственный университет имени М.В. Ломоносова,
Московский физико-технический институт,
Национальный исследовательский университет «Высшая школа экономики»
Россия
Кандидат физико-математических наук, ведущий научный сотрудник отдела технологий программирования ИСП РАН; преподает в МГУ, МФТИ и ВШЭ
Россия
Кандидат физико-математических наук, ведущий научный сотрудник отдела технологий программирования ИСП РАН; преподает в МГУ, МФТИ и ВШЭ
Артем Михайлович КОЦЫНЯК
Институт системного программирования им. В.П. Иванникова РАН
Россия
Младший научный сотрудник отдела технологий программирования
Россия
Младший научный сотрудник отдела технологий программирования
Павел Андреевич ПУТРО
Институт системного программирования им. В.П. Иванникова РАН
Россия
Получил степень бакалавра в области программной инженерии и степень магистра в области системного программирования в ВШЭ, Москва, Россия, работает в ИСП РАН
Россия
Получил степень бакалавра в области программной инженерии и степень магистра в области системного программирования в ВШЭ, Москва, Россия, работает в ИСП РАН
Алексей Владимирович ХОРОШИЛОВ
Институт системного программирования им. В.П. Иванникова РАН,
Московский государственный университет имени М.В. Ломоносова,
Московский физико-технический институт,
Национальный исследовательский университет «Высшая школа экономики»
Россия
Ведущий научный сотрудник, кандидат физико-математических наук, директор Центра верификации ОС Linux в ИСПРАН, доцент кафедр системного программирования МГУ, ВШЭ и МФТИ
Россия
Ведущий научный сотрудник, кандидат физико-математических наук, директор Центра верификации ОС Linux в ИСПРАН, доцент кафедр системного программирования МГУ, ВШЭ и МФТИ
Список литературы
1. R.W. Floyd. Assigning Meanings to Programs. Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19, 1967, pp. 19-32.
2. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, issue 10, 1969, pp. 576-585.
3. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser. Comprehensive Formal Verification of an OS Microkernel. ACM Transactions on Computer Systems (TOCS), vol. 32, issue 1, 2014, pp. 2:1-2:70.
4. E. Cohen, W. Paul, S. Schmaltz. Theory of Multi Core Hypervisor Verification. Lecture Notes in Computer Science, vol. 7741, 2013, pp. 1-27.
5. P. Philippaerts, J.T. Mühlberg, W. Penninckx, J. Smans, B. Jacobs, F. Piessens. Software Verification with VeriFast: Industrial Case Studies. Science of Computer Programming, vol. 82, 2014, pp. 77-97.
6. D. Efremov, M. Mandrykin, A. Khoroshilov. Deductive Verification of Unmodified Linux Kernel Library Functions. Lecture Notes in Computer Science, vol. 11245, 2018, pp. 216-234.
7. D.R. Cok. OpenJML: JML for Java 7 by Extending OpenJDK. Lecture Notes in Computer Science, vol. 6617, 2011, pp. 472-479.
8. A. Kamkin, A. Khoroshilov, A. Kotsynyak, P. Putro. Deductive Binary Code Verification Against Source-Code-Level Specifications. Lecture Notes in Computer Science, vol. 12165, 2020, pp. 43-58.
9. CompCert Project. Available at: http://compcert.inria.fr, accessed 12.07.2020.
10. C. Sun, V. Le, Q. Zhang, Z. Su. Toward Understanding Compiler Bugs in GCC and LLVM. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA), 2016, pp. 294-305.
11. M. Schoolderman. Verifying Branch-Free Assembly Code in Why3. Lecture Notes in Computer Science, vol. 10712, 2017, pp. 66-83.
12. J.-C. Filliˆatre, A. Paskevich. Why3 – Where Programs Meet Provers. Lecture Notes in Computer Science, vol. 7792, 2013, pp. 125-128.
13. M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993, 47 p.
14. M.O. Myreen. Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge, 2009, 131 p.
15. K. Slind, M. Norrish. A Brief Overview of HOL4. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 28-32. DOI: 10.1007/978-3-540-71067-7 6.
16. A. Fox. Formal Specification and Verification of ARM6. Lecture Notes in Computer Science, vol. 2758, 2003, pp. 25-40.
17. K. Crary, S. Sarkar. Foundational Certified Code in a Metalogical Framework. Technical Report CMU-CS-03-108. Carnegie Mellon University, 2003, 19 p.
18. X. Leroy. Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant. In Proc. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL), 2006, pp. 42-54, DOI: 10.1145/1111037.1111042.
19. Y. Bertot. A Short Presentation of Coq. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 12-16.
20. 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.
21. T.M.T. Nguyen, C. March´e. Hardware-Dependent Proofs of Numerical Programs. Lecture Notes in Computer Science, vol. 7086, pp. 314-329.
22. G. Barthe, T. Rezk, A. Saabas. Proof Obligations Preserving Compilation. Lecture Notes in Computer Science, vol. 3866, pp. 112-126.
23. GNU Binutils. Available at: https://www.gnu.org/software/binutils, accessed 12.07.2020
24. C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard Version 2.6. Release 2017-07-18. 104 p.
25. M. Dahiya, S. Bansal. Black-Box Equivalence Checking Across Compiler Optimizations. Lecture Notes in Computer Science, vol. 10695, pp. 127-147.
26. B. Churchill, O. Padon, R. Sharma, A. Aiken. Semantic Program Alignment for Equivalence Checking. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019, pp. 1027-1040.
27. RISC-V Foundation. Available at: https://riscv.org, accessed 12.07.2020.
28. Results of memset binary code verification. Available at: https://forge.ispras.ru/attachments/7472, accessed 12.07.2020.
29. Executable and Linkable Format (ELF. Available at: http://www.skyfree.org/linux/references/ELF Format.pdf, accessed 12.07.2020.
30. M. Chupilko, A. Kamkin, A. Kotsynyak, A. Protsenko, S. Smolov, A. Tatarnikov. Test Program Generator MicroTESK for RISC-V. In Proc. of the International Workshop on Microprocessor and SOC Test and Verification (MTV), 2018, 6 p.
31. MicroTESK Framework. Available at: http://www.microtesk.org, accessed 12.07.2020.
32. Frama-C Platform. Available at: http://frama-c.com, accessed 12.07.2020.
33. MicroVer Project. Available at: https://forge.ispras.ru/projects/microver, accessed 12.07.2020.
34. CVC4 Solver. Available at: https://github.com/CVC4/CVC4, accessed 12.07.2020.
Рецензия
Для цитирования:
ГЛАДЫШЕВ И.В., КАМКИН А.С., КОЦЫНЯК А.М., ПУТРО П.А., ХОРОШИЛОВ А.В. Архитектура системы дедуктивной верификации машинного кода. Труды Института системного программирования РАН. 2020;32(3):7-19. https://doi.org/10.15514/ISPRAS-2020-32(3)-1
For citation:
GLADYSHEV I.V., KAMKIN A.S., KOTSYNYAK A.M., PUTRO P.A., KHOROSHILOV A.V. Architecture of a Machine Code Deductive Verification System. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(3):7-19. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(3)-1
Послать статью по эл. почте 