CSCE 431 Lecture 19

« previous | Tuesday, April 1, 2014 | next »

Note: Spiral Model has proven best for mission critical software

Verification

Introduction

Correctness

System performs according to its specification, in cases covered by the specification

Robustness

System performs reasonably in cases not covered by its specification

Security

System's ability to protect itself against hostile (malicious) use

Testing, code reviews, static analysis, informal reasoning, etc. are useful in strengthening the belief that a program is correct.

If we want to guarantee correct behavior, we need proofs: two ways to do so — let fact be expressed by formula $P$

1. by inspecting a program and the requirements, and through the logical reasoning assure that $P$ must always be true. This often takes place with help from a proof assistant.
2. form a semantic model of the program, and check that $P$ holds in that model. This might mean "running" the model exhaustively to cover all possible states of the program. One might resort to using Model checkers.

Goal: understand static correctness proofs via modeling

Often, we do not wish to prove precise behavior of program. Rather, we want to prove some safety features.

Premises:

1. unambiguous language of specifying requirements
2. unambiguous language of specifying meaning of implementations

Specifying Implementations

operational semantics

program is stream of instructions to abstract machine

meaning of program: behavior / result of abstract machine

denotational semantics

define meaning of each language construct in some suitable semantic domain

i.e. define a model for the language

meaning of a program arises recursively as a composition of the meanings of sub-programs

axiomatic semantics

attach proof rules to each language construct, and eventually reach ...

Theory

A mathematical framework for proving properties about a certain object domain

Properties that are true are called theorems

Components of a theory:

• grammar (e.g. BNF)
• axioms (formulae asserted to be theorems)
• inference rules (ways to prove new theorems)

Definition: a theorem $t$ in a theory is a well-formed formula of the theory, such that $t$ may be derived from the axioms of zero or more inference rules.

Proof

• Each proof is a sequence of lines.
• Each line is numbered
• Each line contains a formula, which the line asserts to be a theorem.

Discovering a proof is insight

Checking a proof can be mechanized.

Interpretation and Models

A theory is purely a formal / syntactic mechanism that defines a set of formulae, and allows for deriving some of the formulae as theorems.

What the formulae represent is not defined.

Interpretation:

• Associate some member drawn from a suitable mathematical domain.

...

Theories About Programs

Formulae should be about properties of programs

Properties are expressed as assertions

Assertion is a property of some objects in the program. (May or may not be true in a praticular state in the program.)

Usually the language's concrete syntax of boolean expressions is used for assertions

Quantifiers (for all, exists, unique existence

Assertions in Programs

• Floyd, 1967
  • use assertions as foundation for static correctness proofs
  • specify assertions at every program point

• Hoare
  • Axiomatic semantics

• Dijkstra

Well-formed formulas of an axiomatic theory for a programming language are not mere assertions, but expressions that consist of both assertions and program fragments

Definition: A program fragment is correct with respect to a certain precondition $P$ and a certain precondition $Q$ if, when executed in a state in which $P$ is satisfied, it yields a state in which $Q$ is satisfied.

Soundness and Completeness

soundness

every deduced property holds of all corresponding program executions

completeness

every property that holds of all program executions can be proven by logic (this is, of course, undecidable)

Well-formed formulas are "Hoare triples"

$\left\{P\right\}A\left\{Q\right\}$

• $A$ is a program fragment
• $P,Q$ are predicates over the program state
• If $A$ is started in any state that satisfied $P$, the state after $A$ terminates will satisfy $Q$.

What if $A$ doesn't terminate?

Definition. A program fragment $A$ is totally correct with respect to $P$ and $Q$ if, when started in any state satisfying $P$, terminates in a state satisfying $Q$.

Definition. A program fragment $A$ is partially correct with respect to $P$ and $Q$ if, when started in any state satisfying $P$, if it terminates, does so in a state satisfying $Q$. (i.e. it need not terminate, and if it doesn't we can say anything about $Q$:

@pre{}
while (true) {}
@post{ P == NP }

Examples

{ T } x = 5 { x == 5 }
{ x == y } x = x + 3 { x == y+3 }
{ x > 0 } x = x * 2 { x > −2 }
{ x == a } if (x < 0) then x = -x { x == |a| }
{ F } x = 3 { x == 8 }

Program Structures =

skip

$\left\{P\right\}{\mbox{skip}}\left\{P\right\}$

assignment

$\vdash \left\{\left[e/x\right]\,Q\right\}x\gets e\left\{Q\right\}$

conditional

${\frac {\left\{B\wedge P\right\}S_{1}\left\{Q\right\}\quad \quad \left\{\neg B\wedge P\right\}S_{2}\left\{Q\right\}}{\left\{P\right\}{\mbox{if}}\ B\ {\mbox{then}}\ S_{1}\ {\mbox{else}}\ S_{2}\ {\mbox{end}}\left\{Q\right\}}}$

composition

${\frac {\left\{P\right\}S_{1}\left\{Q\right\}\quad \quad \left\{Q\right\}S_{2}\left\{R\right\}}{\left\{P\right\}S_{1};S_{2}\left\{R\right\}}}$

loop

Definition: A predicate that is true when entering in a loop, when entering a new iteration of a loop, and immediately after exiting the loop is a loop invariant $I$:

${\frac {\left\{B\wedge I\right\}S\left\{I\right\}}{\left\{I\right\}{\mbox{while}}\ B\ {\mbox{do}}\ S\ {\mbox{end}}\left\{\neg {B}\wedge I\right\}}}$

This demonstrates partial correctness

For total correctness, we have $V$, of type int, as a variant.

We assume $z$ is fresh (not written to in $B$)

${\frac {\left\{(B\wedge I)\implies V>0\right\}\quad \quad \left\{B\wedge I\right\}z\gets V;S\left\{I\wedge V<z\right\}}{\left\{I\right\}{\mbox{while}}\ B\ {\mbox{do}}\ S\ {\mbox{end}}\left\{\neg B\wedge I\right\}}}$

consequence

${\frac {\left\{P\right\}a\left\{Q\right\}\quad \quad P'\implies P\quad \quad Q\implies Q'}{\left\{P'\right\}a\left\{Q'\right\}}}$

it may seem that $\left\{x>1\right\}\implies \left\{x+x>2\right\}$, but in programming languages, if $x$ is an int (but not in $\mathbb {Z}$), then $x+x$ might wrap around to $x+x<0$.

Hence our definitions of $+$ and $>$ must be consistent with the assertions of the programming language.

conjunction

${\frac {\left\{P\right\}a\left\{Q\right\}\quad \quad \left\{P\right\}a\left\{R\right\}}{\left\{P\right\}a\left\{Q\wedge R\right\}}}$

Termination

Problematic language constructs are loops and recursion (if allowed in language)

Basic idea: if one can show that during each loop iteration, some measure gets smaller and eventually reaches a value from which it can no longer decrease, then the loop cannot go on forever.

The loop values must get substantially smaller (i.e. not $\left\{1,{\frac {1}{2}},{\frac {1}{4}},{\frac {1}{8}},\ldots \right\}$

This gives rise to the total correctness notation of the loop statement.

Dafny

• http://research.microsoft.com/en-us/projects/dafny/
• http://rise4fun.com/dafny/Hello

Language designed to be easy for writing provably correct code.

Correct means

• no runtime errors (index out of bounds, null pointer exceptions, etc)
• correct with respect to the intended meaning, where specification is given in the annotations.

Program may be rejected if

1. $Dafny$ finds annotations inconsistent with the implementations
2. Dafny is not "clever" enough to prove that the annotations are consistent with the implementation.