Transcript KIV TOOL (Karlsruhe Interactive Verifier )

KIV TOOL
(Karlsruhe Interactive Verifier )
Anna Rossato – [email protected]
Index
 Introduction
– What is KIV
– Application areas
– History: former and current projects
 KIV system
– KIV features
– Using KIV
– Proof Support
 An example
– Java Smart Card
The KIV System
 tool for formal system development
 used to
– construct formal models
– design and to verify high assurance systems
 used in
– industrial pilot applications
– in formal methods courses as an educational
tool
Why Formal Methods
 software failures can
– cause significant economic loss
– endanger human life or environmental damage
 formal methods use mathematics as a
sound basis for
– describing the structure of the system in a
formal specification
– finding the properties of the system
– symplifing the whole software
KIV Application Areas
 specification and verification of software
systems
 development of safety critical systems, from
formal requirements specifications to
executable code
 semantical foundations of programming
language, from a specification of the
semantics to a verified compiler
 other areas, like mathematics
KIV History
 KIV started in 1986 at the University of
Karlsruhe
– first project sponsored by the DFG (German
Research Foundation)
– focus on tactical theorem proving
– PPL, the basic framework of the KIV system,
was developed
KIV History
 work continued in 1992 with two projects:
– KORSO, sponsored by the BMFT (German
ministry of research)
 theory of modular, sequential software systems was
developed and implemented
 strategy for the reuse of proofs
– VSE (Verification Support Environment),
sponsored by the BSI (German Security
Agency)
 a case tool and an automatic theorem prover were
integrated with the KIV system
KIV History:
Current Projects
 functional Verification of JavaCard Applets
– the study investigates costs, benefits,
requirements to formally verify Java Card
programs
 VSE-II
– extension of the application domain of the VSE
to distributed, reactive systems
– improvements to the productivity and
ergonomics of the VSE system for its use in
industrial projects
KIV History
Current Projects
 FORMOSA (Integrating FORmal MOdels
and Safety Analysis)
– method for the systematic development of formal
models for high assurance systems
 SMaCOS (Secure Multiapplicative
SmartCard Operating System)
 generic formal security model for multiplicative
smartcards
 Asbru Medical Protocols
– formally verifying the correctness of medical
treatment protocols
KIV Features
 different specification and implementation
techniques, usying a Higher-Order variant of
Dynamic Logic
 powerful proof support
– automation, heuristics, simplification
 a large library of standard data types
 ergonomical graphical user interface
 documentation facilities for all levels of
development
PPL
 the meta-language of the KIV system is PPL
– typed functional language in the style of ML
 the basic data structure of PPL are proof
trees of sequents
– the root is the assertion to be proved
– the leaves are closed if they correspond to
some axiom, or open if the proof is partial
– each step in a proof tree corresponds to a rule
application
Using KIV
 KIV handles every single software system in
a project, consisting of
– specification components
– implementation modules
– their dependencies
Software development
environment
KIV
Start
Project 1
Spec 1
…
…
Project k
DaVinci
Specification/Module
Module m
Proof 1
…
Proof n
Specification/Module
Strategy
Specification
 structured algebraic specifications
– signature
– axioms
– principles of induction
 to create a new specification
– choose its type
– type its text
– install it (its syntactical correctness is
automatically checked)
– work on it
– when all theorems are proved, it can be set in
the Proved State
Implementation modules
 used to implement one abstract data type,
i.e. a specification, on the basis of another
 consist of
– an export interface: the specification to
implement
– an export interface: the specification of the used
data type
– a mapping that defines the corrispondance
between the export interface, the import one
and the module implementation
– the implementation: procedure declarations that
implement the export operations
Implementation modules
 each one has some files
– module: text for the module
– sequents: to enter or modify theorems
– module-specific: pattern of the heuristics
– formulas: to enter complex formula for rules
– proofs: theorem base and all proofs
– doc: documentation automatically generated
Dependencies
 dependencies between specification and
module form a directed acyclic graph
 represented with DaVinci development
graphs
KIV walkthrough
 example: implementing ordered sets by ordered
lists
– sets are generated by the empty set and insert which
adds an element to a set
– specification: orderset
– module: ordeset-module
 what to do?
–
–
–
–
write the import and export specification
proof the specification until it is set in the proved state
write the implementation module
proof the module
KIV walk through:
Project selection
KIV walk through:
Work on specification
KIV walk through:
Work on implementation
Proof Support
 the heart of KIV is a tactical theorem prover
 construction of proofs is done by
– applying tactics, selectioned by heuristics
– reducing goals to subgoals
 if all heuristics fail, the user may
– select tactics or heuristics
– backtracking (If the choice proves incorrect,
computation backtracks or restarts at the point of choice
and tries another choice)
– pruning the proof tree
– introducing lemmas
Proof Support:
Rules
 two kinds of rules
– basic rules
– user-defined rules
 rules may be schematic, in that their
sequents may contain meta-variables for all
syntactical categories
S1
S2
S
…
Sn
C
Proof Support:
Proof tactics
 proofs are supported by an advanced interactive
deduction component based on proof tactics
– simplification
– lemma application
– induction for first-order reasoning
 first order induction systems do not typically allow quantification
over predicates. But, unlike first order systems, all objects are
assumed to be finite.
– proof strategy based on symbolic execution
 a static analysis technique in which program execution is
