Sökning: "HOL4"

Visar resultat 1 - 5 av 11 avhandlingar innehållade ordet HOL4.

1. 1. Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software

   Författare :Ning Dong; Roberto Guanciale; Mads Dam; Magnus Myreen; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formal Verification; Information Flow; Refinement; Interactive Theorem Prover; HOL4; Serial Interface; Pipelined Processor; Microarchitecture; Out-of-order Execution; Formell Verifiering; Informationsflöde; Förfining; Interaktiva Bevisprogrammet; HOL4; Seriellt Gränssnitt; Pipelined Processor; Mikroarkitektur; Omordnad Exekvering; Datalogi; Computer Science;

   Sammanfattning : Computer systems, consisting of hardware and software, have gained significant importance in the digitalised world. These computer systems rely on critical components to provide core functionalities and handle sensitive data. LÄS MER

3. 2. Proving Safety and Security of Binary Programs

   Författare :Andreas Lindner; Roberto Guanciale; Mads Dam; Tamara Rezk; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Binary Code; Binary Analysis; Formal Verification; Model-Based Testing; Theorem Proving; HOL4; Intermediate Language; Instruction Set Architectures; ISA; Observational Models; Symbolic Execution; Weakest-Precondition; Execution Time Analysis; binärkod; binärkodsanalys; formell verifiering; modellbaserad testning; satsbevisning; HOL4; mellankod; instruktionsuppsättningar; ISA; observationsmodeller; symbolisk exekvering; minst restriktiva villkoret; analys av övre tidsgräns; Datalogi; Computer Science;

   Sammanfattning : With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. LÄS MER

4. 3. Secure System Virtualization : End-to-End Verification of Memory Isolation

   Författare :Hamed Nemati; Mads Dam; Gustavo Betarte; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; Cache attack; Security Monitor; Information Flow; Computer Science; Datalogi;

   Sammanfattning : Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. LÄS MER

5. 4. No Hypervisor Is an Island : System-wide Isolation Guarantees for Low Level Code

   Författare :Oliver Schwarz; Mads Dam; Christian Gehrmann; Gerwin Klein; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; DMA; Peripheral Devices; Instruction Set Architectures; ISA; Information Flow; Boot; Computer Science; Datalogi;

   Sammanfattning : The times when malware was mostly written by curious teenagers are long gone. Nowadays, threats come from criminals, competitors, and government agencies. Some of them are very skilled and very targeted in their attacks. LÄS MER

7. 5. Building Verified Hardware and Verified Stacks in HOL

   Författare :Andreas Lööw; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : This thesis explores building provably correct software and hardware inside the HOL4 interactive theorem prover. Interactive theorem provers such as HOL4 are proof environments where manual (human) and automated (machine) proofs can be composed in logically safe ways, and all proof steps (be it manual or automated) are mechanically checked. LÄS MER