Welcome to the VFiasco project!

Newsflash

10 Jul 2005

New Paper The VFiasco approach for a verified operating system, accepted at the 2nd ECOOP Workshop on Programm Languages and Operating Systems (ECOOP-PLOS'05)

22 Oct 2004

New Paper Verifying Duff's device: A simple compositional denotational semantics for Goto and computed jumps

4 Aug 2004

Duff's device verified.

Find more news in the What's new section.

Overview

What is the VFiasco project?

VFiasco stands for ``Verified Fiasco.'' The VFiasco project has two primary goals:

1. to further develop coalgebraic specification techniques such that these techniques can be applied to real software
2. to mechanically verify some security relevant properties of a complete µ-kernel (microkernel) operating system running on x86 PCs

Motivation

For most computer applications absence of errors is desirable, but not strictly necessary. However, there exist application domains where even a single malfunction cannot be tolerated. In the future cryptographic applications will run on general purpose PC's to sign documents, safely transfer money and so on. The correctness of these applications in an environment where possibly malicious attackers are present will be an requirement or at least a strong selling point.

An application can only provide guarantees about its correctness if it can rely on assurances of similar strength of the underlying operating system. For instance for the validity of an electronic signature the operating system must make sure that during every run of the signing program nobody can access the main memory to spy out the secret key that is used for signing. Nowadays the correctness of operating systems is ensured via careful design and sophisticated testing. However, tests can only reveal errors. The absence of errors can only be proved through the use of formal methods, that is through the investigation of the program and its semantics with mathematical means.

Who is involved?

The VFiasco project is a cooperation of the chair for Algebraic and Logical Foundations of Computer Science (which contributes coalgebraic specification techniques) and the operating systems group (which contributes the Fiasco µ-kernel) at the department of computer science at Dresden University.

Basis of the project

There are two recent developents in computer science.

1. Powerful tools for theorem proving (like Isabelle and PVS) and new approaches to software verification (namely the use of coalgebras) make it possible to analyze software of considerable size.
2. µ-kernels of the second generation make it possible to structure operating systems into several parts with smaller interfaces. These interfaces can be enforced through the separation of address spaces.

The work in the LOOP project proved that coalgebraic specification can well applied to real software and further that coalgebric specification techniques work well together with modern interactive theorem provers.

Bringing these two developments together promises a breakthrough in operating system verification.

Preliminary work

In preparing the project a case study has been carried out. In the case study the interface of one class of the Fiasco µ-kernel has been specified in the coalgebraic class specification language CCSL. With the theorem prover PVS it was checked if the source code of Fiasco fulfills the specification. The whole case study is descibed in detail here.

More Information

about the project, the (preliminary) schedule, related work, and so on can be found in the technical report VFiasco - Towards a Provably Correct Microkernel and in the DFG Application (in German only).

What's new

10 Jul 2005

New Paper The VFiasco approach for a verified operating system, accepted at the 2nd ECOOP Workshop on Programm Languages and Operating Systems (ECOOP-PLOS'05)

22 Oct 2004

New Paper Verifying Duff's device: A simple compositional denotational semantics for Goto and computed jumps

4 Aug 2004

Duff's device verified.

3 Jul 2003

New Paper The Semantics of C++ Types: Towards Verifying low-level System Components, accepted for the emerging trends track on TPHOLs

2 Aug 2002

Students! Next semester, Hendrik Tews teaches a lecture titled ``Program verification and specification with coalgebras.'' This course presents most of the foundation work used in the VFiasco project. If you are interested in working with (``Großer Beleg,'' master's thesis, or student job), be sure to attend this course.

6 Jun 2002

Added a description of VFiasco's subprojects to this website.

15 Apr 2002

Added a related work section to this website.

5 Apr 2002

Released a new technical report: Applying source-code verification to a microkernel - The VFiasco project.

5 Nov 2001

The VFiasco project starts!

29 Jun 2001

A Work-in-progress talk at the USENIX Annual Technical Conference 2001 about the VFiasco project was well received by the audience.

23 Jan 2001

Hendrik Tews and colleagues have written an introduction to the VFiasco project, which aims at a formally verified and high-level security-certified microkernel: VFiasco - Towards a Provably Correct Microkernel.

If you are a student at TU Dresden, you might be interested in our asssignment and project list for VFiasco.

Jan 2001

The VFiasco project receives funding from the Deutsche Forschungsgemeinschaft.

20 Mar 2000

Hendrik Tews carried out a case study that applies coalgebraic specification and verification techniques to Fiasco. A part of the memory management of Fiasco was specified in the Coalgebraic Class Specification Language CCSL. With the support of a modern theorem prover (namely PVS) it was possible to check the source code of Fiasco against this specification. It turns out that, on the basis of coalgebras and with the use of state of the art tools like PVS and CCSL, it becomes feasible to verify practically used operation-system software.