Portfolio item number 1
Short description of portfolio item number 1
Posts by Collection
portfolio
Portfolio item number 2
Short description of portfolio item number 2
publications
Formal Verification of Systems Software: No Execution of Malicious Software in Linux in Networked Embedded Systems
Published:
Master’s thesis describing a model of a direct memory access controller (DMAC) of a network interface controller (NIC), the implementation of a monitor in a hypervisor to prevent Linux from configuring the DMAC to break isolation and inject untrusted code, and a description of how it can be formally verified that in this system Linux can execute trusted code only. The thesis is based on previous work that has formally verified that Linux executes only trusted code where there is no NIC and DMAC.
Download here
Trustworthy Isolation of DMA Enabled Devices
Published in Information Systems Security: 15th International Conference, ICISS 2019, 2019
A case study of how one can formally verify sufficient conditions that a device driver of the network interface controller (NIC) can satisfy to ensure that the NIC can access only certain memory regions.
Download here
Trustworthy Isolation of DMA Devices
Published in Journal of Banking and Financial Technology, 2020
This paper presents a monitor in a hypervisor with the purpose of making sure that a Linux guest cannot configure the NIC (described in Trustworthy Isolation of DMA Devices) to break isolation (i.e. access memory regions allocated to the hypervisor or any other guest). It is also motivated in detail why the monitor ensures this isolation.
Download here
Formally Verified Isolation of DMA
Published in Formal Methods in Computer-Aided Design, 2022
This paper describes a generic formal model in HOL of the common characteristics of DMA controllers. This generic model can be instantiated to describe the operational behavior of a specific DMA controller. It is formally verified under which conditions such DMA controllers are isolated.
Download here
Formal Verification of Peripheral Memory Isolation
Published:
PhD thesis about formal verification (by means of interactive theorem proving) of memory isolation of I/O devices, that can be used to formally verify that device drivers configure their associated devices to access only certain memory regions.
Download here
talks
Talk 1 on Relevant Topic in Your Field
Published:
This is a description of your talk, which is a markdown files that can be all markdown-ified like any other post. Yay markdown!
Conference Proceeding talk 3 on Relevant Topic in Your Field
Published:
This is a description of your conference proceedings talk, note the different field in type. You can put anything in this field.
teaching
Teaching experience 1
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Teaching experience 2
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.