Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

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.