Cryptology ePrint Archive: Report 2014/984
Undermining Isolation through Covert Channels in the Fiasco.OC Microkernel
Michael Peter and Jan Nordholz and Matthias Petschick and Janis Danisevskis and Julian Vetter and Jean-Pierre Seifert
Abstract: In the new age of cyberwars, system designers have
come to recognize the merits of building critical systems on top
of small kernels for their ability to provide strong isolation at
system level. This is due to the fact that enforceable isolation is
the prerequisite for any reasonable security policy. Towards this
goal we examine some internals of Fiasco.OC, a microkernel of
the prominent L4 family. Despite its recent success in certain highsecurity
projects for governmental use, we prove that Fiasco.OC
is not suited to ensure strict isolation between components meant
to be separated.
Unfortunately, in addition to the construction of system-wide
denial of service attacks, our identified weaknesses of Fiasco.OC
also allow covert channels across security perimeters with high
bandwidth. We verified our results in a strong affirmative way
through many practical experiments. Indeed, for all potential use
cases of Fiasco.OC we implemented a full-fledged system on its
respective archetypical hardware: Desktop server/workstation on
AMD64 x86 CPU, Tablet on Intel Atom CPU, Smartphone on
ARM Cortex A9 CPU. The measured peak channel capacities
ranging from 13500 bits/s (Cortex-A9 device) to 30500 bits/s
(desktop system) lay bare the feeble meaningfulness of Fiasco.
OC’s isolation guarantee. This proves that Fiasco.OC cannot
be used as a separation kernel within high-security areas.
Category / Keywords: implementation / Critical systems, Separation, Microkernel, Covert Channel
Date: received 3 Dec 2014, last revised 10 Dec 2014
Contact author: Jean-Pierre Seifert at telekom de
Available format(s): PDF | BibTeX Citation
Note: Minor editing.
Version: 20141210:210206 (All versions of this report)
Short URL: ia.cr/2014/984
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]