Open Robust Infrastructures (ROBIN)
ROBIN is a project in the 2005 EC call on Preparatory Action for
Security Research. Our mission is to research and develop an
operating-system infrastructure capable of protecting against the
threats our information and communication infrastructure is currently
The objective of this Preparatory Action is to explore key
technologies for a small, robust platform that can host legacy
operating systems and their applications, but that is small enough to
undergo formal analysis and construction techniques. Preliminary
studies have shown that in the order of a hundred thousand lines of
code can be sufficient. The platform is comprised of the Nova
microhypervisor and the Bastei secure operating-system layer. It will
allow applications to be split into security-sensitive and other
parts. It will also allow applications to fall-back into an emergency
mode. This platform will be open and originate from Europe which will
establish an alternative to proprietary US solutions that we expect to
The project has been accepted under the Grant Agreement no.
SEC5-PR-104600. The project started February 2006 and ended April 2008.
- Hendrik Tews, Marcus Völp, Tjark Weber A Formal Model of Memory Peculiarities for the
Verification of Low-Level Operating-System Code in proceedings of the International Workshop on Systems
Software Verification (SSV08), Sydney. Also in ENTCS Volume 217.
- Hendrik Tews Formal Methods in the Robin project: Specification and verification
of the Nova microhypervisor in proceedings of the C/C++ Verification workshop 2007.
- Hendrik Tews Microhypervisor verfication: possible approaches and relevant properties in proceedings of the NLUUG Voorjaarsconferentie 2007.
- Hendrik Tews Olmar: manipulating C and C++ abstract syntax trees in OCaml in proceedings of the C/C++ Verification workshop 2007.
- Marcus Völp Statically Checking Confidentiality of Shared-Memory Programs with Dynamic Labels in Third International Conference on Availability, Security and Reliability (ARES 2008) Barcelona, Spain.
- Marcus Völp, Claude-Joachim Hamann, Hermann Härtig Avoiding Timing Channels in Fixed-Priority Schedules in ACM Symposium on Information, Computer and Communication Security (ASIACCS 2008), Tokyo, Japan.
- Norman Feske, Christian Helmuth Design of the Bastei OS Architecture TU-Dresden technical report TUD-FI06-07, Dresden, Germany 2006.
Publishable Project Deliverables
The Bastei TCB Construction Kit
The Nova Microhypervisor
The sources of the Nova microhypervisor and corresponding
documentation will be published in December 2008.
Formal Specification and Verification of the Nova Microhypervisor
Further information is available on the respective web pages of the
In this project have joint forces the
To contact the members of this consortium please send email to: