Elementi di Software Dependability - Software Safety

Precise abstraction

© Willem Visser 2002

Precise abstraction, w.r.t. the property being checked, may be obtained if the behaviors being removed are indeed not influencing the property.

Slicing– Program is an example of an automated under-approximation that will lead to a precise abstraction w.r.t. the property being checked.

Property-directed Slicing indirectly relevant Slicementioned Source program Resulting slicein property.

Slicing criterion generated automatically from observables mentioned in the property.

Backwards slicing automatically finds all components that might influence the observables.

Over-Approximations Abstract Interpretation

Maps sets of states in the concrete program to one state in the abstract program.

Reduces the number of states, but increases the number of possible transitions, and hence the number of behaviors.

Can in rare cases lead to a precise abstraction.

Type-based abstractions (-->)

Predicate abstraction

(-->)• Automated (conservative) abstraction

Problem: Eliminating spurious errors

Abstract program has more behaviors, therefore when an error is found in the abstract program, is that also an error in the original program?

Data Type Abstraction

Abstraction homomorphism h: int --> Sign

Replace by abstraction

int Sign {neg,pos,zero}

NEG if x<0

h(x) = ZERO if x =0

POS if x>0

Abstract Interpretation

Code

int x = 0; Sign x = ZERO;

h… …

if (x == 0) if (Sign.eq(x,ZERO))

x = x + 1; x = Sign.add(x,POS);

© Willem Visser 2002

Predicate Abstraction

Replace predicates in the program by boolean variables, and replace each instruction that modifies the predicate with a corresponding instruction that modifies the boolean.

T F

Abstract EQ = T EQ := F EQ = F

int int bool" : # EQ (x = y)

EQ (x = y) $$

Concrete x y x y

= ! y++

x = 0 x = 0

y = 0 y = 1

Mapping of a concrete system to an abstract system, whose states

correspond to truth values of a set of predicate

• Create an abstract transition system before model checking

How do we Abstract Behaviors?

• Abstract domain A – Abstract concrete values to those in A
• Then compute transitions in the abstract domain
  • Over-approximations: Add extra behaviors
  • Under-approximations: Remove actual behaviors

Underlying model: Kripke Structures

• M = (S, s, %>, L) on AP
  • S: Set of States
  • s: Initial State
  • %>: Transition Relation
  • L: S -> AP, Labeling on States
• Simulations on Kripke Structures
  • M = (S, s, L) -> 0
  • M' = (S', s', L') -> 0

Definition: R ⊆ S × S' is a simulation relation between M and M' if

1. L(s) = L'(s')
2. for all t such that s %> t, there exists t' such that s' %>' t' and (t, t') ∈ R

M' simulates M (M ⊆ M') if (s, t) ∈ R~' implies (s, t) ∈ R~ for all (s, t) ∈ M

• M concrete model, M’ abstract model

Strong Preservation:

• – M’ P iff M P|= |=

Weak Preservation:

• – M’ P M P|= => |=

Simulation:

• preserves ACTL* properties
• – If M M’ then M’ AG p M AG p~ |= => |=

Abstraction Homomorphisms:

• Concrete States S, Abstract states S’
• Abstraction function (Homomorphism)
• – h: S S’->– Induces a partition on S equal to size of S’
• Existential Abstraction - Over-Approximation
• – Make a transition from an abstract state if at least one corresponding concrete state has the transition.
• – Abstract model M’ simulates concrete model M
• Universal Abstraction - Under-Approximation
• – Make a transition from an abstract state if all the corresponding concrete states have the transition.

Existential Abstraction - Preservation

