Preview

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

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

Совмещение ACSL спецификаций с машинным кодом

https://doi.org/10.15514/ISPRAS-2018-30(4)-6

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

Аннотация

При разработке программ на языках высокого уровня, разработчикам приходится делать предположение о корректности компилятора. Однако это может быть неприемлемо для критически важных систем. Поскольку на данный момент не существует полноценных компиляторов, для которых корректность доказана, автор предлагает решать эту проблему путём доказательства корректности сгенерированного машинного кода методами дедуктивной верификации. Для достижения данной цели необходимо решить ряд задач, одной из которых является слияние модели спецификаций пред- и постусловий с моделью поведения машинного кода. В данной статье представлен подход к проведению слияния спецификаций для случая Си функций без циклов. Суть подхода заключается построении моделей как машинного кода, так и его спецификации на едином логическом языке, и использовании ABI целевого процессора для связывания машинных регистров с параметрами функции высокого уровня. Для успешной реализации такого подхода необходимо предпринять ряд мер по обеспечению совместимости высокоуровневых спецификаций с моделью поведения машинного кода. К таким мерам, в частности, относятся использование типа регистра в высокоуровневых спецификациях, трансляция пред- и постусловий в абстрактные предикаты. Также в статье производится и обосновывается выбор логического языка для построения моделей, выбираются наиболее подходящие инструменты для реализации подхода слияния спецификаций и производится оценка работы системы дедуктивной верификации машинного кода, построенной на основе предложенного подхода, с использованием тестовых примеров полученных путём компиляции Си программ без циклов.

Об авторе

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


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

1. MicroVer - Deductive Verification Tool for Machine Code, Доступно по ссылке: https://forge.ispras.ru/projects/microver, дата обращения 20.07.2018

2. Leroy Xavier. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, vol. 43, issue 4, 2009, pp 363-446

3. CompCert - The CompCert C compiler. Доступно по ссылке: compcert.inria.fr, дата обращения 13-02-2018

4. GCC Releases. Доступно по ссылке: http://www.gnu.org/software/gcc/releases.html, дата обращения 13-02-2018

5. Butterfield A., Ngondi G., Kerr A. A Dictionary of Computer Science (ed. 7), Oxford University Press, 2016, 608 p.

6. ACSL specification. Доступно по ссылке: http://frama-c.com/acsl.html, дата обращения 13-02-2018

7. Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. In Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2012

8. C Barrett, R Sebastiani, S Seshia, and C Tinelli. Satisfiability Modulo Theories. In Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, Feb. 2009, pp. 825-885

9. EREF: A Programmer’s Reference Manual for Freescale Power Architecture Processors, Rev. 1 (EIS 2.1). Доступно по ссылке: http://cache.freescale.com/files/32bit/doc/ref_manual/EREF_RM.pdf, дата обращения 13-02-2018

10. Filliâtre JC., Paskevich A. Why3 - Where Programs Meet Provers. Lecture Notes in Computer Science, vol. 7792, 2013, pp. 125-128

11. M. Mandrykin, A. Khoroshilov. A Memory Model for Deductively Verifying Linux Kernel Modules. Lecture Notes in Computer Sciences. vol. 10742, 2018, pp. 256-275

12. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowsk. Frama-c: A Software Analysis Perspective. Formal Aspects of Computing, vol. 27, issue 3, 2015, pp 573-609

13. Jessie3 at Why3 source repository. Доступно по ссылке: https://gitlab.inria.fr/why3/why3/tree/master/src/jessie, дата обращения 12.04.2018.

14. Вarrett C., Fontaine P., Tinelli C. The SMT-LIB Standard Version 2.6. Доступно по ссылке: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf, дата обращения 12.04.2018

15. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds. CVC4. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 171-177

16. Schoolderman M. Verifying Branch-Free Assembly Code in Why3. Lecture Notes in Computer Science, vol. 10712, 2017, pp. 66-83

17. Why3-avr project repository. Availible at: https://gitlab.science.ru.nl/sovereign/why3-avr, дата обращения 12.04.2018.

18. Myreen M.O.: Formal verification of machine-code programs. Ph.D. thesis, University of Cambridge, 2009

19. Konrad Slind and Michael Norrish. A brief overview of HOL4. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 28-32

20. Anthony Fox. Formal specification and verification of ARM6. Lecture Notes in Computer Science, vol. 2758, 2003, pp 25-40

21. Karl Crary and Susmit Sarkar. Foundational certified code in a metalogical framework. Technical Report CMU-CS-03-108, Carnegie Mellon University, 2003.

22. Xavier 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, 2006, pp. 42-54

23. Yves Bertot. A short presentation of Coq. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 12-16

24. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001, 190 p.

25. Edelman Joseph R. Machine Code Verification Using the Bogor Framework. Master Thesis, Brigham Young University, 2008

26. Bogor framework homepage. Доступно по ссылке: http://bogor.projects.cs.ksu.edu, дата обращения 13.02.2018


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


Путро П.А. Совмещение ACSL спецификаций с машинным кодом. Труды Института системного программирования РАН. 2018;30(4):95-106. https://doi.org/10.15514/ISPRAS-2018-30(4)-6

For citation:


Putro P.A. Combining ACSL Specifications and Machine Code. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):95-106. https://doi.org/10.15514/ISPRAS-2018-30(4)-6

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


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


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