Published:
PhD thesis about formal verification (by means of interactive theorem proving) of memory isolation of I/O devices, that can be used to formally verify that device drivers configure their associated devices to access only certain memory regions.
Download here
Published in Formal Methods in Computer-Aided Design, 2022
This paper describes a generic formal model in HOL of the common characteristics of DMA controllers. This generic model can be instantiated to describe the operational behavior of a specific DMA controller. It is formally verified under which conditions such DMA controllers are isolated.
Download here
Published in Journal of Banking and Financial Technology, 2020
This paper presents a monitor in a hypervisor with the purpose of making sure that a Linux guest cannot configure the NIC (described in Trustworthy Isolation of DMA Devices) to break isolation (i.e. access memory regions allocated to the hypervisor or any other guest). It is also motivated in detail why the monitor ensures this isolation.
Download here
Published in Information Systems Security: 15th International Conference, ICISS 2019, 2019
A case study of how one can formally verify sufficient conditions that a device driver of the network interface controller (NIC) can satisfy to ensure that the NIC can access only certain memory regions.
Download here
Published:
Master’s thesis describing a model of a direct memory access controller (DMAC) of a network interface controller (NIC), the implementation of a monitor in a hypervisor to prevent Linux from configuring the DMAC to break isolation and inject untrusted code, and a description of how it can be formally verified that in this system Linux can execute trusted code only. The thesis is based on previous work that has formally verified that Linux executes only trusted code where there is no NIC and DMAC.
Download here