Transcript Program verification -

Program verification -- 096229
Ofer Strichman
Room 412
[email protected]
Office hours: after class
1
Agenda for the first class




Up to slide 36: what is this course about ?
Slide 37:
Slide 38-39:
Slide 40:
why not take this course
why take this course
requirements
2
The goal – reliable software systems


Importance of reliable software – almost
needless to mention.
A nice collection of famous bugs:
http://en.wikipedia.org/wiki/Software_bugs
3
The goal – reliable software systems

Here are some famous ones:

ESA Ariane 5 Flight 501 self-destruction 40 seconds
after takeoff (June 4, 1996).


A conversion from 64-bit floating point to 16 bit integer with
a value larger than possible with Arian 4. The overflow
caused a hardware trap.
The 2003 North America blackout was triggered by a
local outage that went undetetected.

A race condition in General Electric’s monitoring software
prevented an alarm.
4
The goal – reliable software systems

Here are some famous ones:

The MIM-104 Patriot bug, which resulted in the
deaths of 28 Americans in Dharan, Saudi Arabia
(February 25, 1991).



The radar classifies detections according to a trajectory
model it builds in real time. (“in x mSec the missile should be
in position y”)
Due to rounding of the clock values, it accumulates
inaccuracies. After several hours this inaccuracy is critical.
The Pentium bug


Incorrect floating-point division.
Cost Intel ~ $400,000,000
5
The goal – reliable software systems


Not unusual to have more than 50% of
resources allocated to testing
Testing and verification are (becoming) the
bottleneck of development
6
bEgInSlIdE
Remarks by Bill Gates
17th Annual ACM Conference on Object-Oriented
Programming, Seattle, Washington, November 8, 2002
“… When you look at a big commercial software company
like Microsoft, there's actually as much testing that
goes in as development. We have as many testers as we
have developers. Testers basically test all the time, and
developers basically are involved in the testing process
about half the time…
7
bEgInSlIdE
Remarks by Bill Gates
17th Annual ACM Conference on Object-Oriented
Programming, Seattle, Washington, November 8, 2002
“… We've probably changed the industry we're in.
We're not in the software industry; we're in the
testing industry, and writing the software is the thing
that keeps us busy doing all that testing.”
“…The test cases are unbelievably expensive; in fact,
there's more lines of code in the test harness than
there is in the program itself. Often that's a ratio of
about three to one.”
8
The goal – reliable software systems


Quality dilemma: quality / features / time
More efficient methods for test and verification
are always needed


No ‘silver-bullet’ when it comes to testing.
Formal verification is on the rise...
9
Formal methods

Formal = based on rigorous mathematical logic
concepts.


It is ‘machine-readable’, and hence can be used by a
verification algorithm.
Once we formally specify what we expect from
the program, we can try to prove that the
program satisfies the specification.
10
Specification can be: Informal, textual, visual...

Local assertions:
at this point in the program always
x > y.



How is it different than writing ‘assert ( x > y);’ ?
A more global property:
The array bound is never exceeded
Temporal properties:
If a request is sent,
acknowledgement is eventually
received
11
... or it can be formal
(1· x · 5 U x=7) Æ G (x¸ 0)
(Translated from: The value of x will be between 1
and 5, until at some point it will become 7, and it
will always (“Globally”) be positive.)
x=7
1· x · 5
x¸ 0
12
A system can be general and messy...
struct node *copy_node(struct node *f) {
static int count = 0;
struct node *temp;
count ++;
if (f == NULL) return NULL;
if ((temp = (struct node *) malloc (sizeof (struct
node))) == NULL)
fprintf(stderr,"Out of memory");
temp -> tag = f -> tag;
temp -> name = strdup(f -> name);
temp -> left = copy_node(f -> left);
temp -> right = copy_node(f -> right);
temp -> cnf_id = f -> cnf_id;
return temp;
}
13
... or its underlying algorithm can be modeled

E.g., as a finite-state machine
release
s1
pull
s2
extended
release
s3
malfunction
14
The program can be tested...

Try inputs





... As good as the set of input test-cases
... and as good as the reference system




x1 = 2, x2 = 25, str = ‘llk’
x1 = 0, x2 = 31, str = ‘aaa’
...
Manual inspection
Regression testing
Specification-based testing
For simple, non-critical code, this is the easiest
and most immediate option.
15
...or can be formally verified


Given the formal specification
G(:malfunction)
// always not malfunctioning
And the system model
release
s1
pull
s2
extended

release
s3
malfunction
Run a model-checker program to formally verify
that the system satisfies the specification.
16
bEgInSlIdE
Remarks by Bill Gates
17th Annual ACM Conference on Object-Oriented
Programming, Seattle, Washington, November 8, 2002
“We also went back and say, OK, what is the state-ofthe-art in terms of being able to prove programs, prove
that a program behaves in a certain way? This is the
kind of problem that has been out there for many
decades...
...When I dropped out of Harvard, this was an
interesting problem that was being worked on, and
actually at the time I thought, well, if I go and start a
company it will be too bad, I'll miss some of the big
breakthroughs in proving software programs because
I'll be off writing payroll checks. “
17
bEgInSlIdE
Remarks by Bill Gates
17th Annual ACM Conference on Object-Oriented
Programming, Seattle, Washington, November 8, 2002
...and it turns out I didn't miss all that much in terms
of rapid progress which now has become, I'd say, in a
sense, a very urgent problem. And although a full
general solution to that is in some ways unachievable,
for many very interesting properties this idea of proof
has come a long way in helping us quite substantially
just in the last year.
We call the system that does this kind of proof -- a
model-checking system.
18
Model-checking

Input:



A finite state machine M
A temporal property P P
Output: Does M satisfy P ?
01
00
10
P = “never in state 11”
11
M
19
Model-checking

