Fraunhofer AISECWhile most microkernel-based systems implement non-essential software components as user space tasks and strictly separate those tasks during runtime, they often rely on a static configuration and composition of their software components to ensure safety and security.
In our research, we extend a microkernel-based system architecture with a TPM and propose a verification mechanism for a microkernel runtime environment, which calculates integrity measurements before allowing to load (remote) binaries.
As a result, our approach is the first to adopt the main ideas of the Integrity Measurement Architecture (IMA), which has been proposed for Linux-based systems, to a microkernel. In comparison, however, it significantly reduces the Trusted Computing Base (TCB) and allows for a strict separation of the integrity verification component from any rich operating system, such as GNU/Linux or Android, running in parallel.
In our implementation, which is based on L4/Fiasco.OC with L4Re as runtime environment, we present our extension of the existing L4Re loader service that calculates integrity measurements for each binary. We also evaluate our implementation on two ARM-based developer boards and discuss code size, security, and performance of our proposed integrity verification mechanism.
Further information
