RustHorn: CHC-based verification for Rust programs. (English) Zbl 1508.68071
Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 484-514 (2020).
Summary: Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
For the entire collection see [Zbl 1496.68030].
For the entire collection see [Zbl 1496.68030].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
Rust; Viper; Lean; Spacer; MoCHi; Cyclone; RustBelt; Rust2Viper; GitHub; Spec#; SeaHorn; JayHorn; Coq; VCC; CrustReferences:
| [1] | Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253-284 (1991). https://doi.org/10.1016/0304-3975(91)90224-P · Zbl 0728.68083 |
| [2] | Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bjørner, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7180, pp. 46-61. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_7 · Zbl 1352.68141 |
| [3] | Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification (2018). https://doi.org/10.3929/ethz-b-000311092 |
| [4] | Baranowski, M.S., He, S., Rakamaric, Z.: Verifying Rust programs with SMACK. In: Lahiri and Wang [42], pp. 528-535. https://doi.org/10.1007/978-3-030-01090-4_32 |
| [5] | Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: The Spec# experience. Commun. ACM 54(6), 81-91 (2011). https://doi.org/10.1145/1953122.1953145 |
| [6] | Bjørner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol. 9300, pp. 24-51. Springer (2015). https://doi.org/10.1007/978-3-319-23534-9_2 · Zbl 1321.03008 |
| [7] | Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 259-270. ACM (2005). https://doi.org/10.1145/1040305.1040327 · Zbl 1369.68130 |
| [8] | Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: Preventing data races and deadlocks. In: Ibrahim, M., Matsuoka, S. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8, 2002. pp. 211-230. ACM (2002). https://doi.org/10.1145/582419.582440 |
| [9] | Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2694, pp. 55-72. Springer (2003). https://doi.org/10.1007/3-540-44898-5_4 · Zbl 1067.68537 |
| [10] | Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. Lecture Notes in Computer Science, vol. 3855, pp. 427-442. Springer (2006). https://doi.org/10.1007/11609773_28 · Zbl 1176.68116 |
| [11] | Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10805, pp. 365-384. Springer (2018). https://doi.org/10.1007/978-3-319-89960-2_20 · Zbl 1468.68058 |
| [12] | Champion, A., Kobayashi, N., Sato, R.: HoIce: An ICE-based non-linear Horn clause solver. In: Ryu, S. (ed.) Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11275, pp. 146-156. Springer (2018). https://doi.org/10.1007/978-3-030-02768-1_8 · Zbl 1519.68045 |
| [13] | Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: Freeman-Benson, B.N., Chambers, C. (eds.) Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA ’98), Vancouver, British Columbia, Canada, October 18-22, 1998. pp. 48-64. ACM (1998). https://doi.org/10.1145/286936.286947 · Zbl 0924.68038 |
| [14] | Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5674, pp. 23-42. Springer (2009). https://doi.org/10.1007/978-3-642-03359-9_2 |
| [15] | Coq Team: The Coq proof assistant (2020), https://coq.inria.fr/ |
| [16] | van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. Journal of the ACM 23(4), 733-742 (1976). https://doi.org/10.1145/321978.321991 · Zbl 0339.68004 |
| [17] | Erdin, M.: Verification of Rust Generics, Typestates, and Traits. Master’s thesis, ETH Zürich (2019) |
| [18] | Fedyukovich, G., Kaufman, S.J., Bodík, R.: Sampling invariants from frequency distributions. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 100-107. IEEE (2017). https://doi.org/10.23919/FMCAD.2017.8102247 · Zbl 1506.68054 |
| [19] | Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 259-277. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_14 · Zbl 1533.68038 |
| [20] | Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), 17 (2007). https://doi.org/10.1145/1232420.1232424 · Zbl 1369.68136 |
| [21] | Gondelman, L.: Un système de types pragmatique pour la vérification déductive des programmes. (A Pragmatic Type System for Deductive Verification). Ph.D. thesis, University of Paris-Saclay, France (2016), https://tel.archives-ouvertes.fr/tel-01533090 |
| [22] | Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012. pp. 405-416. ACM (2012). https://doi.org/10.1145/2254064.2254112 |
| [23] | Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 343-361. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_20 |
| [24] | Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C/C++ programs. In: Ranzato, F. (ed.) Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10422, pp. 148-168. Springer (2017). https://doi.org/10.1007/978-3-319-66706-5_8 |
| [25] | Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016. pp. 338-348. ACM (2016). https://doi.org/10.1145/2950290.2950330 |
| [26] | Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri and Wang [42], pp. 248-266. https://doi.org/10.1007/978-3-030-01090-4_15 · Zbl 1517.68239 |
| [27] | Hahn, F.: Rust2Viper: Building a Static Verifier for Rust. Master’s thesis, ETH Zürich (2016). https://doi.org/10.3929/ethz-a-010669150 |
| [28] | Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: A pearl in compositional verification. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 473-485. ACM (2017). https://doi.org/10.1145/3009837 · Zbl 1380.68274 |
| [29] | Hojjat, H., Rümmer, P.: The Eldarica Horn solver. In: Bjørner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp. 1-7. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603013 |
| [30] | Horn, A.: On sentences which are true of direct unions of algebras. The Journal of Symbolic Logic 16(1), 14-21 (1951), http://www.jstor.org/stable/2268661 · Zbl 0043.24801 |
| [31] | Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: Ellis, C.S. (ed.) Proceedings of the General Track: 2002 USENIX Annual Technical Conference, June 10-15, 2002, Monterey, California, USA. pp. 275-288. USENIX (2002), http://www.usenix.org/publications/library/proceedings/usenix02/jim.html |
| [32] | Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: Securing the foundations of the Rust programming language. PACMPL 2(POPL), 66:1-66:34 (2018). https://doi.org/10.1145/3158154 |
| [33] | Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https://doi.org/10.1017/S0956796818000151 · Zbl 1476.68062 |
| [34] | Jung, R., Lepigre, R., Parthasarathy, G., Rapoport, M., Timany, A., Dreyer, D., Jacobs, B.: The future is ours: Prophecy variables in separation logic. PACMPL 4(POPL), 45:1-45:32 (2020). https://doi.org/10.1145/3371113 |
| [35] | Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 637-650. ACM (2015). https://doi.org/10.1145/2676726.2676980 · Zbl 1346.68135 |
| [36] | Kahsai, T., Kersten, R., Rümmer, P., Schäf, M.: Quantified heap invariants for object-oriented programs. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol. 46, pp. 368-384. EasyChair (2017) · Zbl 1403.68126 |
| [37] | Kahsai, T., Rümmer, P., Sanchez, H., Schäf, M.: JayHorn: A framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9779, pp. 352-358. Springer (2016). https://doi.org/10.1007/978-3-319-41528-4_19 |
| [38] | Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: Analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018. The Internet Society (2018) |
| [39] | Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. pp. 222-233. ACM (2011). https://doi.org/10.1145/1993498.1993525 |
| [40] | Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 17-34. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_2 · Zbl 1358.68072 |
| [41] | Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2937, pp. 267-281. Springer (2004). https://doi.org/10.1007/978-3-540-24622-0_22 · Zbl 1202.68251 |
| [42] | Lahiri, S.K., Wang, C. (eds.): Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11138. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4 · Zbl 1396.68018 |
| [43] | Lattner, C., Adve, V.S.: Automatic pool allocation: Improving performance by controlling data structure layout in the heap. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005. pp. 129-142. ACM (2005). https://doi.org/10.1145/1065010.1065027 |
| [44] | Lindner, M., Aparicius, J., Lindgren, P.: No panic! Verification of Rust programs by symbolic execution. In: 16th IEEE International Conference on Industrial Informatics, INDIN 2018, Porto, Portugal, July 18-20, 2018. pp. 108-114. IEEE (2018). https://doi.org/10.1109/INDIN.2018.8471992 |
| [45] | Matsakis, N.D.: Introducing MIR (2016), https://blog.rust-lang.org/2016/04/19/MIR.html |
| [46] | Matsakis, N.D., Klock II, F.S.: The Rust language. In: Feldman, M., Taft, S.T. (eds.) Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014. pp. 103-104. ACM (2014). https://doi.org/10.1145/2663171.2663188 |
| [47] | Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs (full version). CoRR (2020), https://arxiv.org/abs/2002.09002 |
| [48] | Microsoft: Boogie: An intermediate verification language (2020), https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/ |
| [49] | de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9195, pp. 378-388. Springer (2015). https://doi.org/10.1007/978-3-319-21401-6_26 · Zbl 1465.68279 |
| [50] | Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 41-62. Springer (2016). https://doi.org/10.1007/978-3-662-49122-5_2 · Zbl 1475.68191 |
| [51] | Rust Community: The MIR (Mid-level IR) (2020), https://rust-lang.github.io/rustc-guide/mir/index.html |
| [52] | Rust Community: Reference cycles can leak memory - the Rust programming language (2020), https://doc.rust-lang.org/book/ch15-06-reference-cycles.html |
| [53] | Rust Community: RFC 2025: Nested method calls (2020), https://rust-lang.github.io/rfcs/2025-nested-method-calls.html |
| [54] | Rust Community: RFC 2094: Non-lexical lifetimes (2020), https://rust-lang.github.io/rfcs/2094-nll.html |
| [55] | Rust Community: Rust programming language (2020), https://www.rust-lang.org/ |
| [56] | Rust Community: std::cell::RefCell - Rust (2020), https://doc.rust-lang.org/std/cell/struct.RefCell.html |
| [57] | Rust Community: std::rc::Rc - Rust (2020), https://doc.rust-lang.org/std/rc/struct.Rc.html |
| [58] | Rust Community: std::vec::Vec - Rust (2020), https://doc.rust-lang.org/std/vec/struct.Vec.html |
| [59] | Rust Community: Two-phase borrows (2020), https://rust-lang.github.io/rustc-guide/borrow_check/two_phase_borrows.html |
| [60] | Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. pp. 47-53. ACM (2019). https://doi.org/10.1145/3294032.3294081 |
| [61] | Steensgaard, B.: Points-to analysis in almost linear time. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. pp. 32-41. ACM Press (1996). https://doi.org/10.1145/237721.237727 |
| [62] | Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. pp. 29-37. IEEE Computer Society (2001). https://doi.org/10.1109/LICS.2001.932480 |
| [63] | Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory deallocation. In: Hu, Z. (ed.) Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5904, pp. 128-143. Springer (2009). https://doi.org/10.1007/978-3-642-10672-9_11 |
| [64] | Terauchi, T.: Checking race freedom via linear programming. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. pp. 1-10. ACM (2008). https://doi.org/10.1145/1375581.1375583 |
| [65] | Toman, J., Pernsteiner, S., Torlak, E.: crust: A bounded verifier for Rust. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015. pp. 75-80. IEEE Computer Society (2015). https://doi.org/10.1109/ASE.2015.77 |
| [66] | Ullrich, S.: Electrolysis reference (2016), http://kha.github.io/electrolysis/ |
| [67] | Ullrich, S.: Simple Verification of Rust Programs via Functional Purification. Master’s thesis, Karlsruhe Institute of Technology (2016) |
| [68] | Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008), http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.612221 |
| [69] | Z3 Team: The Z3 theorem prover (2020), https://github.com/Z3Prover/z3 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
