Computer aided verification

Computer aided verification

Lecture 8:

Abstraction

Sławomir Lasota University of Warsaw

Abstraction

– Model M = (S, S0, L, R)

– Abstraction = reduction of the size of the model by removing irrelevant details

system

 //

 //

correctness property

 //

.

n 77n n n n n n n n n n n n n

n

M  φ ?

Abstraction

– Model M = (S, S0, L, R)

– Abstraction = reduction of the size of the model by removing irrelevant details

system

 //

 //

correctness property

 //

.

n 77n n n n n n n n n n n n n

n

M  φ ?

– We hope that computing cM and checking cM |= φ is cheaper than checking M |= φ.

Abstraction

– Model M = (S, S0, L, R)

– Abstraction = reduction of the size of the model by removing irrelevant details

system

 //

 //

correctness property

 //

.

n 77n n n n n n n n n n n n n

n

M  φ ?

– We hope that computing cM and checking cM |= φ is cheaper than checking M |= φ.

– Abstract model cM = ( bS, cS₀, bL, bR) (concrete model M = (S, S0, L, R))

Existential abstraction

Existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

Existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

– Abstraction function h : M → cM (h : S → bS)

Existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

– Abstraction function h : M → cM (h : S → bS) – Existential abstraction:

– ∃s ∈ S⁰. h(s) = bs =⇒ bs ∈ cS₀

– ∃s, s^′ ∈ S. R(s, s^′) ∧ h(s) = bs ∧ h(s^′) = bs^′ =⇒ Rb(bs, bs^′)

Existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

– Abstraction function h : M → cM (h : S → bS) – Existential abstraction:

– ∃s ∈ S⁰. h(s) = bs =⇒ bs ∈ cS₀

– ∃s, s^′ ∈ S. R(s, s^′) ∧ h(s) = bs ∧ h(s^′) = bs^′ =⇒ Rb(bs, bs^′)

Minimal existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

– Abstraction function h : M → cM (h : s → bS) – Minimal existential abstraction:

– ∃s ∈ S⁰. h(s) = bs ⇐⇒ sb∈ cS₀

– ∃s, s^′ ∈ S. R(s, s^′) ∧ h(s) = bs ∧ h(s^′) = bs^′ ⇐⇒ Rb(bs, bs^′) – We say that cM overapproximates M.

Model

Hardware: M = (S, S0, L, R) V = {x¹, . . . , xn} S = Dⁿ R, S₀, L represented by formulas

abstraction applies to representation of the model

Software: abstraction applies to program source running example: predicate abstraction

Predicate abstraction – basic idea

Example: Predicate x > 0

h_x>0 : D → {true, false} h_x>0(d) =

true d > 0 false d ≤ 0

Predicate abstraction – basic idea

Example: Predicate x > 0

h_x>0 : D → {true, false} h_x>0(d) =

true d > 0 false d ≤ 0

x = 0

_

x−−



false

_

x−−



Predicate abstraction – basic idea

Example: Predicate x > 0

h_x>0 : D → {true, false} h_x>0(d) =

true d > 0 false d ≤ 0

x = 0

_

x−−



false

_

x−−



x = 5

_

x−−



true

_

x−−



nondeterminism!

Boolean programs

h : Dⁿ → {true, false}^m

Correctness via simulation

Simulation game G

M c M

– players: Spoiler, Duplicator

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM)

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a transition s −→ r in M (assuming M total) – Duplicator answers with a transition bs −→ br in cM (assuming cM total) – the play continues from the configuration hr, bri

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a transition s −→ r in M (assuming M total) – Duplicator answers with a transition bs −→ br in cM (assuming cM total) – the play continues from the configuration hr, bri

– if the play is infinite, Duplicator wins

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a transition s −→ r in M (assuming M total) – Duplicator answers with a transition bs −→ br in cM (assuming cM total) – the play continues from the configuration hr, bri

– if the play is infinite, Duplicator wins

Question: How to adapt the definition for non-total models?

Simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a transition s −→ r in M (assuming M total) – Duplicator answers with a transition bs −→ br in cM (assuming cM total) – the play continues from the configuration hr, bri

– if the play is infinite, Duplicator wins

Question: How to adapt the definition for non-total models?

Question: How to adapt the definition for models with more initial states?

Simulation pre-order

Def.: M  cM ⇐⇒ Duplicator has a winning strategy in the game GM cM

Example:

GFED

@ABC

 ?>=<

89:;

}}|| || || || ||

C !!C C C C C C C C

7654

