Tech Xplore: Researchers reveal a new computing platform that is provably secure even alongside software compromised I/O devices

[Karl]

https://doi.ieeecomputersociety.org/10.1109/SP40001.2021.00101

Abstract
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/html
Size: 2332 bytes
Desc: not available
URL: <https://lists.cpunks.org/pipermail/cypherpunks/attachments/20210617/2f9e0909/attachment.txt>