[1]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.

References

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