simulated using symbols, such as variable names, rather than
actual values for input data, and program outputs are expressed
as logical or mathematical expressions involving these symbols
Proof Support:
Heuristics
 rules that reduces or limits the search for solutions
in domains that are difficult. Unlike algorithms,
heuristics do not guarantee optimal solutions
 to automate proofs (for both specifications and
modules) KIV offers a number of heuristics
– induction
– simplification
– ...
 heuristics can be chosen freely and changed any
time during the proof
 heuristics manage to find 80 - 100 % of the
required proof steps automatically
Proof Support:
Simplifier
 a complete proof for φ means to simplify φ in the
formula true
 simplifier rules describe what simplification step
should be done
 KIV handles thousands of rules, using some
extensions like forward reasoning
– given an implication of the form:
If conditions then conclusion
and a collection of statements that match the conditions,
forward reasoning derives the conclusion as a logical
consequence of the conditions
 the user explicitly chooses the simplification rules
Proof Support:
Proof engineering facilities
 the problem in engineering high assurance
systems is to interpret failed proof
– errors in specifications, programs, lemmas etc
 the user is assisted in the decision whether
the goal to prove is not correct, proof
decisions were incorrect, or there is a flaw in
the specification
Proof Support:
Proof reuse
 both successful and failed proof attempts
are reused automatically to guide the
verification after corrections or modifications
 90% of a failed proof attempt can be
recycled for the verification after correction
Proof Support:
Correctness management
 changes to or deletions of specifications,
modules, and theorems do not lead to
inconsistencies
 proofs can be done in any order
 only the minimal number of proofs are
invalidated after modifications
 there are no cycles in the proof hierarchy
 all used lemmas are been proved
Java Smart Card
 Java Cards are
– open
– portable
– component of distributed systems
– GSM computer (in cellular phones)
 but
– limited resources
– few innovative application realised
Java Smart Card
The project
 objective: improving the security of
application JSC for internet based usage
 formal design metodology for
multi
– abstract and modular specification for innovative
applications
– formalization and proof of security objectives
– implementation and verification of JavaCard applet
– NOT physical tampering and cryptographic algorithms
 deveploment of a security policy for a multi
application JC
Java Smart Card
An Application
 application
– purchase and transfer of a railroad ticket via
mobile phone
– SmartCard contains
 ticket
 ticketing applet (Railroad Company)
 digital signature capability (Trust Center)
Java Smart Card
An Application
Java Smart Card
Security objectives
 customer
– ticket genuine, anonymous, trasferible
– loading a ticket modifies no other data on the
card
– purchase and restitution are provable
 railroad company
– no forgery and copying possible
– no multiple usage
– offline ticket inspection
– no repudiation of expense claim
Java Smart Card
Security mechanisms
 modular combination of protocol and
cryptographic methods
 authentication with PIN
 public key cryptography for tamper-proof
signature
 nonrepudation through time stamps and
trust center
 uniqueness with session keys
Java Smart Card
Formal methods
is this a correct
implementation
of
the protocol?
 formal specification
of use cases and
protocols
 formalization
of
security objectives
 proof of security
Java Smart Card
Formal methods
 verification of JC programs
– correctness of command encoding
– correctness of data encoding
– bounded resources
– time conditions
 advantage
– correctness
– no gaps
Java Smart Card
Formal methods
 the semantic chosen is the natural one,
defined relatively to an algebraic
specification
– the full semantics of the language constructs is
described in 123 rules
 every one describes exactly one case that may occur
during evaluation
 proof rules are specified and implemented in
KIV and their corretness has been proved
 currently KIV is the only prover usable for a
Java Card calculus
References
 KIV at Karlsruhe
http://i11www.ira.uka.de/~kiv/KIV-KA.html
 KIV at Augsburg
http://www.informatik.uniaugsburg.de/swt/fmg/
 KIV at Saarbrücken
http://www.dfki.unisb.de/vse/projects/kiv.html
Higher Order Logic
 it has more expressive power then firstorder logic
 extends first-order logic with function that
have functions as argument and results
 function variables
 lambda expression λx.e that denote
anonymous function
Dynamic Logic
 extends predicate logic with two modal operators
– [.] box
[]φ
statement  terminates and afterwards φ holds
– <.> diamond
<>φ
if statement  terminates then afterwards φ holds
 allows the expression of properties of programs
like partial and total correctness, program
equivalence etc
example:
card.balance =1 |--- <card.change(17);>card.balance = 18
DaVinci development graph
specification
implementation module
DaVinci development graph
 each node
– corresponds to a specification component or a
implementation module
– has a theorem base attached, containing
 axioms
 automatically generated proof
 theorems added by the user
and managing proofs and their dependencies
– the colors show the status: planed, worked on,
proved
Sequents
 let φ1,…, φn,ψ1,… ψm DL(Σ,X)
(DL=Dynamic Logic) be two lists of formulas with
n,m>=0
φ1,…, φn |--- ψ1,… ψm
is called sequent
 It is a simple way to present
φ1Λ…Λφn → ψ1Λ…Λψm
Simplification
 simplifier rules are sequents whose syntactical
form describes what simplification step should be
done, i.e.
– Formula substitution step: a formula is substituted with a
simpler one
 Γ |--- φ → (ψ ↔ χ)
ψ is the formula to be simplified and χ the result of the
simplification
– Term rewriting step: a term is riwritten to another, simpler
one
 Γ |--- φ → ζ = σ
ζ is the term to be simplified and σ the result of the simplification