## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Semantics-based program verifiers for all languages.

OOPSLA, no. 10 (2016): 74-91

EI

Abstract

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relativel...More

Code:

Data:

Introduction

- Operational semantics are easy to define and understand, to implementing an interpreter.
- Operational semantics are typically used as trusted reference models for the defined languages.
- Despite these advantages, they are rarely used directly for program verification, because proofs tend to be low-level, as they work directly with the corresponding transition system.
- The state-of-the-art in mechanical program verification is to develop and prove such language-specific proof systems sound w.r.t. a trusted operational semantics [3, 26, 36], but that needs to be done for each language separately and is labor intensive

Highlights

- Operational semantics are easy to define and understand, to implementing an interpreter
- We do not expect the reader to immediately agree with us that the reachability logic proof above is more intuitive than the Hoare logic proof
- Urge the reader to consider the main practical benefits of the reachability logic proof: it used the executable semantics of the programming language unchanged and only a fixed set of language-independent proof rules, without requiring any other semantics to be crafted or the program to be modified in order to be verifiable
- One can regard the reachability logic proof system as an effective mechanism to turn an operational semantics into a corresponding axiomatic semantics
- We evaluate the K verification infrastructure by instantiating it with four different semantics, obtaining program verifiers for four different languages: KernelC, C, Java, and JavaScript
- First we implemented all the features required to verify the programs in Table 1 with KernelC: symbolic execution, reasoning with heap abstractions, integration with Z3, etc

Results

- The authors evaluate the K verification infrastructure by instantiating it with four different semantics, obtaining program verifiers for four different languages: KernelC, C, Java, and JavaScript.
- The authors' goal is to validate the hypothesis that building program verifiers by using K operational semantics and its verification infrastructure is effective both in terms of verification capabilities and tool building effort.
- To evaluate this hypothesis, first the authors implemented all the features required to verify the programs in Table 1 with KernelC: symbolic execution, reasoning with heap abstractions, integration with Z3, etc.
- The implementation and the experiments are available as part of the K framework at http://github.com/ kframework/k/wiki/Program-Verification

Conclusion

- Forty-five years of Hoare logic cannot be taken lightly. The authors do not expect the reader to immediately agree with them that the reachability logic proof above is more intuitive than the Hoare logic proof.
- Urge the reader to consider the main practical benefits of the reachability logic proof: it used the executable semantics of the programming language unchanged and only a fixed set of language-independent proof rules, without requiring any other semantics to be crafted or the program to be modified in order to be verifiable
- These benefits cannot be taken lightly either, especially when certifiable verification is a concern.
- One can regard the reachability logic proof system as an effective mechanism to turn an operational semantics into a corresponding axiomatic semantics

- Table1: Summary of verification experiments: ‘Execution’ shows time (seconds) and number of operational semantic steps for symbolic execution (Section 5.1); ‘Reasoning’ shows time (seconds) and number of Z3 queries for reasoning (Section 5.2 & 5.3)
- Table2: The development costs effort scales with the language complexity. The effort for C is considerably larger than for Java and JavaScript due to the low level complexity of C. Overall, the numbers in Table 2 validate our hypothesis that program verification based on operational semantics and the K verification infrastructure is cost effective in terms of development effort

Related work

- The program verification literature is rich. We only discuss work close to ours, omitting theoretical work that has not been applied to large languages or work on interactive verification.

A popular approach to building program verifiers for realworld languages is to translate to an IVL and do verification at the IVL level. This results in some re-usability, as the VC generation and reasoning about state properties are implemented only once, at the IVL level. However, the development of translators is both time consuming and susceptible to bugs. Boogie [4] is a popular IVL integrated with Z3. There are several verifiers built on top of Boogie, including VCC [11], HAVOC [28], Spec# [5], Dafny [30], and Chalice [31]. VCDrayd [39] is a separation logic based verifier built on top of VCC. Why3 [21] is another IVL, also integrated with SMT solvers (and other provers). Tools built on top of Why3 include Frama-C [21] and Krakatoa [20]. There are many other practical VC generation based tools (with or without an IVL), including Verifast [27] and jStar [17]. In contrast, we use existing operational semantics directly for verification, without any translation to IVLs or language-specific VC generation.

Funding

- The work in this paper was supported in part by the NSF grants CCF1218605, CCF-1318191, and CCF-1421575, by the DARPA HACMS grant FA8750-12-C-0284, and by the Boeing grant on “Formal Analysis Tools for Cyber Security” 2015-2016

Reference

