Transcript intro - Department of Computer Science

Course Overview
CS 680: Formal Methods for Verification of Computer
Systems
Jeremy Johnson
Drexel University
Course Description

This course is devoted to verification of
computer systems including both hardware and
software. Verification and Validation is the
process of checking that a computer system
meets its specifications and fulfills its intended
purpose. This course covers techniques and
tools for computer verification with an emphasis
on formal methods of verification which use
mathematical techniques to prove that
computer systems meet their specifications.
1
Course Themes






Propositional and predicate logic
Specification and verification of computer systems
SAT solvers and fast practical tools for checking the satisfiability of
boolean formulas
Temporal logic and model checking
Generation of test cases and counter examples
Automatic theorem proving and proof assistants
2
Course Topics










Week 1: Propositional Calculus
Week 2: Natural Deduction
Week 3: SAT solvers
Week 4: Predicate Calculus
Week 5: ACL2 Proof Assistant
Week 6: ACL2 Proof Assistant
Week 7: ACL2 Proof Assistant
Week 8: Temporal Logic and Model Checking
Week 9: Model Checking
Week 10: Model Checking
3
Audience and Prerequisites

This is a graduate elective appropriate for
graduate students in Computer Science,
Computer Engineering, Software Engineering
and Mathematics.

Undergraduate degree in CS, CE, SE, or
MATH. Students are expected to have solid
programming skills, be familiar with software
design and development, and have had some
introduction to logic and mathematical proof.
4
Course Objectives





To be able to use mathematical logic to formally specify
properties of computer systems
To be able to use state-of-the-art SAT solvers to solve
practical problems in verification
To be able to use a model checker to verify properties
of computer systems
To be able to use a proof assistant to prove properties
of computer systems
To be able to explain how SAT solvers, model
checkers, and proof assistants work
5
Course Benefits




To be able to provide more formal specifications
To be able to reason formally about computer systems
To be able to use automated tools in computer
verification
To be able to design and build more reliable computer
systems
6
Textbook and Required Software






Logic in Computer Science: Modelling and Reasoning
about Systems, 2nd Ed., Michael Huth and Mark Ryan,
2004.
Computer-Aided Reasoning: An Approach, Matt
Kaufmann, Panagiotis Manolios, and J Strother Moore,
Kluwer Academic Publishers, June, 2000.
MiniSat
ACL2
ACL2s
NuSMV
7
Course Logistics
Online and in class students combined
 Lectures W 6-9 (streamed and recorded)
 Weekly readings and labs



Checked off in class or through BbLearn
submission
Three projects (MiniSat, ACL2, NuSMV)
done in two student teams
 Must use of specified SW on chosen problem
 Requires ppt presentation (with audio)
8

Grading

Course Requirements and Grading

Weekly labs and course participation (40%)

Three Projects [SAT solver, Proof Asst,
Model Checker] (60% - each worth 20%)
9
Software Bugs



In 1980, NORAD reported that the US was under missile attack.
The problem was caused by a faulty circuit, a possibility the
reporting software hadn’t taken into account.
The Therac-25 medical radiation therapy device was involved in
several cases where massive overdoses of radiation were
administered to patients in 1985-87, a side effect of the buggy
software powering the device.
In 1996, a European Ariane 5 rocket was set to deliver a payload of
satellites into Earth orbit, but problems with the software caused
the launch rocket to veer off its path a mere 37 seconds after
launch.
10
Software Bugs



In 1994 in Scotland, a Chinook helicopter crashed and killed all 29
passengers. While initially the pilot was blamed for the crash, that
decision was later overturned since there was evidence that a
systems error had been the actual cause.
One of the subcontractors NASA used when building its Mars
climate orbiter had used English units instead of the intended
metric system, which caused the orbiter’s thrusters to work
incorrectly. Due to this bug, the orbiter crashed almost immediately
when it arrived at Mars in 1999. The cost of the project was $327
million, not to mention the lost time (it took almost a year for the
orbiter to reach Mars).
In 2002 NIST estimated that programming errors cost the US
economy $60B annually
11
Hardware Bug

Intel FDIV Bug




Intel P5 Pentium floating point unit
$500M
Error as high as the fourth significant digit of a
decimal number, but the possibilities of this
happening are 1 in 360 billion.
Approximately 8000 bugs introduced in during
design of Pentium 4.
12
Verification and Validation

