Biblio

Commodity I/O hardware often fails to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity systems sometimes trade off separation assurance for increased performance. Remarkably, device firmware need not be malicious. Instead, any malicious driver, even if isolated in its own execution domain, can manipulate its device to breach I/O separation. To prevent such vulnerabilities with high assurance, a formal I/O separation model and its use in automatic generation of secure I/O kernel code is necessary.This paper presents a formal I/O separation model, which defines a separation policy based on authorization of I/O transfers and is hardware agnostic. The model, its refinement, and instantiation in the Wimpy kernel design, are formally specified and verified in Dafny. We then specify the kernel implementation and automatically generate verified-correct assembly code that enforces the I/O separation policies. Our formal modeling enables the discovery of heretofore unknown design and implementation vulnerabilities of the original Wimpy kernel. Finally, we outline how the model can be applied to other I/O kernels and conclude with the key lessons learned.

For systems composed of many rapidly-deployed microservices that cross networks and span trust domains, strong authentication between microservices is a prerequisite for overall system trustworthiness. We examine standard authentication mechanisms in this context, and we introduce new comprehensive, automated, and fine-grained mutual authentication mechanisms that rely on attestation, with particular attention to provisioning and managing secrets. Prototype implementations and benchmark results indicate that mutual attestation introduces only modest overheads and can be made to meet or exceed the performance of common but weaker authentication mechanisms in many scenarios.