0123 ?>=< 89:;

≡

6

GFED

@ABC

}}|| || || || |

C !!C C C C C C C C

?>=<

89:;



?>=<

89:;

 7654

0123 ?>=< 89:;

Correctness via simulation

Simulation preorder is conservative:

Thm.: M  cM =⇒ (∀φ ∈ ACTL^∗. cM  φ =⇒ M  φ)

Correctness via simulation

Simulation preorder is conservative:

Thm.: M  cM =⇒ (∀φ ∈ ACTL^∗. cM  φ =⇒ M  φ) Thm.: M  cM =⇒ (∀φ ∈ ECTL^∗. M  φ =⇒ M  φ)c

Correctness via simulation

Simulation preorder is conservative:

Thm.: M  cM =⇒ (∀φ ∈ ACTL^∗. cM  φ =⇒ M  φ) Thm.: M  cM =⇒ (∀φ ∈ ECTL^∗. M  φ =⇒ M  φ)c

Def.: Simulation equivalence: ≃ =  ∩ 

Thm.: M ≃ cM =⇒ (∀φ ∈ ACTL^∗. cM  φ ⇐⇒ M  φ)

Correctness of existential abstraction

[Clarke, Grumberg, Jha, Lu, Veith 2003]

Abstraction function h : M → cM

Thm.: M  cM, if h preserves the atomic properties

Fair simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

Fair simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a fair path s −→ s¹ −→ s² −→ . . . (assuming M total) – Duplicator answers with a fair path bs −→ bs₁ −→ bs₂ −→ . . .

– Spoiler chooses i

– the play continues from the configuration hsⁱ, bsii

Fair simulation game G

M c M

– players: Spoiler, Duplicator – configurations: hs, bsi

– initial configuration: hs⁰, bs₀i (assuming one initial state in M and cM) – if L(s) 6= L(bs), Spoiler wins

– a round

– Spoiler chooses a fair path s −→ s¹ −→ s² −→ . . . (assuming M total) – Duplicator answers with a fair path bs −→ bs₁ −→ bs₂ −→ . . .

– Spoiler chooses i

– the play continues from the configuration hsⁱ, bsii – if the play is infinite, Duplicator wins

Summary

M  cM ∀φ ∈ ACTL^∗. cM  φ =⇒ M  φ M ^F Mc ∀φ ∈ ACTL^∗. cM ^F φ =⇒ M ^F φ M ≃ cM ∀φ ∈ ACTL^∗. M  φ ⇐⇒ cM  φ M ≃^F Mc ∀φ ∈ ACTL^∗. M ^F φ ⇐⇒ cM ^F φ M ∼ cM ∀φ ∈ CTL^∗. M  φ ⇐⇒ cM  φ M ∼^F Mc ∀φ ∈ CTL^∗. M ^F φ ⇐⇒ cM ^F φ Lω(M ) ⊆ L^ω( cM) ∀φ ∈ LTL. cM  φ =⇒ M  φ Lω(M ) = Lω( cM) ∀φ ∈ LTL. M  φ ⇐⇒ cM  φ

CEGAR

CEGAR

Counter-example guided abstraction refinement (1) Compute initial abstraction

CEGAR

Counter-example guided abstraction refinement

(1) Compute initial abstraction (2) Repeat:

– verify the abstract model

– if the result positive – answer yes and stop

– if the result negative – abstract counterexample

CEGAR

Counter-example guided abstraction refinement

(1) Compute initial abstraction (2) Repeat:

– verify the abstract model

– if the result positive – answer yes and stop

– if the result negative – abstract counterexample – check feasibility of the counterexample

– if the counterexample feasible – answer no and stop

CEGAR

Counter-example guided abstraction refinement

(1) Compute initial abstraction (2) Repeat:

– verify the abstract model

– if the result positive – answer yes and stop

– if the result negative – abstract counterexample – check feasibility of the counterexample

– if the counterexample feasible – answer no and stop

– refine the abstraction to eliminate the unfeasible counterexample

CEGAR loop

M, φ

  

 

computation of

abstraction abstract model cM

//

 

 

verification Mc |= φ?

counterexample

 //

 

 

abstraction refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

CEGAR loop

M, φ

  

 

computation of

abstraction abstract model cM

//

 

 

verification Mc |= φ?

counterexample

 //

 

 

abstraction refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

– correctness: whenever CEGAR stops the answer is correct

CEGAR loop

M, φ

  

 

computation of

abstraction abstract model cM

//

 

 

verification Mc |= φ?

