Jonas Haglund

Jonas Haglund

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Future Blog Post

less than 1 minute read

Published:

This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.

Blog Post number 4

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 3

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 2

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 1

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

portfolio

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

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.