Formal Verification of Peripheral Memory Isolation
Time: Wed 2023-06-14 15.00
Location: D3 Lindstedtsvägen 9
Video link: https://kth-se.zoom.us/j/69872122832
Subject area: Computer Science
Doctoral student: Jonas Haglund , Teoretisk datalogi, TCS
Opponent: Professor Gligor Virgil, Carnegie Mellon University
Supervisor: Roberto Guanciale, Teoretisk datalogi, TCS; Mads Dam, Teoretisk datalogi, TCS
In many contexts, computers run both critical and untrusted software,necessitating the need for isolating critical software from untrusted software.These computers contain CPUs, memory and peripherals. For performance reasons,some of these peripherals have a direct memory access (DMA) controller (DMAC),allowing them to access memory without involving the CPU.
This thesis is a study of memory isolation of peripherals. That is, howperipherals are configured such that they can access only restricted memoryregions. If DMACs are not configured appropriately, they may be able to read andleak sensitive data, or modify and corrupt sensitive data and critical programcode, with potentially disastrous consequences. Since DMACs are configured by anassociated DMAC driver software, the DMAC driver is a critical point for security.Testing drivers for isolation is infeasible, due to the necessity of exhaustivetesting to detect violating writes and differential testing to detect violatingreads. Therefore, we use formal methods and interactive theorem proving (ITP), todevelop formal conditions that, if satisfied by a driver, ensure that theassociated DMAC is memory isolated.
We present a detailed case study of formally verifying memory isolation of anEthernet DMAC in the ITP HOL4. We also generalize this case study in the form ofa verification tool in HOL4, reducing the complexity and time needed to formallyverify the conditions under which a DMAC is isolated. The tool includes ageneral DMAC model, reflecting the common features of DMACs. By means ofrefinement, we verified the conditions under which this general DMAC isisolated. By instantiating this general DMAC model with the specifics of a givenDMAC, and by proving the associated proof obligations, the user obtains theformal conditions for DMAC memory isolation.
In addition, we have implemented and analyzed a run-time monitor that checksthat Ethernet DMAC configurations respect memory isolation. This monitor is usedin a CCTV system, part of an isolation verified hypervisor, on top of whichLinux and a CCTV guest runs. This system gives Linux Internet access, butwithout being able to to obtain unencrypted photos taken by the CCTV guest: Thehypervisor configures the CPU such that Linux and the CCTV guest are isolated,except for a communication channel used to transfer encrypted photos; and themonitor applies only DMAC configurations, defined by Linux, that cannot causethe DMAC to access non-Linux memory.