# Presentation: 066126

## Qualifiable Model Checkers

- Songtao Xia and Ben Di Vito

## Outline

- Model checkers add functionality and flexibility to software certification
- Proof-carrying Code
- New applications
- Structure of model checkers
- Solution: reuse of transition information
- Plan

## Terminology

- Server: software developer obligated to show the correctness of the software
- Client: the regulatory authority responsible to independently verify a server’s claim
- Certificate: artifacts that the server presents to help prove the correctness
- Reverification: client’s activity to independently check the server’s claim
- Trust base: set of tools the client must trust to achieve reverification

## Software Certification

- Peer review/testing
- Advantage: easy to learn/understand process
- Disadvantage: we don’t know how much is enough
- Proof-carrying code
- Advantage: indisputable mathematical facts as certifcates, automation in tool support (for certain properties), small trust base
- Disadvantage: expressive power/automation trade off

## Proof-carrying code

- Server Side:

- Client Side:

- Program

- Verification
- Conditions

- Proof

- VCGen

- Theorem
- Prover

- ProofChecker

- VCGen

## Proof-carrying Code

- Automatic for certain properties
- Memory safety and type safety
- Other domain-specific properties
- Proof: property specific
- VCGen often tied to class of properties
- Not flexible

## Model Checker

- Software model checking with predicate abstraction
- For safety properties
- For engineering programs
- Protocol verification

## Using model checker

- Automation
- Functionality
- Flexibility
- But qualification issue
- Model checkers are more complicated than a proof-checker

## New Application 1:

- Server Side:

- Client Side:

- Program

- Spin Model

- ModelAbstraction

- Model Checker

- ModelChecker

- ModelValidator

## New Application 2:Abstraction-carrying Code (ACC)

- Server Side:

- Client Side:

- Program

- Boolean Program

- PredicateAbstraction

- Model Checker

- ModelChecker

- ModelValidator

## Predicate Abstraction

- Observe the program’s behavior over value changes of a set of predicates
- Example: consider x++ over x>0corresponding BP: if b then b:= true else b:= unknown, where b represents x>0
- Reduce state space

## BP Validator

- Validation of Hoare Triples:
-     {x>0} x++ {x>0}
- Implemented in ACCEPT (ACC Evaluation Prototype System) as dependent typed assembly language type checking

## Complexity of Model Checkers

- General purpose model checkers
- Explicit state model checkers
- Symbolic model checkers
- Spin, JPF, SMV,...
- Special purpose model checkers
- For an often simplified model
- Moped, Bebop

## Cost of software qualification

- Expensive

## Cost of software qualification

- More expensive
- for larger, more complicated programs
- Programs in the trust base must be qualified

## Structure of Model Checkers

- Search Engine

- State Management

- Next state =?

- Relatively Simple Search

- PathManagement

## Run Model Checker Twice

- Search Engine

- State Management

- Next state =?

- Relatively Simple Search

- PathManagement

- Chance to reuse information from previous run

## Run Model Checker Twice

- Search Engine

- Coverage Testing

- Is Next State x?

- Relatively Simple Search

- Optimization conditionverification

- Instead of computation, we verify the results

## Example: BP model checker

- BP statement: if (b1) then b2:= b1 && b3...
- If we know: nextState((1,1,0)) = (1,0,0))...
- We can use a Boolean evaluator, very efficient, a few lines of code
- Result: we can save ourselves a BDD library from the trust base!

## Research Plan

- Moped: a model checker for push-down systems
- Model checks BP
- BDD library is large than the source code itself
- Reduce the size of moped to a few thousands lines of code

## Evaluation Plan

- To watch: performance should not be severely affected
- ACCEPT/C
- A prototype we have built to evaluate Abstraction-carrying code
- Plug modified moped back to ACCEPT/C, evaluates its performance and compare it to the original Moped

## Related Work

- Proof-emitting model checkers
- Software model checking
- Model-carrying code