Formal Verification of Peripheral Memory Isolation

التفاصيل البيبلوغرافية
العنوان:	Formal Verification of Peripheral Memory Isolation
بيانات النشر:	KTH, Teoretisk datalogi, TCS Stockholm 2023
تفاصيل مُضافة:	Haglund, Jonas
نوع الوثيقة:	Electronic Resource
مستخلص:	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 syste Många datorer exekverar både kritisk och opålitlig mjukvara. Detta gör det nödvändig att isolera dessa typer av mjukvara från varandra. Dessa datorer innehåller CPUer, minne och periferienheter. För att maximera prestanda så innehåller vissa periferienheter en minnesstyrkrets för direkt minnesåtkomst som gör att periferienheterna kan läsa och skriva minnet utan inblandning av CPUn. Denna uppsats presenterar en studie av hur periferienheter kan konfigureras så att de är isolerade till vissa minnesregioner. Om minnesstyrkretsen inte är konfigurerad på rätt sätt så kan den möjligtvis läsa och läcka känslig data, eller skriva och förstöra känslig data och kritisk programkod, med förödande konsekvenser. En minnesstyrkrets konfigureras av en tillhörande drivrutin. För att begränsa styrkretsen till vissa minnesregioner så måste därför drivrutinen konfigurera styrkretsen på en motsvarande sätt. Detta gör att drivrutiner för minnesstyrkretsar har en kritisk roll i datorsäkerhet. Testning av drivrutiner för isolering är omöjligt på grund av det stora antalet nödvändiga testfall för att utesluta oönskade minnesåtkomster. Därför använder vi formella metoder och ett interaktivt bevisverktyg för att identifiera formella villkor som garanterar, om satisfierade av drivrutinen, att styrkretsen är minnesisolerad. Vi presenterar en detaljerad formell verifiering i bevisverktyget HOL4 av att en minnesstyrkrets i en Ethernet-adapter är minnesisolerad. Vi generaliserar denna studie i form av ett verifieringsverktyg i HOL4, som reducerar arbetsbördan för att verifiera minnesisolering av minnesstyrkretsar. Verktyget inkluderar en generell model som beskriver de gemensamma operationerna som minnesstyrkretsar utför. Vi har utgått från en abstrakt och generell styrkretsmodell, och steg för steg lagt till mer detaljerade styrkretsoperationer och verifierat att den resulterande modellen respekterar minnesisolering, och slutligen erhållit verifiering av en konkret generell modell som beskriver r QC 20230523
مصطلحات الفهرس:	formal verification, interactive theorem proving, direct memory access, memory isolation, input/output, formell verifiering, interaktiv datorassisterad beviskonstruktion, direkt minnesåtkomst, minnesisolering, indata/utdata, Computer Systems, Datorsystem, Doctoral thesis, comprehensive summary, info:eu-repo/semantics/doctoralThesis, text
URL:	http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-327312 TRITA-EECS-AVL ; 2013:48
الإتاحة:	Open access content. Open access content info:eu-repo/semantics/openAccess
ملاحظة:	application/pdf English
أرقام أخرى:	UPE oai:DiVA.org:kth-327312 0000-0001-7293-5735 urn:isbn:978-91-8040-604-8 1400070213
المصدر المساهم:	UPPSALA UNIV LIBR From OAIster®, provided by the OCLC Cooperative.
رقم الأكسشن:	edsoai.on1400070213
قاعدة البيانات:	OAIster

الوصف
الوصف غير متاح.