All-Path Reachability LogicAndrei Stefanescu1, Stefan Ciobaca2, Radu Mereuta1,2,

Brandon Moore1, Traian Serbanuta3, Grigore Rosu1

1 University of Illinois, USA2 University of Iasi, Romania

3 University of Bucharest, Romania

2

Main GoalLanguage-independent program verification

framework

Prove program properties from operational semantics

Proof systemOperational semantics ⊢ program properties

Overview

State-of-the-art in Certifiable Verification

All-Path ReachabilitySpecifying State PropertiesSpecifying Reachability PropertiesReasoning about Reachability

4

Operational SemanticsEasy to define and understand

Can be regarded as formal “implementations”Require little mathematical knowledge

Great introductory topics in PL coursesExecutable, so testable

Can be tested against real benchmarks

5

Operational SemanticsFrameworks

PLT-Redex/Racket (Findler et al.)Raskal (Klint et al.)RLS-Maude (Meseguer et al.)PLanComps (Mosses et al.)K (Rosu et al.)OTT (Sewell et al.)

6

Operational SemanticsScale

C (Ellison and Rosu, POPL’12)GCC torture test suite

JavaScript (Bodin et al., POPL’14)ECMA test262 suite

Python (Politz et al., OOPSLA’13)CPython test suite

PHP (Filaretti and Maffeis, ECOOP’14)Zend test suite

7

Operational SemanticsSample rule (may require a configuration

context)

Define languages only with rules of the form

l, r are configuration termsb is a Boolean side condition

8

Unfortunately …Operational semantics considered inappropriate

for program verification; proofs are low-level and tedious:Formalization of and working with transition systemTypically by induction

on the structure of the programon the number of execution stepsetc.

Done in ACL2 before

9

Axiomatic Semantics(Hoare Logic)

Emphasis on program verificationProgramming language captured as a formal proof

system deriving Hoare triples

precondition postcondition

10

Axiomatic SemanticsNot easy to define and understand, error-prone

Not executable, hard to testRequire program transformations, behavior loss

Write e = 1 and you’ve got a wrong semantics!

11

State-of-the-art inCertifiable Verification

Languages C (Appel et al.) – CompCert operational semantics Java (Jacobs et al.)

Approach Define an operational semantics: trusted language model Define an axiomatic semantics: for verification purposes Prove axiomatic semantics sound for operational semantics

Now we have trusted verification … BUT Requires two semantics of the same language

C operational semantics took more than 2 years! Must be done individually for each language

Overview

State-of-the-art in Certifiable Verification

All-Path ReachabilitySpecifying State PropertiesSpecifying Reachability PropertiesReasoning about Reachability

13

Our ApproachUnderlying belief: one semantics for each

language! Executable (testable), easy to define and understand Suitable for program verification, “as is”

Approach: language-independent proof system Takes operational semantics unchanged Derives program properties Both operational semantics rules and program

specifications stated as reachability rules Sound and relatively complete

Overview

State-of-the-art in Certifiable Verification

All-Path ReachabilitySpecifying State PropertiesSpecifying Reachability PropertiesReasoning about Reachability

15

Matching LogicLogic for specifying static properties about

program configurations and reasoning about them

Key insight:Configuration terms with variables are allowed to

be used as predicates, called patternsSemantically, their satisfaction means matching

Matching logic is parametric in a (first-order) configuration model: typically the underlying model of the operational semantics

[Rosu, Ellison, Schulte 2010]

16

PatternsC configurations

Example of a pattern

Extra 70 cells

17

Model of Configurations- Properties -

Configuration abstraction (list)“Separation” achieved at term level

Operations (reverse)

18

Separation Logic =Matching Logic Instance

Separation logic: popular logic for heap propertiesMechanical translation to matching logic

Configuration: Separation encoded using different sub-terms

Example SL ML

No expressiveness loss from using matching logicMatching logic gives “structural separation” anywhere

in the configuration, not only in the heap

[OOPSLA’12]

Overview

State-of-the-art in Certifiable Verification

All-Path ReachabilitySpecifying State PropertiesSpecifying Reachability PropertiesReasoning about Reachability

20

One-Path Reachability Rules

Pairs of matching logic patterns

One-Path Reachability: Any terminating concrete configuration satisfying reaches, on some execution path, some configuration satisfying , in the transition system induced by the operational semantics .

21

All-Path Reachability RulesPairs of matching logic patterns

All-Path Reachability: Any concrete configuration satisfying reaches, on any terminating execution path, some configuration satisfying , in the transition system induced by the operational semantics .

…

22

Reachability Rules- Operational + Axiomatic

-Operational flavor

Axiomatic flavor

23

Hoare Triple = Syntactic Sugar

24

Operational and Axiomatic Semantics Rules as Reachability

RulesReachability rules generalize

Operational semantics rulesHoare triples

Operational semantics rule is syntactic sugar for reachability rule

Hoare triple encoded in a reachability rule with the empty code in the right-hand-side

Overview

State-of-the-art in Certifiable Verification

All-Path ReachabilitySpecifying State PropertiesSpecifying Reachability PropertiesReasoning about Reachability

26

Reasoning aboutAll-Path Reachability

The main result of this section is a proof system deriving reachability rules from reachability rules:

Operational semantics

Target reachability rule

Claimed reachability rules

(Coinductively) trusted reachability rules

27

Reachability Proof System- In Two Sentences -

Symbolic execution based on operational semantics

Coinductive proof rule for repetitive behaviorGeneralizes invariant rules from Hoare logicSound and (relatively) complete

28

Reachability Proof System- 8 Rules -

Symbolic execution (multiple steps)Code with circular behaviorCode with circular behavior

29

Reachability Proof System

Each configuration has some successorEach successor of a configuration satisfies

30

Circular behaviorsCircularity, Transitivity and Axiom proof rules

Hoare logic rule for while loops

Language-independent

Language-specific

Claim (cannot use yet)!

Enable!

Use!

31

Reachability Proof System

32

Soundness

Theorem: If is derivable by the proof system, then is semantically valid.

33

Relative Completeness

RelativityValidity oracle for static configuration properties

Language-independent result, unlike Hoare logics

Theorem: If is semantically valid, then is derivable by the proof system, with the operational semantics of a language.

34

ImplementationPart of the K framework (k-framework.org)Operational semantics and program properties

represented as K rules

Automatic prover (user specified properties) symbolic execution based on the K semantics Circularity for repetitive behaviors custom prover for matching logic implications

Java (mostly) and Z3 (for theory reasoning)

35

NarrowingConcrete execution

ground configuration rewritingSymbolic execution

symbolic configuration narrowingunification modulo theories

Narrowing generalizes control flow proof rulescode sample

construct operational semantics

36

ConclusionSound and relatively complete proof system

Circularity generalizes language specific proof rules for repetitive behaviors (loops, recursive functions, …)

Implemented as part of the K frameworkLanguage independent program verification

based solely on operational semantics is possible