Nondeterminism is used to model systems with
inputs
Model-checking is exponential in the number of
inputs
00
11
10
=
inputs
01
M
outputs

M
20
Model-checking


The model M defines a set of behaviors (traces)
L(M)
The model P defines a set of allowed behaviors
L(P)
01
00
10
11
11
M
P
Never “11”
21
Model-checking as language-inclusion
?

The model checking problem: L(M) µ L(P)
error
L(P)
L(M)

Q: What if this problem is too hard in practice?
22
Program verification


Bill: Prove that the program is correct !
MS-employee: let me quote Carl Popper’s
answer about verification vs. falsification in
science.


Science does not progress by finding eternal truths...
... only by refuting previous theories.
23
Program verification


Bill: Ok, So just prove that the program satisfies
the specification !
MS-employee :


ok ... but even if I prove that the system satisfies the
specification, there can still be an error in the proof
process or the proof tool that I use...
... and there is no guarantee that the specification
fully specifies what we consider as ‘correct’.
24
Program verification


Bill: Ok, fine, so just increase the probability
that the program is correct !
MS-employee :

Well, boss, if you want this process to be automatic,
please provide me



a model of the program, and
a formal (machine-readable) specification...
... Such that checking the model with respect to the
specification is a decidable problem.
25
Program verification


Bill: Will it be better than testing ?
MS-employee: when it is possible, it is much
better.
26
Testing / Formal Verification
A very crude dichotomy:
Testing
Correct with respect to the set of
test inputs, and reference system
Easy to perform
Dynamic
In practice:
Many types of testing,
Many types of formal verification.
27
Testing / Formal Verification
A very crude dichotomy:
Testing
Formal Verification
Correct with respect to the set of
test inputs, and reference system
Correct with respect to all inputs,
with respect to a formal
specification
Easy to perform
Decidability problems,
Computational problems,
Dynamic
Static
In practice:
Many types of testing,
Many types of formal verification.
28
Testing + formal-verification


Bill: is there a mid-way ?
MS-employee: Yes: Specify formally, verify
informally
This is called run-time verification...


The idea is to write a small program that monitors
the tested program
It checks during run-time that the tested program
satisfies a given (Formal) specification.
29
Where do we start ?




Bill: ok, where do we start ?
MS-employee: with some basics of Logics
Bill: Why Logic ?
MS-employee: I will show you an example.
30
Reminder: some Boolean connectives





Æ
Ç
:
!
$
and
or
not
implies
equal
A propositional formula: :(a Ç (b ! (c Æ : a)))
31
Program transformation
if(!a && !b)
h();
else if(!a)
g();
else f();
+
if(!a) {
if(!b) h();
else g(); }
else f();
if(a) f();
else if(b) g();
else h();
*
)
if(a) f();
else {
if(!b) h();
else g(); }
How can we check that these two versions are equivalent?
32
Code transformation example – cont’d

Represent procedures as independent Boolean
variables
original :=
if :a Æ b then h
else if :a then g
else f

optimized :=
if a then f
else if b then g
else h
Transform if-then-else chains into Boolean
formulas
transform(if x then y else z) ≡ (x Æ y) Ç (:x Æ z)

Check equivalence of boolean formulae
33
Code transformation example – cont’d
original
≡ if :a Æ :b then h else if :a then g else h
≡ (:a Æ :b) Æ h Ç :(:a Æ :b) Æ if :a then g else f
≡ (:a Æ :b) Æ h Ç :(:a Æ :b) Æ (:a Æ g Ç a Æ f )
optimized
≡ if a then f else if b then g else h
≡ (a Æ f ) Ç ( :a Æ if b then g else h )
≡ ( a Æ f ) Ç ( :a Æ (b Æ g Ç :bÆ h) )
Verification Condition :
((:a Æ :b) Æ h Ç :(:a Æ :b) Æ (:a Æ g Ç a Æ f )) $
(a Æ f ) Ç (:a Æ (b Æ g Ç :b Æ h))
The question: is  valid ?
34
Not just software...
Prove the equivalence of two circuits:
Ç
Æ
Ç
Æ
Ç
35
So...

We will learn:

A brief introduction to Propositional Logic



Incl. General logic jargon such as: validity, satisfiability,
soundness, completeness,...
In a later stage in the course we will also learn algorithms
for checking whether a given formula is valid/satisfiable
Temporal Logic, and its ability to formally specify
systems
36
So...

... and



... And also



Specification-based testing (specifically: Run-time
verification)
Other types of testing
Modeling of systems
Formal verification of systems against formal
specification with model-checking.
More... if we have the time
37
Why not take this course

In the end of the course you will NOT be able to
automatically verify the big software you wrote
in C



No one can, (completely) automatically.
After your Ph.D, you might be able to do it with some manual
guidance.
On the bright side ... with certain restrictions, or compromises
on what it means to ‘verify’, you might be able to verify even
large C programs.
38
Why take this course

There are some restricted type of programs that
can be verified automatically.



There is an industry behind it, incl. in Haifa.



Finite-state programs (e.g. protocols) and more.
The ‘killer-application’: hardware circuits.
Developers of verification tools: IBM, Intel.
Users of such tools: IBM, Intel, Melanox, Freescale, Verisity
(now Cadence), Galileo (now Marvel)...
Background in hardware is not necessary at all.

Most developers & users in this field do not have it.
39
Why take this course (cont’d)


Very different than other courses you took...
Combines





Theory (logic, automata-theory)
Algorithms
Acquaintance with type of programs and systems you
have probably not seen before.
Not difficult...
Only assumes ‘mathematical maturity’, not
specific knowledge.
40
Requirements


~5 homework assignments
2 exams, 3-questions each (1.5 hours).
41