The KIV System
Overview
KIV is a tool for formal systems development and interactive verification. It can be employed, e.g.,
- for the development of safety critical systems from formal requirements specifications downto executable code, including the verification of safety requirements and the correctness of implementations,
- for semantical foundations of programming languages from a specification of the semantics downto a verified compiler,
- for building security models and architectural models as they are needed for high level ITSEC or CC evaluations.
More information on KIV can be found below:
- How to dowload KIV and its documentation.
- The KIV projects page gives online documentation for a number of recent specification and verification projects. It includes larger case studies of various types as well as the solutions to recent verification challenges that had to be solved in short time.
- KIV's specification language supports both the functional and the state-based approach to describe hierarchically structured systems. The functional approach is based on algebraic data types and higher-order logic, the state-based approach supports abstract sequential and concurrent programs, abstract state machines, statecharts, and sequential Java programs.
- KIV provides proof support for all elements of the specification language based on sequent calculus, efficient rewriting and symbolic execution of programs.
- Developing a software system requires support to deal with large specifications, handling large sets of theorems, and (most important) the iterative development of proofs. KIV provides a number of proof engineering facilities to help with this task.
- The development process of a correct software system typically start with an abstract specification, that is then step by step refined to become code of a programming language. KIV supports various types of refinement.
- KIV has an elaborate graphical interface.
Download KIV
Currently you can download KIV as part of a vmware-image or as a .tgz archive for linux.
VMWare-Image
Linux-ArchiveFor general help with the installation, please contact Gerhard Schellhorn. If you need support for java verification with KIV, please mail Kurt Stenzel. License AgreementKIV is copyrighted by University of Augsburg, Formal Methods group of the chair of Software Engineering (Prof. Reif). This license grants the signer a non-transferable and non-exclusive right to use KIV. This license is restricted to noncommercial use. KIV is provided on an "as is" basis, without warranty or liability of any kind. Licensee agrees not to modify, or disassemble any of the software files KIV consists of. This license is free of charge. Licensee also agrees to respect the license of clisp and uDraw, since both are contained in the distribution of KIV. |
Specification Language
The functional approach uses higher-order algebraic specifications. The first-order part is a subset of CASL. Specifications are built up from elementary specifications with the operations enrichment, union, renaming, parameterization and actualization. Specifications have a loose semantics and may include generation principles to define inductive data types.For the state-based approach KIV offers four approaches: Abstract State Machines (ASMs), parallel programs, state charts and the direct verification of sequential Java programs (including generics).
ASMs define rules (abstract sequential programs that are executed atomically) to describe state transitions. The semantics of an ASM is the set of traces generated by the transition relation defined by the rules of the ASM. Our variant of ASMs is based on algebraically specified data types. The abstract programs used to define rules used include parallel assignments, (infinite) nondeterminism (with choose) and mutually recursive procedures.
Parallel programs extend the sequential ones with additional operators to execute programs in parallel, using shared variables: both (weak-fair and unfair) interleaving as well as asyncronous parallel execution are supported. An await-operator is used for synchronisation.
Finally, KIV supports state charts, with a semantics based on micro and macro steps. Like programs, statecharts are embedded in the Temporal Logic of KIV (see below) as formulas.
Proof Support: Higher-Order, Dynamic and Temporal Logic
In KIV, proofs for specification validation, design verification, and
program verification are supported by an advanced interactive
deduction component based on proof tactics. It combines a high degree
of automation with an elaborate interactive proof engineering
environment.
Deduction is based on a sequent calculus with explicit proof trees that can be graphically visualized (see left), saved and edited. Beginners, who want to learn sequent calculus can switch to using its very basic rules. For doing larger case studies, the basic rules are too low-level (they would lead to proof trees with thousands of steps). Therefore KIV uses proof tactics like simplification of higher-order logic formulas, lemma application, induction and the symbolic execution of programs. These collapse many basic steps into a single step. To automate proofs, KIV offers a number of heuristics. Among others, heuristics for induction, unfolding of procedure calls and quantifier instantiation are provided. Heuristics can be chosen freely, and changed any time during the proof. Additionally, a `problem specific' heuristic exists which is easily adaptable to specific applications. Usually, the heuristics manage to find 80 - 100 % of the required proof steps automatically. The conditional rewriter in KIV (called simplifier) handles thousands of rules very efficiently by compiling them to executable functional programs. Rules may be higher-order, conditions of rules may be checked either by recursive simplifier calls or by checking occurrence in the current goal. Some extensions of standard rewrite rules are rewriting modolo AC (associativity and/or commutativity), elimination rules and forward reasoning. As the structure of a formula helps to understand its meaning, the KIV simplifier always preserves this structure. The user explicitly chooses the rewrite and simplification rules. Different sets of simplification rules can be chosen for different tasks. Verification of partial or total correctness individual programs is supported using a calculus based on Dynamic Logic. The proof strategy is based on symbolic execution of programs, invariants for loops and induction for recursive procedures. Due to the use of Dynamic Logic, the calculus for sequential programs is not limited to the verification of properties of a single program. It is also possible to prove properties involving several programs like program inclusion, which is useful for refinement. For abstract programs the calculus supports total correctness of nondeterministic programs even with infinite nondeterminism (in terms of weakest precondition calculus it can handle all monotonic predicate transformers). The calculus for Java supports full sequential Java(see this paper) including generics (see this paper). The calculus for verifying parallel programs and statecharts is based on a powerful temporal logic, which extends CTL* and ITL. Like ITL, the logic has finite (termination!) and infinite traces, and embeds programs directly as formulas. No encoding into transition systems as e.g. in TLA is necessary. This allows to keep the intuitive principle of symbolic execution from sequential programs, thus allowing for a high degree of automation. Since the interleaving operator has a compositional semantics, modular reasoning over individual threads is supported. In particular, various forms of rely-guarantee rules (with or without deadlocking and termination) are derivable (see this paper and this paper for more details on the logic). An important application of parallel programs we a currently looking into is the verification of lock-free algorithms for multi-core processors, see the VeriCAS project for details. |
Proof Engineering
In KIV, formal specifications of software and system designs are represented explicitly as directed acyclic graphs called development graphs. Each node corresponds to a specification component or an ASM. Each node has a theorem base attached. Theorem bases initially contain axioms, ASM rules, parallel programs, state charts and automatically generated proof obligations for refinements. The theorem base also stores theorems added by the user (proved and yet unproved ones), and manages proofs and their dependencies.
Frequently, the problem in engineering high assurance systems is not to verify proof obligations affirmatively, but rather to interpret failed proof attempts that may indicate errors in specifications, programs, lemmas etc. Therefore, KIV offers a number of proof engineering facilities to support the iterative process of (failed) proof attempts, error detection, error correction and re-proof. Dead ends in proof trees can be cut off, proof decisions may be withdrawn both chronologically and non-chronologically. Unprovable subgoals can be detected by automatically generating counter examples. This counter example can be traced backwards through the proof to the earliest point of failure. Thereby 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. After a correction the goal must be re-proved. Here another interesting feature of KIV, the strategy for proof reuse, can be used. Both successful and failed proof attempts are reused automatically to guide the verification after corrections. This goes far beyond proof replay or proof scripts. We found that typically 90% of a failed proof attempt can be recycled for the verification after correction.
The correctness management in KIV ensures that changes to or deletions of specifications, modules, and theorems do not lead to inconsistencies, and that the user can do proofs in any order (not only bottom up). It guarantees that only the minimal number of proofs are invalidated after modifications, that there are no cycles in the proof hierarchy and that finally all used lemmas and proof obligations are proved (in some sub-specification).
Refinement
One of the strengths of KIV is verification of developments starting with an abstract designs down to executable code using refinement. KIV offers several variants of refinement, depending on the type of system specified. Traditionally, for functional specifications, KIV has supported algebraic refinement in the form of modules for a long time (see this paper).
Newer case studies use various forms of state-based refinement, most prominently ASM refinement (see this paper, this paper and the corresponding KIV project). ASM refinement comes with a modularization theorem that decomposes the correctness proofs for a refinement into proofs showing the commutativity of diagrams consisting of m abstract and n concrete steps. Such m:n diagrams generalize the usual 1:1 diagrams used in forward and backward simulations of data refinement. Case studies include the verification of a Prolog compiler and the Mondex case study on the security of an electronic purse implemented on Smartcards.
KIV also supports standard data refinement (the specifications are explained here as part of the solution to the original Mondex challenge) and IO automata refinement (given here for comparison with ASM refinement). A form of data refinement allows to refine abstract programs to Java code (see this paper) was also used in the Mondex case study.
A current project that uses ASM refinement is the Flashix project on the development of a fully verified Flash file system.
Graphical User Interface
KIV offers a powerful graphical user interface (see this paper) which has been constantly improved over the years. The intuitive user interface allows easy access to KIV for first time users, and is an important prerequisite for managing large applications. The interface is object oriented, and is implemented in Java to guarantee platform independency. The top-level object of a development, the development graph, is displayed (an example is left) using uDraw, a graph visualization tool which automatically arranges large graphs conveniently. The theorem base, which is attached to each development node, is arranged in tables, and context sensitive popup menus are provided for manipulation. While proving a theorem, the user is able to restrict the set of applicable tactics by selecting a context, i.e. a formula or term in the goal, with the mouse. This is extremely helpful for applying rewrite rules, as the set of hundreds of rewrite rules is reduced to a small number of applicable rules for the selected context. Proofs are presented as trees, where the user can click on nodes to inspect single proof steps. In large applications, the plentitude of information may be confusing. Therefore, important information is summarized, and more details are displayed on request. Different colors are used to classify the given information. A special font allows the use of a large number of mathematical symbols. KIV automatically produces LaTeX as well as XML documentation for a development on different levels of detail (see the KIV projects page for various examples of the latter). Specifications, implementations, theorem bases, proof protocols, and various kinds of statistics are pretty printed. The user is encouraged to add comments to specifications, which are also used to automatically produce a data dictionary. As several users may work simultaneously on a large project, the documentation facilities of KIV are very important. The automatically extracted information can also be included into reports. |