Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

• Autorzy: Alpuente Maria , Pardo Daniel , Villanueva Alicia

Identyfikatory

DOI

10.3233/FI-2020-1989

• Języki publikacji: EN

Abstrakty

EN

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNEL C, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNEL C in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KIND SPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.

Słowa kluczowe

EN

contract inference; symbolic execution; abstract subsumption; deductive verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 177, nr 3/4
• Strony: 235--273
• Opis fizyczny: Bibliogr. 48 poz., rys., tab.

Twórcy

autor

Alpuente Maria

• VRAIN, Universitat Politècnica de València, Camino de Vera s/n, Valencia, Spain

autor

Pardo Daniel

• DSIC, Universitat Politècnica de València, Valencia, Spain

autor

Villanueva Alicia

• VRAIN, Universitat Politècnica de València, Camino de Vera s/n, Valencia, Spain

Bibliografia

• [1] Meyer B. Applying “design by contract”. Computer, 1992. 25(10):40-51. doi:10.1109/2.161279.
• [2] Cousot P, Cousot R, Fähndrich M, Logozzo F. Automatic Inference of Necessary Preconditions. In: 14th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), volume 7737 of Lecture Notes in Computer Science. Springer, 2013 pp. 128-148. doi:10.1007/978-3-642-35873-9_10.
• [3] Ellison C, Roşu G. An Executable Formal Semantics of C with Applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). ACM, New York, 2012 pp. 533-544. doi:10.1145/2103656.2103719.
• [4] Cobleigh JM, Giannakopoulou D, Păsăreanu CS. Learning Assumptions for Compositional Verification. In: Proceedings of the 9th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), volume 2619 of Lecture Notes in Computer Science. Springer, Heidelberg, 2003 pp. 331-346. doi:10.1007/3-540-36577-X_24.
• [5] Alpuente M, Feliú MA, Villanueva A. Automatic Inference of Specifications Using Matching Logic. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM’13). ACM, New York, 2013 pp. 127-136. doi:10.1145/2426890.2426914.
• [6] Alpuente M, Pardo D, Villanueva A. Automatic Inference of Specifications in the K Framework. Electronic Proc. in Theoretical Comp. Science, 2015. 200:1-17. doi:10.4204/EPTCS.200.1.
• [7] Liskov B, Guttag J. Abstraction and Specification in Program Development. MIT Press, Cambridge, MA, USA, 1986.
• [8] King JC. Symbolic Execution and Program Testing. Communications of the ACM, 1976. 19(7):385-394. doi:10.1145/360248.360252.
• [9] Păsăreanu CS, Visser W. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer, 2009. 11(4):339-353. doi:10.1007/s10009-009-0118-1.
• [10] Roşu G, Şerbănuţă TF. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 2010. 79(6):397-434. doi:10.1016/j.jlap.2010.03.012.
• [11] Roşu G, Ştefănescu A. Matching Logic: A New Program Verification Approach (NIER Track). In: Proceedings of the 33rd Int’l Conf. on Software Engineering (ICSE’11). ACM, New York, 2011 pp. 868-871. doi:10.1145/1985793.1985928.
• [12] Ştefănescu A, Park D, Yuwen S, Li Y, Roşu G. Semantics-based Program Verifiers for All Languages. In: Proceedings of the 2016 ACM SIGPLAN Int’l Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’16). ACM, 2016 pp. 74-91. doi:10.1145/2983990.2984027.
• [13] Arusoaie A, Lucanu D, Rusu V. Symbolic execution based on language transformation. Computer Languages, Systems & Structures, 2015. 44(A):48-71. doi:10.1016/j.cl.2015.08.004.
• [14] Anand S, Păsăreanu CS, Visser W. Symbolic execution with abstraction. International Journal on Software Tools for Technology Transfer, 2009. 11(1):53-67. doi:10.1007/s10009-008-0090-1.
• [15] Khurshid S, Păsăreanu CS, Visser W. Generalized Symbolic Execution for Model Checking and Testing. In: Proceedings of the 9th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03). ACM, New York, 2003 pp. 553-568. doi:10.1007/3-540-36577-X_40.
• [16] Alpuente M, Pardo D, Villanueva A. Symbolic Abstract Contract Synthesis in a Rewriting Framework. In: Proceedings of the 26th Int’l Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’16), volume 10184 of Lecture Notes in Computer Science. Springer, Cham, 2016 pp. 187-202. doi:10.1007/978-3-319-63139-4_11.
• [17] Moura Ld, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of the 14th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), volume 4963 of Lecture Notes in Computer Science. Springer, Heidelberg, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3_24.
• [18] Baudin P, Cuoq P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V. ACSL: ANSI/ISO C Specification Language, version 1.4, 2010.
• [19] Milner R. Communication and Concurrency. Prentice Hall, 1989.
• [20] Hähnle R, Baum M, Bubel R, Rothe M. A Visual Interactive Debugger Based on Symbolic Execution. In: Proceedings of the 25th IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE’10). ACM, New York, 2010 pp. 143-146. doi:10.1145/1858996.1859022.
• [21] Cousot P, Cousot R. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’77). ACM, New York, 1977 pp. 238-252. doi:10.1145/512950.512973.
• [22] Manevich R, Yahav E, Ramalingam G, Sagiv S. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Proceedings of the 6th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI’05), volume 3385 of Lecture Notes in Computer Science. Springer, Heidelberg, 2005 pp. 181-198. doi:10.1007/978-3-540-30579-8_13.
• [23] Jaffar J, Navas JA, Santosa AE. Unbounded Symbolic Execution for Program Verification. In: Proceedings of the Second Int’l Conf. on Runtime Verification, RV’11. Springer, Heidelberg. ISBN 978-3-642-29859-2, 2012 pp. 396-411. doi:10.1007/978-3-642-29860-8_32.
• [24] Padhi S, Sharma R, Millstein T. LoopInvGen: A Loop Invariant Generator based on Precondition Inference, 2017. URL https://arxiv.org/abs/1707.02029.
• [25] Roşu G. From Rewriting Logic, to Programming Language Semantics, to Program Verification. In: Logic, Rewriting, and Concurrency: Essays dedicated to J. Meseguer on the occasion of his 65th Birthday, Lecture Notes in Comp. Sci., pp. 598-616. Springer, 2015. doi:10.1007/978-3-319-23165-5_28.
• [26] Reichel H. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, 1995. 5(2):129-152. doi:10.1017/S0960129500000694.
• [27] Ştefănescu A, Ciobâcă S, Moore B, Şerbănuţă TF, Roşu G. Reachability Logic in K. Technical report, UIUC, 2013.
• [28] Roşu G, Ştefănescu A, Ciobâcă S, Moore B. One-Path Reachability Logic. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’13). 2013 pp. 358-367. doi:10.1109/LICS.2013.42.
• [29] Ştefănescu A, Ciobâcă Ş, Mereuta R, Moore BM, Şerbănută TF, Roşu G. All-Path Reachability Logic. In: Proceedings of the Joint 25th Int’l Conf. on Rewriting Techniques and Applications and 12th Int’l Conf. on Typed Lambda Calculi and Applications (RTA-TLCA’14), volume 8560 of Lecture Notes in Computer Science. Springer, Cham, 2014 pp. 425-440. doi:10.1007/978-3-319-08918-8_29.
• [30] Magill S, Nanevski A, Clarke A, Lee P. Inferring invariants in Separation Logic for imperative list-processing programs. In: 3rd SPACE Workshop. 2006 doi:10.1.1.115.8677.
• [31] Calcagno C, Distefano D, O’Hearn PW, Yang H. Footprint Analysis: A Shape Analysis That Discovers Preconditions. In: Proceedings of the 14th Int’l Static Analysis Symposium (SAS’07), volume 4634 of Lecture Notes in Computer Science. Springer, Heidelberg, 2007 pp. 402-418. doi:10.1007/978-3-540-74061-2_25.
• [32] Gulavani BS, Chakraborty S, Ramalingam G, Nori AV. Bottom-up Shape Analysis Using LISF. ACM Transactions on Programming Languages and Systems (TOPLAS), 2011. 33(5):17:1-17:41. doi:10.1145/2039346.2039349.
• [33] Moy Y, Marché C. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 2010. 45(11):1184-1211. doi:10.1016/j.jsc.2010.06.004.
• [34] Wei Y, Furia CA, Kazmin N, Meyer B. Inferring Better Contracts. In: Proceedings of the 33rd Int’l Conf. on Software Engineering (ICSE’11). ACM, 2011 pp. 191-200. doi:10.1145/1985793.1985820.
• [35] Tillmann N, Chen F, Schulte W. Discovering Likely Method Specifications. In: Proceedings of the 8th Int’l Conf. on Formal Methods and Software Engineering (ICFEM’06), volume 4260 of Lecture Notes in Computer Science. Springer, Heidelberg, 2006 pp. 717-736. doi:10.1007/11901433_39.
• [36] Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 2007. 69(1-3):35-45. doi:10.1016/j.scico.2007.01.015.
• [37] Hangal S, Lam MS. Tracking Down Software Bugs Using Automatic Anomaly Detection. In: Proceedings of the 24th Int’l Conf. on Software Engineering (ICSE’02). ACM, New York, 2002 pp. 291-301. doi:10.1145/581339.581377.
• [38] Smallbone N, Johansson M, Claessen K, Algehed M. Quick specifications for the busy programmer. Journal on Functional Programming, 2017. 27:e18. doi:10.1017/S0956796817000090.
• [39] Henkel J, Reichenbach C, Diwan A. Discovering Documentation for Java Container Classes. IEEE Transactions on Software Engineering, 2007. 33(8):526-543. doi:10.1109/TSE.2007.70705.
• [40] Csallner C, Tillmann N, Smaragdakis Y. DySy: Dynamic Symbolic Execution for Invariant Inference. In: Proceedings of the 30th Int’l Conf. on Software Engineering (ICSE’08). ACM, New York, 2008 pp.281-290. doi:10.1145/1368088.1368127.
• [41] Whaley J, Martin MC, Lam MS. Automatic Extraction of Object-oriented Component Interfaces. In: Proceedings of the 12th ACM SIGSOFT Int’l Symposium on Software Testing and Analysis (ISSTA’02). ACM, New York, 2002 pp. 218-228. doi:10.1145/566171.566212.
• [42] Giannakopoulou D, Păsăreanu CS. Interface Generation and Compositional Verification in JavaPathfinder. In: Proceedings of the 12th Int’l Conf. on Fundamental Approaches to Software Engineering (FASE’09), volume 5503 of Lecture Notes in Computer Science. Springer, Heidelberg, 2009 pp. 94-108. doi:10.1007/978-3-642-00593-0_7.
• [43] Bacci G, Comini M, Feliú MA, Villanueva A. Automatic Synthesis of Specifications for First Order Curry Programs. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP’12). ACM, New York, 2012 pp. 25-34. doi:10.1145/2370776.2370781.
• [44] Taghdiri M, Jackson D. Inferring specifications to detect errors in code. Automated Software Engineering, 2007. 14(1):87-121. doi:10.1007/s10515-006-0005-x.
• [45] Ghezzi C, Mocci A, Monga M. Synthesizing intensional behavior models by graph transformation. In: Proceedings of the IEEE 31st Int’l Conf. on Software Engineering (ICSE’09). 2009 pp. 430-440. doi:10.1109/ICSE.2009.5070542.
• [46] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott CL (eds.). All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007.
• [47] Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn PW, Wies T, Yang H. Shape Analysis for Composite Data Structures. In: Proceedings of the 19th Int’l Conf. on Computer Aided Verification (CAV’07), volume 4590 of Lecture Notes in Comp. Sci. Springer, Heidelberg, 2007 pp. 178-192. doi:10.1007/978-3-540-73368-3_22.
• [48] Distefano D, O’Hearn PW, Yang H. A Local Shape Analysis Based on Separation Logic. In: Proceedings of the 12th Int’l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), volume 3920 of Lecture Notes in Comp. Sci. Springer, 2006 pp. 287-302. doi:10.1007/11691372_19.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).