Formal Verification of Systems Software

Notes for EECS 498

• Imperative, Declarative (like SQL).
• int is mathematical integer.
• Immutatable is important (what about shadowing)
• Expression (evaluate a value) and Statement.
• Ghost (not compiled)
• Lemma syntax
• Pre and post conditions
• Prove by contradiction (?): a lemma proves false.
• The body of function is always visible.

Basics

Basic Quantifier

• forall x | Q(x) :: P(x)
• statement form,

forall x | Q(x)
  ensures P(x)
{

}

• exists needs a witness.

Imperative

predicate IsMaxIndex(a:seq<int>, x:int) {
  && 0 <= x < |a| 
  && (forall i | 0 <= i < |a| :: a[i] <= a[x])
}

Formal Specification

the most important part

Ways of specify:

• C-style assertions
• Postconditions
• Property / Invariants: “At most one node holds the lock at any time”
• Refinement: Linearizability. Equivalence to logically centralized service

Syntax

• Datatype member functions
• Calc statements: proves a=b=c=d using

calc {
  a;
  { MyUsefulLemma(a,b); }
  b;
  c;
  d;
}

• Choose operator var x :| x % 7 == 1; (choose x such that …)

• Modules

module A {
       predicate MyPredicate() { ... }
}
module B {
       import A
       predicate MySecondPredicate() { A.MyPredicate() }
}

State Machine

Sample

datatype Card = Shelf | Patron(name: string) 
datatype Book = Book(title: string)
type Variables = map<Book, Card>

ghost predicate Init(v: Variables) {
  forall b | b in v :: v[b] == Shelf
}

ghost predicate CheckOut(v : Variables, v' : Variables, book: Book, name: string)  {
  && book in v
  && v[book] == Shelf
  && (forall book | book in v :: v[book] != Patron (name))
  && v' == v[book := Patron(name)]
}

ghost predicate CheckIn(v : Variables, v' : Variables, book: Book, name: string) { 
  && book in v 
  && v[book] == Patron (name)
  && v' == v[book := Shelf]
}

ghost predicate Next(v: Variables, v': Variables) {
  || (exists book, name :: CheckOut(v, v', book, name))
  || (exists book, name :: CheckIn(v, v', book, name))
} 

Induction in Dafny

ghost predicate Next(v: Variables, v': Variables) {
  || (exists book, name :: CheckOut(v, v', book, name))
  || (exists book, name :: CheckIn(v, v', book, name))
} 

predicate Safety (v: Variables) {
  // No one has more than one book
  ! exists b1, b2 :: (b1 in v) && (b2 in v) && (b1 != b2) && (v[b1] == v[b2]) && (v[b1] != Shelf)
}