Till innehåll på sidan
Till KTH:s startsida

Formal Verification of Peripheral Memory Isolation

Tid: On 2023-06-14 kl 15.00

Plats: D3 Lindstedtsvägen 9

Videolänk: https://kth-se.zoom.us/j/69872122832

Språk: Engelska

Ämnesområde: Datalogi

Respondent: Jonas Haglund , Teoretisk datalogi, TCS

Opponent: Professor Gligor Virgil, Carnegie Mellon University

Handledare: Roberto Guanciale, Teoretisk datalogi, TCS; Mads Dam, Teoretisk datalogi, TCS

Exportera till kalender

QC 20230523

Abstract

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.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-327312