Let be a Universally quantified formula (es,

An ACTL* property M' existentially abstracts M, so M ~ M'

Preservation Theorem: M' |= |= M

Converse does not hold: M |= |= M'

(counterexample may be spurious: M' :|= )

NOTE: ACTL* is the universal fragment of CTL*

Universal Abstraction - Preservation:

Let be a existential-quantified property (i.e., expressed in ECTL*) and M simulates M'

Preservation Theorem: M' |= |= M

Converse does not hold: M |= |= M'

NOTE: ECTL* is the universal fragment of CTL*

Model Checking (safety):

I AG ~ unsafe (true property) = unsafe state

Abstraction: Under-Approximation

IAG ~ unsafe true (but it is not preserved)

Abstraction: Over-Approximation

I It is not a path in the concrete system

spurious AG ~ unsafe false counterexample

Refinement of the abstraction:

Separate states that are the reason of AG ~ unsafe true the spurious counterexample

Automated Abstraction/Refinement:

Counterexample-Guided AR (CEGAR) M' := abstract(M) - Build an abstract model M'

Model check property P, M’ P?|= No BugTM’ |= P– If M’ P, then M P by Preservation|= |=Theorem F– Otherwise, check if Counterexample (CE) Fspurious(CE) Bugis spurious T– Refine abstract state space using CE M’:= refine(M’)analysis results– Repeat Hand-Translation© Willem Visser 2002Early applications at NASA• Remote Agent – Havelund,Penix,Lowry 1997– http://ase.arc.nasa.gov/havelund– Translation from Lisp to Promela (most effort)– Heavy abstraction– 3 man months et al.• DEOS – Penix, Visser, 1998/1999– http://ase.arc.nasa.gov/visser– C++ to Promela (most effort in environment generation)– Limited abstraction - programmers produced sliced system– 3 man months© Willem Visser 2002Semi-Automatic Translation• Table-driven translation and abstraction– Feaver system by Gerard Holzmann– User specifies code fragments in C and how to translate

themto Promela (SPIN) – Translation is then automatic

Found 75 errors in Lucent’s PathStar system – http://cm.bell-labs.com/cm/cs/who/gerard/

Advantages:

• Can be reused when program changes
• Works well for programs with long development and only local changes

© Willem Visser 2002

Fully Automatic Translation

• Advantage: No human intervention required
• Disadvantage: Limited by capabilities of target system

Examples:

• Java PathFinder 1 - http://ase.arc.nasa.gov/havelund/jpf.html
• Translates from Java to Promela (Spin)
• JCAT - http://www.dai-arc.polito.it/dai-arc/auto/tools/tool6.shtml
• Translates from Java to Promela (or dSpin)
• Bandera - http://www.cis.ksu.edu/santos/bandera/
• Translates from Java bytecode to Promela, SMV or dSpin

Bringing Model Checking to Programs

• Allow model checkers to take programming languages as input, (or notations of similar expressive power)

Major

Problem: how to encode the state of the system efficiently

• Alternatively state-less model checking
• No state encoding or storing
• On the fly model checking
• Almost exclusively explicit-state model checking
• Abstraction can still be used as well
• Source to source abstractions

Custom-made Model Checkers

• Translation based
• dSpin
• Spin extended with dynamic constructs
• Essentially a C model checker
• Source-2-source abstractions can be supported
• http://www.dai-arc.polito.it/dai-arc/auto/tools/tool7.shtml

• SPIN Version 4
• PROMELA language augmented with C code
• Table-driven abstractions
• Bandera
• Translated Bandera Intermediate Language (BIR) to a number of back-end model checkers, but, a new BIR custom-made model checker is under development
• Supports source-2-source abstractions as well as property-specific slicing
• http://www.cis.ksu.edu/santos/bandera/

© Willem Visser 2002

Model Checkers

• Abstraction based
• SLAM
• C programs are abstracted via predicate abstraction to boolean programs for model checking
• http://research.microsoft.com/slam/
• BLAST lazy
• Similar basic idea to SLAM, but using abstraction, i.e. during abstraction refinement don't abstract the whole program only certain parts
• http://www-cad.eecs.berkeley.edu/~tah/blast/
• 3-Valued Model Checker (3VMC) extension of TVLA for Java programs
• http://www.cs.tau.ac.il/~yahave/3vmc.htm
• http://www.math.tau.ac.il/~rumster/TVLA/

© Willem Visser 2002

Java PathFinder (JPF)

Java Code Bytecode

void add(Object o) {
    buffer[head] = o;     // 0: iconst_0
    head = (head+1)%size; // 1: istore_2
}                         // 2: goto #39

Object take() {
    tail = (tail+1)%size; // 8: aload_0...
    return buffer[tail];  // 9: iload_2
}                         // 10: aaload

Model Checker

Special

JVM

Bandera & JPF

© Willem Visser 2002

Architecture

Translators

Property Tool

Abstraction BIR

Analyses Engine

BIRC

SPIN

SPIN is a Java Jimple (BC) Parser SMV Slicer Simulator Decompile; javac Error Trace Display JPF© Willem Visser 2002

One Case Study at NASA: DS-1

Remote Agent Spacecraft Commands Sensors Tasks Achieve Property Subscribe Data Property base Locks Lock Event Change Interrupt Event Properties Monitor

• Several person-months to create verification model.
• One person-week to run verification studies.

One Case Study at NASA: DS-1© Willem Visser 2002 Remote Agent Unexpected timing DB change? of change event Monitor Logic yes nowait check

• Five difficult to find concurrency errors detected
• "[Model Checking] has had a substantial impact, helping the RA team improve the quality of the Executive well"