AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
One can regard the reachability logic proof system as an effective mechanism to turn an operational semantics into a corresponding axiomatic semantics

Semantics-based program verifiers for all languages.

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

Cited by: 79|Views228
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:

0
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
Tables
  • 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
Download tables as Excel
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.
    Findings
  • S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. J. ACM, 47(4):776–822, 2000.
    Google ScholarLocate open access versionFindings
  • A. W. Appel. Verified software toolchain. In ESOP, volume 6602 of LNCS, pages 1–17, 2011.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • B. Beckert, R. Hähnle, and P. H. Schmitt. Verification of Objectoriented Software: The KeY Approach. Springer-Verlag, 2007.
    Google ScholarFindings
  • G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, 1992.
    Google ScholarLocate open access versionFindings
  • D. Bogdanas and G. Rosu. K-Java: A complete semantics of Java. In POPL, pages 445–456. ACM, 2015.
    Google ScholarLocate open access versionFindings
  • S. Bucur, J. Kinder, and G. Candea. Prototyping symbolic execution engines for interpreted languages. In ASPLOS, pages 239–254. ACM, 2014.
    Google ScholarLocate open access versionFindings
  • A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234– 245, 2011.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • L. M. de Moura and N. Bjørner. Efficient E-matching for SMT solvers. In CADE, volume 4603 of LNCS, pages 183–198, 2007.
    Google ScholarLocate open access versionFindings
  • L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340, 2008.
    Google ScholarLocate open access versionFindings
  • L. M. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, pages 45–52. IEEE, 2009.
    Google ScholarLocate open access versionFindings
  • D. Distefano and M. J. Parkinson. jStar: Towards practical verification for Java. In OOPSLA, pages 213–226. ACM, 2008.
    Google ScholarLocate open access versionFindings
  • C. Ellison and G. Ros, u. An executable formal semantics of C with applications. In POPL, pages 533–544. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT, 2009.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • J. Filliâtre and A. Paskevich. Why3 - where programs meet provers. In ESOP, volume 7792 of LNCS, pages 125–128, 2013.
    Google ScholarLocate open access versionFindings
  • C. George, A. E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. S. Pedersen. The RAISE Development Method. Prentice Hall, 1995.
    Google ScholarFindings
  • S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405–416. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • D. Harel, D. Kozen, and J. Tiuryn. Dynamic logic. In Handbook of Philosophical Logic, pages 497–604, 1984.
    Google ScholarLocate open access versionFindings
  • C. Hathhorn, C. Ellison, and G. Rosu. Defining the undefinedness of C. In PLDI, pages 336–345. ACM, 2015.
    Google ScholarLocate open access versionFindings
  • B. Jacobs. Weakest pre-condition reasoning for Java programs with JML annotations. J. Logic and Algebraic Programming, 58(1-2):61–88, 2004.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • S. K. Lahiri and S. Qadeer. Verifying properties of wellfounded linked lists. In POPL, pages 115–126, 2006.
    Google ScholarLocate open access versionFindings
  • D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with VCC. In FM, volume 5850 of LNCS, pages 806–809, 2009.
    Google ScholarLocate open access versionFindings
  • K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, pages 348–370, 2010.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL, pages 123–136. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI, pages 221–231, 2001.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171– 186, 1998.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • D. Park, A. Stefanescu, and G. Rosu. KJS: A complete formal semantics of JavaScript. In PLDI, pages 346–356. ACM, 2015.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • J. A. N. Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, pages 556–566. ACM, 2011.
    Google ScholarLocate open access versionFindings
  • X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI, pages 231–242. ACM, 2013.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • G. Rosu, A. Stefanescu, S. Ciobâca, and B. M. Moore. Onepath reachability logic. In LICS, pages 358–367. IEEE, 2013.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • G. Ros, u and A. S, tefanescu. From Hoare logic to matching logic reachability. In FM, volume 7436 of LNCS, pages 387– 402, 2012.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • G. Ros, u and A. S, tefanescu. Checking reachability using matching logic. In OOPSLA, pages 555–574. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
Author
Shijiao Yuwen
Shijiao Yuwen
Yilong Li
Yilong Li
Your rating :
0

 

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