- VCC: A verifier for concurrent C. http://vcc.codeplex.com. Accessed: October 5, 2016.
- S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. J. ACM, 47(4):776–822, 2000.
- A. W. Appel. Verified software toolchain. In ESOP, volume 6602 of LNCS, pages 1–17, 2011.
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects (FMCO’05), volume 4111 of LNCS, pages 364–387, 2006.
- M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and verification: the Spec# experience. Commun. ACM, 54(6):81–91, 2011.
- B. Beckert, R. Hähnle, and P. H. Schmitt. Verification of Objectoriented Software: The KeY Approach. Springer-Verlag, 2007.
- G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, 1992.
- D. Bogdanas and G. Rosu. K-Java: A complete semantics of Java. In POPL, pages 445–456. ACM, 2015.
- S. Bucur, J. Kinder, and G. Candea. Prototyping symbolic execution engines for interpreted languages. In ASPLOS, pages 239–254. ACM, 2014.
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234– 245, 2011.
- E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs, volume 5674 of LNCS, pages 23–42, 2009.
- A. Stefanescu, S. Ciobâca, R. Mereuta, B. M. Moore, T. F. Serbanuta, and G. Rosu. All-path reachability logic. In RTA, volume 8560 of LNCS, pages 425–440, July 2014.
- E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Semantics-based generation of verification conditions by program specialization. In PPDP, pages 91–102. ACM, 2015.
- L. M. de Moura and N. Bjørner. Efficient E-matching for SMT solvers. In CADE, volume 4603 of LNCS, pages 183–198, 2007.
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340, 2008.
- L. M. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, pages 45–52. IEEE, 2009.
- D. Distefano and M. J. Parkinson. jStar: Towards practical verification for Java. In OOPSLA, pages 213–226. ACM, 2008.
- C. Ellison and G. Ros, u. An executable formal semantics of C with applications. In POPL, pages 533–544. ACM, 2012.
- M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT, 2009.
- J. Filliâtre and C. Marché. The why/krakatoa/caduceus platform for deductive program verification. In CAV, volume 4590 of LNCS, pages 173–177, 2007.
- J. Filliâtre and A. Paskevich. Why3 - where programs meet provers. In ESOP, volume 7792 of LNCS, pages 125–128, 2013.
- C. George, A. E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. S. Pedersen. The RAISE Development Method. Prentice Hall, 1995.
- S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405–416. ACM, 2012.
- D. Harel, D. Kozen, and J. Tiuryn. Dynamic logic. In Handbook of Philosophical Logic, pages 497–604, 1984.
- C. Hathhorn, C. Ellison, and G. Rosu. Defining the undefinedness of C. In PLDI, pages 336–345. ACM, 2015.
- B. Jacobs. Weakest pre-condition reasoning for Java programs with JML annotations. J. Logic and Algebraic Programming, 58(1-2):61–88, 2004.
- B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of the Third International Conference on NASA Formal Methods (NFM’11), volume 6617 of LNCS, pages 41–55, 2011.
- S. K. Lahiri and S. Qadeer. Verifying properties of wellfounded linked lists. In POPL, pages 115–126, 2006.
- D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with VCC. In FM, volume 5850 of LNCS, pages 806–809, 2009.
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, pages 348–370, 2010.
- K. R. M. Leino, P. Müller, and J. Smans. Deadlock-free channels and locks. In ESOP, volume 6012 of LNCS, pages 407–426, 2010.
- H. Liu and J. S. Moore. Java program verification via a JVM deep embedding in ACL2. In TPHOLs, volume 3223 of LNCS, pages 184–200, 2004.
- P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL, pages 123–136. ACM, 2012.
- A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI, pages 221–231, 2001.
- H. H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size properties via separation logic. In VMCAI, volume 4349 of LNCS, pages 251–266, 2007.
- T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171– 186, 1998.
- P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of LNCS, pages 1–19, 2001.
- D. Park, A. Stefanescu, and G. Rosu. KJS: A complete formal semantics of JavaScript. In PLDI, pages 346–356. ACM, 2015.
- E. Pek, X. Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in C using separation logic. In PLDI, pages 440–451. ACM, 2014.
- J. A. N. Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, pages 556–566. ACM, 2011.
- X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI, pages 231–242. ACM, 2013.
- G. Rosu. Matching logic — extended abstract. In RTA, volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5–21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.
- G. Rosu, A. Stefanescu, S. Ciobâca, and B. M. Moore. Onepath reachability logic. In LICS, pages 358–367. IEEE, 2013.
- G. Ros, u and T.-F. S, erbanut,a. An overview of the K semantic framework. J. Logic and Algebraic Programming, 79(6):397– 434, 2010.
- G. Ros, u and A. S, tefanescu. From Hoare logic to matching logic reachability. In FM, volume 7436 of LNCS, pages 387– 402, 2012.
- G. Ros, u and A. S, tefanescu. Towards a unified theory of operational and axiomatic semantics. In ICALP, volume 7392 of LNCS, pages 351–363, 2012.
- G. Ros, u and A. S, tefanescu. Checking reachability using matching logic. In OOPSLA, pages 555–574. ACM, 2012.
- G. Ros, u, C. Ellison, and W. Schulte. Matching logic: An alternative to Hoare/Floyd logic. In AMAST, volume 6486 of LNCS, pages 142–162, 2010.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn