A PVS Proof Obligation Generator for Lustre Programs

We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verification of proof obligations in the framework of the BWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark provided by the BWare project.

Download Full-text

Beyond Tests

ACM Transactions on Software Engineering and Methodology ◽

10.1145/3418461 ◽

2021 ◽

Vol 30 (2) ◽

pp. 1-27

Author(s):

Xiang Gao ◽

Bo Wang ◽

Gregory J. Duck ◽

Ruyi Ji ◽

Yingfei Xiong ◽

...

Keyword(s):

Symbolic Execution ◽

Test Suite ◽

Proof Obligation ◽

Correctness Criterion ◽

Automated Program Repair ◽

Execution Engine ◽

Program Repair ◽

Wide Range ◽

Overfitting Problem ◽

Repair Techniques

Automated program repair is an emerging technology that seeks to automatically rectify program errors and vulnerabilities. Repair techniques are driven by a correctness criterion that is often in the form of a test suite. Such test-based repair may produce overfitting patches, where the patches produced fail on tests outside the test suite driving the repair. In this work, we present a repair method that fixes program vulnerabilities without the need for a voluminous test suite. Given a vulnerability as evidenced by an exploit, the technique extracts a constraint representing the vulnerability with the help of sanitizers. The extracted constraint serves as a proof obligation that our synthesized patch should satisfy. The proof obligation is met by propagating the extracted constraint to locations that are deemed to be “suitable” fix locations. An implementation of our approach (E xtract F ix ) on top of the KLEE symbolic execution engine shows its efficacy in fixing a wide range of vulnerabilities taken from the ManyBugs benchmark, real-world CVEs and Google’s OSS-Fuzz framework. We believe that our work presents a way forward for the overfitting problem in program repair by generalizing observable hazards/vulnerabilities (as constraint) from a single failing test or exploit.

Download Full-text

Reasoning About Code-Generation in Two-Level Languages

BRICS Report Series ◽

10.7146/brics.v7i46.20213 ◽

2000 ◽

Vol 7 (46) ◽

Cited By ~ 2

Author(s):

Zhe Yang

Keyword(s):

Normal Form ◽

Code Generation ◽

Partial Evaluation ◽

Type System ◽

Language Design ◽

Proof Obligation ◽

Object Language ◽

Good Tool ◽

Type Preservation ◽

Preservation Property

We show that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them as well. Indeed, some general properties of two-level languages capture common proof obligations of code-generation algorithms in the form of two-level programs. - To prove that the generated code behaves as desired, we use an erasure property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation. - To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a type-preservation property for a refined type system that enforces these constraints. In addition, to justify concrete implementations of code-generation algorithms in one-level languages, we use a native embedding of a two-level language into a one-level language. We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two classes of non-trivial applications: one-pass transformations into continuation-passing style and type-directed partial evaluation for call-by-name and for call-by-value.Keywords. Two-level languages, erasure, type preservation, native implementation, partial evaluation.

Download Full-text