High Assurance Computing on Open Hardware Architectures
Yuqun Chen, PAUL J. ENGLAND, Marcus Peinado, Bryan Willman · 2003
We investigate the problem of supporting a high-assurance operating system on open hardware architectures, which support a large and diverse collection of peripheral devices. The paper focuses on the problems that arise in this context for the management of DMA devices and memory. Our solution combines aspects of virtual machine monitors (VMM) and Exokernels with new software and hardware techniques. In particular, we remove drivers for DMA devices from the base layer without compromising safety. Furthermore, we describe an algorithm that allows guest operating systems to operate directly on the address translation hardware without compromising safety. Beyond our initial goals, we believe that these techniques can be of more general interest in the construction of VMMs and Exokernels. The paper presents a limited prototype implementation for x86 processors and performance measurements. The techniques presented in this paper are being implemented for wide deployment in future versions of x86-class processors and Microsoft’s Next Generation Secure Computing Base (NGSCB).