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 facing.
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 appear soon.

The project has been accepted under the Grant Agreement no. SEC5-PR-104600. The project started February 2006 and ended April 2008.

Publications

• 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

• D.8 Final Activity Report
  This final activity report summarizes the results and achievements of the ROBIN project.

The Bastei TCB Construction Kit

• D.4 Specification of the Bastei OS Architecture
  Bastei Reference Manual.
• D.10 A guided walk though Bastei
  This document describes the Bastei architecture and the corresponding demonstrator. It serves as an introductory document for getting started with Bastei.
• Bastei is now commercially supported by the spin-off company Genode Labs as the open source Genode Operating System Framework.

The Nova Microhypervisor

Formal Specification and Verification of the Nova Microhypervisor

• D.12 Formal Nova Interface Specification
  This document describes a formal specification of the interface of the Nova microhypervisor.
• D.13 Nova Microhypervisor Verification
  Our verification approach and the achieved results are documented in this deliverable.
• Appendix to D.13 Nova Microhypervisor Verification
  This appendix contains the PVS sources in textual form. Please do not print this document.
• PVS Sources of the Robin Verification approach
  

Further information is available on the respective web pages of the project partners.

Partners

• Operating Systems Group of the Technische Universität Dresden Germany
• Advanced Systems Technology Group, STMicroelectronics Rousset France
• Security of Systems Group of the Radboud Universiteit Nijmegen the Netherlands
• secunet Security Networks AG, Dresden Germany