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.

Många datorer exekverar både kritisk och opålitlig mjukvara. Detta gör det nödvändig att isolera dessa typer av mjukvara från varandra. Dessa datorer innehåller CPUer, minne och periferienheter. För att maximera prestanda så innehåller vissa periferienheter en minnesstyrkrets för direkt minnesåtkomst som gör att periferienheterna kan läsa och skriva minnet utan inblandning av CPUn.

Denna uppsats presenterar en studie av hur periferienheter kan konfigureras så att de är isolerade till vissa minnesregioner. Om minnesstyrkretsen inte är konfigurerad på rätt sätt så kan den möjligtvis läsa och läcka känslig data, eller skriva och förstöra känslig data och kritisk programkod, med förödande konsekvenser. En minnesstyrkrets konfigureras av en tillhörande drivrutin. För att begränsa styrkretsen till vissa minnesregioner så måste därför drivrutinen konfigurera styrkretsen på en motsvarande sätt. Detta gör att drivrutiner för minnesstyrkretsar har en kritisk roll i datorsäkerhet. Testning av drivrutiner för isolering är omöjligt på grund av det stora antalet nödvändiga testfall för att utesluta oönskade minnesåtkomster. Därför använder vi formella metoder och ett interaktivt bevisverktyg för att identifiera formella villkor som garanterar, om satisfierade av drivrutinen, att styrkretsen är minnesisolerad.

Vi presenterar en detaljerad formell verifiering i bevisverktyget HOL4 av att en minnesstyrkrets i en Ethernet-adapter är minnesisolerad. Vi generaliserar denna studie i form av ett verifieringsverktyg i HOL4, som reducerar arbetsbördan för att verifiera minnesisolering av minnesstyrkretsar. Verktyget inkluderar en generell model som beskriver de gemensamma operationerna som minnesstyrkretsar utför. Vi har utgått från en abstrakt och generell styrkretsmodell, och steg för steg lagt till mer detaljerade styrkretsoperationer och verifierat att den resulterande modellen respekterar minnesisolering, och slutligen erhållit verifiering av en konkret generell modell som beskriver riktiga minnesstyrkretsar. Genom att instantiera den generella styrkretsmodellen med specifika styrkretsoperationer, och bevisa vissa tillhörande förpliktelser, så erhåller användaren de formella isoleringsvillkoren.

Vi har också implementerat och analyserat en körtidsmonitor. Denna monitor kontrollerar att konfigurationer av en minnesstyrkrets i en Ethernet-adapter bevaras i ett minnesisolerat tillstånd. Denna monitor används i ett CCTV-system, som del av en hypervisor, som Linux och en CCTV-gäst exekveras ovanpå. I detta system har Linux internetåtkomst, men utan möjlighet att kunna erhålla okrypterade foton tagna av CCTV-gästen. Hypervisorn konfigurerar CPUn sådant att Linux och CCTV-gästen är isolerade, bortsett från en kommunikationskanal som används för att överföra krypterade foton mellan CCTV-gästen och Linux. Monitorn verkställer enbart styrkretskonfigurationer, konstruerade av Linux, som inte kan få styrkretsen att läsa eller skriva minne som inte tillhör Linux.