counterexample

 //

 

 

abstraction refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

– correctness: whenever CEGAR stops the answer is correct

predicate abstraction in CEGAR

(instrumented) program

  

 

computation of abstraction

boolean program

//  





counterexample = execution path

 //

 

 

predicate refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

CEGAR: initial abstraction

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR example

[T. Ball, S. K. Rajamani 2000]

CEGAR: computation of abstraction

(instrumented) program

  

 

computation of abstraction

boolean program

//  





counterexample = execution path

 //

 

 

predicate refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

CEGAR: computation of abstraction

h : D^m → {true, false}ⁿ

CEGAR: computation of abstraction

h : D^m → {true, false}ⁿ

– bS = {true, false}ⁿ

CEGAR: computation of abstraction

h : D^m → {true, false}ⁿ

– bS = {true, false}ⁿ

– R(~b y, ~y^′) ≡ ∃~x, ~x^′. R(~x, ~x^′) ∧ ~y=h(~x) ∧ ~y^′=h(~x^′)

x₁, . . . , xm

R

//

~

y=h(~x)



x^′₁, . . . , x^′_m

~

y^′=h(~x^′)



Rb

//

CEGAR: computation of abstraction

h : D^m → {true, false}ⁿ

– bS = {true, false}ⁿ

– R(~b y, ~y^′) ≡ ∃~x, ~x^′. R(~x, ~x^′) ∧ ~y=h(~x) ∧ ~y^′=h(~x^′)

x₁, . . . , xm

R

//

~

y=h(~x)



x^′₁, . . . , x^′_m

~

y^′=h(~x^′)



Rb

//

– cS₀(~y) ≡ ∃~x. S⁰(~x) ∧ ~y=h(~x)

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract transitions:

R(bb 1, b₂, b^′₁, b^′₂) ≡

∃d⁰, e₀, d₁, e₁.

d^′ = e ∧ e^′ = e + 1 ∧

b₁ = (e ≥ 0) ∧ b² = (e ≤ 100) ∧ b^′₁ = (e^′ ≥ 0) ∧ b^′2 = (e^′ ≤ 100)

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract transitions:

R(bb 1, b₂, b^′₁, b^′₂) ≡

∃d⁰, e₀, d₁, e₁.

d^′ = e ∧ e^′ = e + 1 ∧

b₁ = (e ≥ 0) ∧ b² = (e ≤ 100) ∧ b^′₁ = (e^′ ≥ 0) ∧ b^′2 = (e^′ ≤ 100)

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

– nondeterminism

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract transitions:

R(bb 1, b₂, b^′₁, b^′₂) ≡

∃d⁰, e₀, d₁, e₁.

d^′ = e ∧ e^′ = e + 1 ∧

b₁ = (e ≥ 0) ∧ b² = (e ≤ 100) ∧ b^′₁ = (e^′ ≥ 0) ∧ b^′2 = (e^′ ≤ 100)

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

– nondeterminism

– calls to a prover or SMT-solver

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract transitions:

R(bb 1, b₂, b^′₁, b^′₂) ≡

∃d⁰, e₀, d₁, e₁.

d^′ = e ∧ e^′ = e + 1 ∧

b₁ = (e ≥ 0) ∧ b² = (e ≤ 100) ∧ b^′₁ = (e^′ ≥ 0) ∧ b^′2 = (e^′ ≤ 100)

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

– nondeterminism

– calls to a prover or SMT-solver

– non-minimal abstraction (for minimal one, exponential number of calls)

CEGAR: computation of abstraction

– simple block: d := e; e++ 7→ d^′ = e ∧ e^′ = e + 1 – predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract transitions:

R(bb 1, b₂, b^′₁, b^′₂) ≡

∃d⁰, e₀, d₁, e₁.

d^′ = e ∧ e^′ = e + 1 ∧

b₁ = (e ≥ 0) ∧ b² = (e ≤ 100) ∧ b^′₁ = (e^′ ≥ 0) ∧ b^′2 = (e^′ ≤ 100)

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

– nondeterminism

– calls to a prover or SMT-solver

– non-minimal abstraction (for minimal one, exponential number of calls)

CEGAR: computation of abstraction

– iteratively call SAT-solver:

– a satisfying valuation 7→ a blocking clause – bactracking to the highest decision level – the procedure stops when unsatisfiable

b₁ b₂ b^′₁ b^′₂

0 1 0 1

0 1 1 1

1 0 0 1

1 0 1 0

1 1 1 0

1 1 1 1

CEGAR: computation of abstraction

