An I/O Separation Model and its Applications to On-Demand I/O on Commodity Platforms

A key goal of security architectures is to separate I/O transfers of security-sensitive applications from untrusted commodity OSes and other applications, with high assurance. These architectures provide I/O kernels that assure the confidentiality and authenticity of the transmitted I/O data owned by a security sensitive application, even when commodity OSes and other applications are compromised. These kernels help eliminate security-sensitive application exposure to drivers they do not need. This is a major security advantage because drivers contribute over half of code size in commodity OS kernels.
However, existing I/O kernels can only enforce I/O separation on limited hardware configurations of
commodity platforms, if they rely on existing I/O hardware mediation components such as IOMMU, or ignore I/O operations that could be misused to break I/O separation. Commodity I/O hardware designs focus primarily on increasing performance and device connectivity, but often fail to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity
systems sometimes trade off isolation assurance for increased performance. Remarkably, to breach I/O
separation, device firmware need not be malicious, though it is allowed to be so. Instead, any malicious driver can manipulate its device to breach I/O separation. To prevent such vulnerabilities in kernel designs with high assurance, a formal I/O separation model is necessary. This dissertation defines an I/O separation model for general commodity platforms and proves its soundness. The model defines a precise separation policy based on complete mediation of I/O transfers despite frequent lack of commodity hardware to support it. Thus it can be applied to the I/O designs
of all commodity platforms, compared to previous kernels that work on limited hardware configurations. Furthermore, this dissertation applies the model to the latest I/O kernels that offer on-demand I/O separation. These kernels allow security-sensitive applications to relinquish and release their devices to and from untrusted commodity OSes on-demand. The dissertation shows how to apply the I/O separation
model to one carefully but informally designed on-demand I/O kernel, the Wimpy Kernel, and illustrates how the model enables the discovery of formerly unknown vulnerabilities. The dissertation also shows how to remove these vulnerabilities and obtain a model-based I/O design – an unavailable feature of commodity systems. In addition, the dissertation presents a novel GPU Separation Kernel to allow isolated applications to share display with untrusted OS and other applications, and informally analyzes it against the same vulnerabilities.