Lukas Humbel

dblp:198/0735 · DBLP profile ↗
← Back
6ranked-venue papers
2as first author
3since 2021 · last 2021
0000-0001-8326-7074ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 4 · 2 first-author · 3 since 2021Systems, architecture and hardware · 1Theory of computation · 1
YearPublicationVenuePosition
2021 mmapx: uniform memory protection in a heterogeneous world
abstract
Modern Systems-on-Chip (SoCs) are networks of heterogeneous cores, intelligent devices, and memory, connected through multiple configurable address translation and protection units like IOMMUs and System MMUs.
Reto Achermann, David A. Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
HotOS5
2021 Generating correct initial page tables from formal hardware descriptions
abstract
Modern hardware platforms are increasingly complex and heterogeneous. System software uses a hodgepodge of different mechanisms and representations to express the memory topology of the target platform. Considerable maintenance effort is required to keep them in sync while often sharing is impossible due to hard-coded values. Incorrect platform-specific values in the hardware initialization sequence can lead to security critical and hard-to-find bugs because of misconfigured translation hardware, inaccessible devices, or the use of bad pointers.
Reto Achermann, David A. Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
PLOS@SOSP5
2021 A Model-Checked I2C Specification
Lukas Humbel, Daniel David Schwyn, Nora Hossle, Roni Haecki, Melissa Licciardello, Jan Schaer, David A. Cock, Michael Giardino, Timothy Roscoe
SPIN1
2019 Memory-Side Protection With a Capability Enforcement Co-Processor
abstract
Byte-addressable nonvolatile memory (NVM) blends the concepts of storage and memory and can radically improve data-centric applications, from in-memory databases to graph processing. By enabling large-capacity devices to be shared across multiple computing elements, fabric-attached NVM changes the nature of rack-scale systems and enables short-latency direct memory access while retaining data persistence properties and simplifying the software stack. An adequate protection scheme is paramount when addressing shared and persistent memory, but mechanisms that rely on virtual memory paging suffer from the tension between performance (pushing toward large pages) and protection granularity (pushing toward small pages). To address this tension, capabilities are worth revisiting as a more powerful protection mechanism, but the long time needed to introduce new CPU features hampers the adoption of schemes that rely on instruction-set architecture support. This article proposes the Capability Enforcement Co-Processor (CEP), a programmable memory controller that implements fine-grain protection through the capability model without requiring instruction-set support in the application CPU. CEP decouples capabilities from the application CPU instruction-set architecture, shortens time to adoption, and can rapidly evolve to embrace new persistent memory technologies, from NVDIMMs to native NVM devices, either locally connected or fabric attached in rack-scale configurations. CEP exposes an application interface based on memory handles that get internally converted to extended-pointer capabilities. This article presents a proof of concept implementation of a distributed object store (Redis) with CEP. It also demonstrates a capability-enhanced file system (FUSE) implementation using CEP. Our proof of concept shows that CEP provides fine-grain protection while enabling direct memory access from application clients to the NVM, and that by doing so opens up important performance optimization opportunities (up to 4× reduction in latency in comparison to software-based security enforcement) without compromising security. Finally, we also sketch how a future hybrid model could improve the initial implementation by delegating some CEP functionality to a CHERI-enabled processor.
Leonid Azriel, Lukas Humbel, Reto Achermann, Alex Richardson 0001, Moritz Hoffmann 0001, Avi Mendelson, Timothy Roscoe, Robert N. M. Watson, Paolo Faraboschi, Dejan S. Milojicic
ACM Trans. Archit. Code Optim.2
2018 Physical Addressing on Real Hardware in Isabelle/HOL
Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe
ITP2
2017 Towards Correct-by-Construction Interrupt Routing on Real Hardware
abstract
In this paper we address the problem of correctly configuring interrupts. The interrupt subsystem of a computer is increasingly complex: a zoo of different controllers with varying constraints and capabilities form a network with limited connectivity. An OS which aspires to provable correctness must manage a limited set of interrupt vectors, delegate interrupts to device drivers and configure the controllers correctly. No well-specified approach exists.
Lukas Humbel, Reto Achermann, David A. Cock, Timothy Roscoe
PLOS@SOSP1