– control flow: if(e > 50) {goto l} else {goto l’}

– predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

CEGAR: computation of abstraction

– control flow: if(e > 50) {goto l} else {goto l’}

– predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract control flow: if(b₁ ∨ ¬b²) {goto l} + if(b₁ ∨ b²) {goto l’}

CEGAR: computation of abstraction

– control flow: if(e > 50) {goto l} else {goto l’}

– predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract control flow: if(b₁ ∨ ¬b²) {goto l} + if(b₁ ∨ b²) {goto l’}

– abstract guards not necessarily disjoint!

CEGAR: computation of abstraction

– control flow: if(e > 50) {goto l} else {goto l’}

– predicates: b₁ = (e ≥ 0), b² = (e ≤ 100)

– abstract control flow: if(b₁ ∨ ¬b²) {goto l} + if(b₁ ∨ b²) {goto l’}

– abstract guards not necessarily disjoint!

– typically if (while) guards are among predicates

CEGAR: verification

(instrumented) program

  

 

computation of abstraction

boolean program

//  





counterexample = execution path

 //

 

 

predicate refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

CEGAR: verification

– SMC may be convenieniently used (if no recursion nor dynamic allocation)

[Clarke, Kroening, Sharygina, Yorav 2004]

CEGAR: counterexample simulation

(instrumented) program

  

 

computation of abstraction

boolean program

//  





counterexample = execution path

 //

 

 

predicate refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

CEGAR: counterexample simulation

abstract counterexample b1 b2 b3 b4

[Clarke, Grumberg, Jha, Lu, Veith 2003]

counterexample simulation (strongest post-condition)

S₁ := S0 ∩ h⁻¹( b1 ) Si := ~R(S_i−1) ∩ h⁻¹( bi )

CEGAR: spurious counterexample

abstract counterexample b1 b2 b3 b4

[Clarke, Grumberg, Jha, Lu, Veith 2003]

S₄ = ~R(S3) ∩ h⁻¹( b4 ) = ∅ S₃ ∩ ~R⁻¹(h⁻¹( b4 )) = ∅

CEGAR: infinite counterexample

abstract counterexample bs₁( bs₂sb₃)^ω

[Clarke, Grumberg, Jha, Lu, Veith 2003]

– unfold the loop min{size( bs₂), size( bs₃)} times

CEGAR: predicate refinement

(instrumented) program

  

 

computation of abstraction

boolean program

//  





counterexample = execution path

 //

 

 

predicate refinement

OO

 

 

counterexample

simulation ^feasible

//

unfeasible

oo

aim: elimination of the spurious counterexample

CEGAR: predicate refinement

– spurious counterexample:

R(~x₁, ~x₂) ∧ R(~x², ~x₃) ∧ . . . ∧ R(~xn−1, ~xn) unsatisfiable

CEGAR: predicate refinement

– spurious counterexample:

R(~x₁, ~x₂) ∧ R(~x², ~x₃) ∧ . . . ∧ R(~xn−1, ~xn) unsatisfiable

– Craig interpolation: exists a formula φ(~xi) such that – φ(~xi) only uses variables xi

– R(~x₁, ~x₂) ∧ . . . ∧ R(~xⁿ⁻¹, ~xi) =⇒ φ

– φ ∧ R(~xⁱ, ~x_i+1) ∧ . . . ∧ R(~xn−1, ~xn) unsatisfiable

CEGAR: predicate refinement

– spurious counterexample:

R(~x₁, ~x₂) ∧ R(~x², ~x₃) ∧ . . . ∧ R(~xn−1, ~xn) unsatisfiable

– Craig interpolation: exists a formula φ(~xi) such that – φ(~xi) only uses variables xi

– R(~x₁, ~x₂) ∧ . . . ∧ R(~xⁿ⁻¹, ~xi) =⇒ φ

– φ ∧ R(~xⁱ, ~x_i+1) ∧ . . . ∧ R(~xn−1, ~xn) unsatisfiable

– For propositional logic, extract Craig interpolant from SAT-solver output

CEGAR: BDD + SAT

(instrumented) program

  





//  





counterexample = execution path

 //

 





OO

 





//

unfeasible

oo

Software verification success story

– 85% of system crashes of Windows XP caused by bugs in third-party kernel-level device drivers (2003)

– one of reasons is the complexity of the Windows drivers API

– SLAM: automatically checks device drivers for certain correctness properties with respect to the Windows device drivers API

– now part of Windows Driver Development Kit, a toolset for drivers developers