(* = offsite link)
VFiasco is a large project with many facets and subprojects. On this
page, we list and describe our current activities.
If you would like to help with any of these projects, please
On this page, you will find descriptions of these subprojects:
- Hardware model
- We specify hardware interfaces and operations that are
relevant for our verification. This includes a physical
memory with read and write operations, virtual memory with
page tables on top of physical memory, and a TLB-reload handler.
We will prove that our hardware model fulfills some basic
guarantees, but will not verify the model against a formal
hardware specification (such as the VHDL description of an x86
CPU); this would be a major project of its own. Instead, in
our verification we will assume the correctness of this model.
More information: technical
- Model of type-safe object store
- Based on the hardware model, we model a C++
execution environment with type safety. Based on certain
assumptions, this environment guarantees object-store
properties such as ``typed objects do not change value unless
We call the assumptions necessary to provide these
properties ``system guarantees,'' and a major part of the
VFiasco project will be to prove that the Fiasco microkernel
actually provides these guarantees at all times.
- Programming language Safe C++
- Safe C++ is a dialect of C++ that we use as Fiasco's
implementation language. Safe C++ is downward-compatible with
C++, which means that a C++ compiler (with an extra library)
can compile Safe-C++ programs.
The Safe-C++ dialect changes C++ as follows:
- Safe-C++ semantics in
We will model the semantics of Safe C++ and certain knowledge
about the Safe C++ compiler on top of the hardware model and the type-safe object store. These models
include semantics of most C++ constructs (including pointers,
loops, multiple return statements, setjmp/longjmp, and even
gotos), models for C++'s built-in data types, and C++'s stack
We will use these models as base assumptions in our
verification. We will not try to prove that our C++ compiler
implements them correctly, but where we use compiler-specific
features, we will increase confidence in our models using
- Semantics compiler
- The ``semantics compiler'' is the tool that compiles Fiasco's C++
source code into its semantics in higher-order logics (HOL)
that can be loaded and reasoned about in a theorem prover. The
target language of this compiler mainly consists of interfaces
provided by our type-safe object
store and the C++ semantics model.
Currently, there exists a prototype of this compiler written
More information: technical
report, or contact us.
- Proof procedures
- The output generated by our semantics compiler is highly regular.
Under the assumption that the object-store properties initially
hold, models of simple sequential code should simplify to very
simple statements. The goal of this project is to develop
scripts for our theorem prover that automate this task.
(In theorem-prover speak, such scripts are known as tacticals.)
More information: please contact us.
- Module specifications
- What should we prove in the VFiasco project? (See also the corresponding FAQ entry.)
Verifying a large software system like Fiasco can only be
carried out in many small steps. In each step, we intend to
verify one module or class of Fiasco's source code. Of course,
before doing so, we must first formally specify the purpose of
the module or class in question.
More information: list
of student projects, or contact us.
Last modified: Fri Jul 18 19:18:24 2003