International Association
for Cryptologic Research

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.