Полная решающая процедура для теории ограниченной адресной арифметики

Процесс разработки кода на Си довольно часто сопровождается появлением ошибок, связанных с использованием указателей и адресов памяти. В связи с этим возникает потребность создания инструментов автоматизированной проверки программ. Одним из методов, применяемых такими инструментами проверки, является использование решающих процедур на основе SMT-решателей. Но в то же время разрешимые логики (комбинации логических теорий), требуемые для адекватного моделирования указателей в языке Си, непосредственно не присутствуют в стандарте SMT-LIB и не реализованы в большинстве существующих SMT-решателей. Одним из возможных способов поддержки таких логик является непосредственная их реализация в каком-либо SMT-решателе, однако такой подход часто оказывается трудоемким (требуется изменение исходного кода решателя), негибким (трудно модифицировать сигнатуру и семантику новых теорий) и ограниченным (требуется отдельная реализация поддержки теории в каждом используемом решателе). Другим способом является реализация пользовательских стратегий конечного инстанцирования кванторов для сведения формул в неподдерживаемых логиках к формулам в широко распространенных разрешимых логиках, таких как QF_UFLIA. В данной статье представлена процедура инстанцирования лемм для трансляции формул в теории типизированной адресной арифметики в логику QF_UFLIA. Для процедуры трансляции даны доказательства корректности и полноты, а также описана формализация этих доказательств в системе Isabelle/HOL. Сама теория адресной арифметики сформулирована на основе известных ошибок использования адресной арифметики в языке Си, а также спецификаций семантики этих операций из стандарта языка. Аналогичные доказательства и процедура также могут быть сформулированы для фрагмента теории бит-векторов (монотонные формулы над равенствами между выражениями с побитовыми операциями, такими как исключающее “или”, сдвиг, конкатенация, экстракция, отрицание). Представленная в статье процедура трансляции, в частности, позволяет легко реализовать полный метод доказательства утверждений в теории адресной арифметики в системе Isabelle/HOL на основе существующей в этой системе поддержки SMT-решателей (Z3 или VeriT).

1. T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, 2002. 240 p.

2. Vegard Nossum. [PATCH] firmware: declare __{start,end}_builtin_fw as pointers. Available at: https://www.mail-archive.com/linux-kernel@vger.kernel.org/msg1176758.html.

3. Xi Wang, Haogang Chen et al. Undefined behavior: What happened to my code? In Proc. of the Asia-Pacific Workshop on Systems, 2012, Article No.: 9.

4. Chad R. Dougherty and Robert C. Seacord. C compilers may silently discard some wraparound checks. Available at: https://www.kb.cert.org/vuls/id/162289.

5. Р.Ф. Садыков, М.У. Мандрыкин. Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMT. Труды ИСП РАН, том 32, вып. 2, 2020 г., стр. 107-124 / R. Sadykov, M. Mandrykin. Verified Isabelle/HOL tactic for the theory of bounded integers based on quantifier instantiation and SMT. Trudy ISP RAN/Proc. ISP RAS, vol. 32, issue 2, 2020. pp. 107-124 (in Russian). DOI: 10.15514/ISPRAS–2020–32(2)–9.

6. H. Tuch. Formal memory models for verifying C systems code. PhD Thesis. School of Computer Science and Engineering, The University of New South Wales, Australia, 2008, 249 p.

7. Sandrine Blazy and Xavier Leroy. Formal Verification of a Memory Model for C-Like Imperative Languages. Lecture Notes in Computer Science, vol. 3785, 2005, pp. 280-299.

8. Y. Moy. Automatic Modular Static Safety Checking for C Programs. PhD Thesis, Université de Paris-Sud 11, Paris, France, 2009, 249 p.

9. Jeehoon Kang, Chung-Kil Hur et al. 2015. A formal C memory model supporting integer-pointer casts. ACM SIGPLAN Notices, vol. 50, issue 6, 2015, pp. 326–335.

10. K. Memarian and P. Sewell. Clarifying the C memory object model. Available at: http://www.open-std.org/JTC1/SC22/WG14/www/docs/n2012.htm.

11. G. Klein, K. Elphinstone et al. seL4: Formal verification of an OS kernel. In Proc. of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, 2009, pp. 207-220.

12. N. Bjørner, A.Blass et al. Modular difference logic is hard. Tech. Rep. MSR-TR-2008-140, Microsoft, 2008. Available at: https://www.microsoft.com/en-us/research/publication/modular-difference-logic-is-hard/.

13. C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. Available at: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf.

14. S. Böhme. Proof reconstruction for Z3 in Isabelle/HOL. In Proc. of the 7th International Workshop on Satisfiability Modulo Theories (SMT ’09), 2009, pp. 1-11.

15. S. Böhme and T. Weber. Fast LCF-style proof reconstruction for Z3. Lecture Notes in Computer Science, vol. 6172, 2010, pp. 179–194.

16. J. Dawson. Isabelle theories for machine words. Electronic Notes in Theoretical Computer Science, vol. 250, no. 1, pp. 55-70, 2009.

17. R. Sadykov and M. Mandrykin. Complete decision procedure for the bounded theory of pointer arithmetic based on quantifier instantiation and SMT. Available at: https://forge.ispras.ru/projects/tsmt/repository/, 2021.