Verification and Validation is the process
of checking that a SW/HW system meets
specifications and fulfills its intended
purpose
Features
Tie-Line Flows
PowerG rid
Real Time Analysis
Power System
Vulnerabilities
Real Time Analysis
Power System
Reliability
Excellent Training
Facility for Concerned
Parties
Hardware Power System
Model
Decision Making
Station
Engineering
Analysis Station
Economic Analysis
Station
Ultra-Fast Bus
13
Empirical Testing

Traditionally, errors in hardware and software
have been detected empirically by testing

Number of possibilities too large so only a small
subset can be tested

E.G. Testing arithmetic operations on all 264 double
precision floating point numbers is infeasible
14
Formal Methods

In the context of hardware and software
systems, formal verification is the act of
proving or disproving the correctness of
intended algorithms underlying a system
with respect to a certain formal
specification or property, using formal
methods of mathematics
15
Success Stories






Verified the cache coherence protocol in the
IEEE Futurebus+ Standard
Analysis of Microsoft Windows device drivers
using SLAM
Non-overflow proof for Airbus A380 flight control
software
Verification of Pentium 4 floating-point unit with
a mixture of STE and theorem proving
NICTA’s embedded L4 microkernel
Compcert compiler
16
Approaches







Model Checking
Temporal logic, BDD, Z notation, …
Static Analysis
Type Checking
Logical Inference
 Automated theorem proving
Proof Checking
Program Derivation
17
Model Checking


model checking refers to the following problem: Given a model of
a system, test automatically whether this model meets a given
specification. Typically, the systems one has in mind are hardware
or software systems, and the specification contains safety
requirements such as the absence of deadlocks and similar critical
states that can cause the system to crash. Model checking is a
technique for automatically verifying correctness properties of
finite-state systems.
An important class of model checking methods have been
developed for checking models of hardware and software designs
where the specification is given by a temporal logic formula.
Pioneering work in the model checking of temporal logic formulae
was done by E. M. Clarke and E. A. Emerson[1][2][3] and by J. P.
Queille and J. Sifakis.
18
Automated
Theorem Proving



Formal proof by hand is difficult
Have proof checked or generated
automatically by a computer
Higher Order Logic, or HOL, is a widelyused tool for creating formal specifications
of systems, and for proving properties
about them. It has been used in both
industry and academia to support formal
reasoning in many areas, including
hardware and software verification. It can
be used to support any project which can
be defined in higher order logic, an
expressive logic originally developed as a
foundation for mathematics.
19
Proof Carrying Code

Proof-carrying code (PCC) is a software mechanism that allows a
host system to verify properties about an application via a formal
proof that accompanies the application's executable code. The host
system can quickly verify the validity of the proof, and it can
compare the conclusions of the proof to its own security policy to
determine whether the application is safe to execute. This can be
particularly useful in ensuring memory safety, i.e. preventing buffer
overflows and other vulnerabilities common in some programming
languages.

Proof-carrying code was originally described in 1996 by George
Necula and Peter Lee.
20
Static Analysis

Static program analysis (also static code analysis or SCA) is the
analysis of computer software that is performed without actually
executing programs built from that software. The term is usually
applied to the analysis performed by an automated tool.

A growing commercial use of static analysis is in the verification of
properties of software used in safety-critical computer systems and
locating potentially vulnerable code[3]. For example the following
industries have identified the use of static code analysis as a
means of improving the quality of increasingly sophisticated and
complex software: Medical software, Nuclear software.
21
Program Generation

program derivation is the derivation of a program from its
specification, by mathematical means.

To derive a program means to write a formal specification, which is
usually non-executable, and then apply mathematically correct
rules in order to obtain an executable program satisfying that
specification. The program thus obtained is then correct by
construction. Program and correctness proof are constructed
together.

Hoare logic, stepwise refinement, Bird-Meertens Formalism,
parallel program design, FLAME, SPIRAL
22
References












http://en.wikipedia.org/wiki/Verification_and_validation_(software)
http://en.wikipedia.org/wiki/Formal_verification
http://en.wikipedia.org/wiki/Model_checking
http://en.wikipedia.org/wiki/Temporal_logic
http://en.wikipedia.org/wiki/Automated_theorem_proving
http://en.wikipedia.org/wiki/Proof-carrying_code
http://en.wikipedia.org/wiki/Static_program_analysis
http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis
http://en.wikipedia.org/wiki/Program_derivation
E. Allen Emerson, The Beginning of Model Checking: A Personal
Perspective
John Harrison, Formal verification of floating-point arithmetic at Intel, June
2006.
John Harrison, Formal Verification in Industry (I), 1999.
23