Search for dissertations about: "HOL4"

Found 3 swedish dissertations containing the word HOL4.

  1. 1. Secure System Virtualization End-to-End Verification of Memory Isolation

    University dissertation from Stockholm : KTH Royal Institute of Technology

    Author : Hamed Nemati; KTH.; [2017]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; Cache attack; Security Monitor; Information Flow; Computer Science; Datalogi;

    Abstract : 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. READ MORE

  2. 2. No Hypervisor Is an Island System-wide Isolation Guarantees for Low Level Code

    University dissertation from Stockholm : KTH Royal Institute of Technology

    Author : Oliver Schwarz; KTH.; [2016]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; DMA; Peripheral Devices; Instruction Set Architectures; ISA; Information Flow; Boot; Datalogi; Computer Science;

    Abstract : 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. READ MORE

  3. 3. Building Verified Hardware and Verified Stacks in HOL

    University dissertation from ; Chalmers tekniska högskola; Gothenburg

    Author : Andreas Lööw; [2019]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES;

    Abstract : 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. READ MORE