18 citations · 31 across the 4 of their papers we have counts for
5 papers
Secure Memory Management on Modern Hardware
Reto Achermann, Nora Hossle, Lukas Humbel +3
Almost all modern hardware, from phone SoCs to high-end servers with accelerators, contain memory translation and protection hardware like IOMMUs, firewalls, and lookup tables whic…
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer
Roni Haecki, Lukas Humbel, Reto Achermann +3
We present CleanQ, a high-performance operating-system interface for descriptor-based data transfer with rigorous formal semantics, based on a simple, formally-verified notion of o…
A Least-Privilege Memory Protection Model for Modern Hardware
Reto Achermann, Nora Hossle, Lukas Humbel +3
We present a new least-privilege-based model of addressing on which to base memory management functionality in an OS for modern computers like phones or server-based accelerators.…
Formalizing Memory Accesses and Interrupts
Reto Achermann, Lukas Humbel, David Cock +1
The hardware/software boundary in modern heterogeneous multicore computers is increasingly complex, and diverse across different platforms. A single memory access by a core or DMA…
Verifying Probabilistic Correctness in Isabelle with pGCL
David Cock
This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facili…