Why program when you can automatically synthesize OS code?
Event details
| Date | 25.05.2023 |
| Hour | 11:00 › 12:00 |
| Speaker | Dr. Reto Achermann, University of British Columbia |
| Location | |
| Category | Conferences - Seminars |
| Event Language | English |
Abstract
Address translation hardware is at the cornerstone of modern computer systems.
It provides a wide range of security-relevant features and abstractions such as memory partitioning, address space isolation and virtual memory.
Hardware designers
have developed different memory protection schemes with varying features and means of configuration. Correct configuration is mission-critical for a system's integrity.
It is the operating system's task to safely and securely manage and configure the memory hardware of a compute platform -- a task that operating systems developers must repeat for every new memory hardware unit.
In this talk, I present a new approach that frees the OS programmer from writing system code to setup and configure translation hardware. We leverage software synthesis to automatically generate correct systems code interfacing with translation hardware from a high-level, behavioral specification. By synthesizing correct, low-level systems code from a high-level specification we make porting operating systems to new hardware easier and require less effort. Moreover, we envision that our system can generate actual and simulated hardware components enabling research in new memory translation and protection schemes.
Biography
Reto Achermann is a Postdoctoral Research Fellow at the Systopia Lab of the Computer Science Department at the University of British Columbia working with Prof. Margo Seltzer. His research interests are at the intersection of memory and storage systems, hardware platforms, formal specification and verification, device drivers, and software synthesis. The main goal of his research is to help developers build build more reliable system software while at the same time reduce the development efforts.
He was part of the core Barrelfish operating system team, working on various subsystems such as memory management, capabilities, hardware abstractions, device drivers.
Reto Achermann received a PhD in computer science from ETH Zurich where he was advised by Prof. Timothy Roscoe.
Address translation hardware is at the cornerstone of modern computer systems.
It provides a wide range of security-relevant features and abstractions such as memory partitioning, address space isolation and virtual memory.
Hardware designers
have developed different memory protection schemes with varying features and means of configuration. Correct configuration is mission-critical for a system's integrity.
It is the operating system's task to safely and securely manage and configure the memory hardware of a compute platform -- a task that operating systems developers must repeat for every new memory hardware unit.
In this talk, I present a new approach that frees the OS programmer from writing system code to setup and configure translation hardware. We leverage software synthesis to automatically generate correct systems code interfacing with translation hardware from a high-level, behavioral specification. By synthesizing correct, low-level systems code from a high-level specification we make porting operating systems to new hardware easier and require less effort. Moreover, we envision that our system can generate actual and simulated hardware components enabling research in new memory translation and protection schemes.
Biography
Reto Achermann is a Postdoctoral Research Fellow at the Systopia Lab of the Computer Science Department at the University of British Columbia working with Prof. Margo Seltzer. His research interests are at the intersection of memory and storage systems, hardware platforms, formal specification and verification, device drivers, and software synthesis. The main goal of his research is to help developers build build more reliable system software while at the same time reduce the development efforts.
He was part of the core Barrelfish operating system team, working on various subsystems such as memory management, capabilities, hardware abstractions, device drivers.
Reto Achermann received a PhD in computer science from ETH Zurich where he was advised by Prof. Timothy Roscoe.
Practical information
- General public
- Free
- This event is internal
Organizer
- Prof. Sanidhya Kashyap
Contact
- Margaret Church