VFiasco subprojects

If you would like to help with any of these projects, please contact us.

On this page, you will find descriptions of these subprojects:

• Hardware model
• Model of type-safe object store
• Programming language Safe C++
• Safe-C++ semantics in higher-order logics
• Semantics compiler
• Proof procedures
• Module specifications

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 report.

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 updated explicitly.''

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.

More information:

• technical report
• FAQ: What is the real-world counterpart of the object-store layer?

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:

• In: We have added certain language features that are needed in operating-system kernel construction, such as installing a new virtual-memory page table. We implement these features as a separate C++ library.

• Fix: We fixed the semantics of certain language constructs that the C++ standard leaves as undefined or implementation-defined, such as the size of built-in data types and evaluation order of function-call arguments.

  We use static tests to verify that our C++ compiler actually implements our fixed semantics.

• Out: We have removed from C++ all constructs that are not used in Fiasco and for which we do not specify formal semantics. This includes features such as floating-point arithmetics and exceptions. We may re-add these features in a future version of Safe C++.

  We enforce these restrictions by emitting diagnostics from our semantics compiler.

More information:

• Matthias Daum's term paper (unfortunately only in German)
• FAQ: Don't you also have to verify the the C++ compiler with which you compile Fiasco?
• or contact us.

Safe-C++ semantics in higher-order logics

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 allocator.

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 tests.

More information:

• technical report
• FAQ: Do you need a programming language with completely defined semantics?
• FAQ: Do you assume a virtual machine that runs Safe-C++ programs?
• or contact us.

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 in C++.

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.