Roman Meier


Last Name

Meier

First Name

Roman

ORCID

0009-0001-9165-0046

Organisational unit

03757 - Roscoe, Timothy / Roscoe, Timothy

Filters

2022 - 20243
Reset filters

Search Results

Publications1 - 3 of 3
  • seL4 as a CPU Driver for an OS for Real Computers
    Item type: Other Conference Item
    Meier, Roman; Liu, Zikai; Fiedler, Ben; et al. (2024)
    seL4 Summit 2024 Abstracts
  • Specifying the de-facto OS of a production SoC
    Item type: Conference Paper
    Fiedler, Ben; Meier, Roman; Schult, Jasmin; et al. (2023)
    KISV '23: Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification
    Verification of any operating system is inevitably relative to a model of the underlying hardware. Within the context of kernel verification, the underlying hardware model usually comprises of architectural correctness of the executing cores, but pays little attention to devices underneath barring the assumption that they are "trusted".Recent work has pointed out that the de facto operating system of a machine includes not only the kernel and processes running on top, but the multitude of other devices driving the actual hardware: security (co-)processors, DMA engines, network firmware, and more. The concept of the de facto OS shines light on a critical boundary between a kernel and the rest of hardware which is crucial to reasoning about both kernel isolation, and the security properties of the whole operating system. In this paper we report on our experience to date in specifying the de facto OS environment of a production System-on-Chip, and the implications of this effort so far for assured kernel isolation.
  • Declarative Dynamic Power Management
    Item type: Master Thesis
    Meier, Roman (2022)
    Modern computers feature large power networks that are non-trivial to safely control. The same is true for the Enzian resarch computer, which has a power network with 37 voltage regulators, plus a CPU and an FPGA, both of which impose complex requirements on the order in which their power and clock inputs may be operated safely. Initially, the command sequences to control the Enzians power network were written by hand, but this proved tedious and error-prone. Luckily, prior work in the systems group at ETH Zürich has already solved the problem of declarative static power management, but how to manage a dynamic platform that can change unexpectedly remained unadressed. In this thesis, we develop the design for a dynamic power management solution that is able to keep track of the changes the hardware undergoes, react to faults and other undesireable platform states, and generate command sequences online to steer the platform into a new state. Our solution can read a platform description from a declarative specification and is therefore not limited to one pre-defined platform. We also show experimentally that our plan generation mechanisms are fast enough for online usage.
Publications1 - 3 of 3