We conduct research on design and analysis problems at the boundary between hardware and software.
Our recent work focuses on the following topics:
Microarchitectural Security
Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations like caches and speculative execution. To use modern hardware securely, programmers must be aware of how these optimizations impact the security of their code.
In this context, we work on
- Program analysis techniques to analyze the vulnerability of software to microarchitectural attacks
- Design and verification of open-source microarchitectures with rigorous security guarantees
- Fuzzing/systematic testing of modern microarchitectures w.r.t. microarchitectural vulnerabilities
Timing Predictability
Real-time systems have to meet deadlines imposed by the physical environment. E.g. an airbag controller needs to detect a crash and decide to fire the appropriate airbags within a few milliseconds. For safety-critical real-time systems, we need to prove that all deadlines are guaranteed to be met. To this end, worst-case execution time (WCET) analysis [10] determines upper bounds on programs' execution times. In modern systems, the execution time of software heavily depends on the state of the underlying hardware. This means that caches, pipelining, speculative execution all need to be taken account in WCET analysis.
In this context, we work on
- Timing analysis techniques to accurately and efficiently account for particular hardware features, such as caches or speculation
- Principles for the design of timing-predictable microarchitectures
Performance Analysis and Understanding
Modern microarchitectures are some of the world's most complex man-made systems. As a consequence, it is increasingly difficult to predict, explain, let alone optimize the performance of software running on such microarchitectures.
In this context, we work on
- Automatic construction of faithful microarchitectural models as a basis for performance prediction, explanation, and optimization
- Tools for explaining (and potentially optimizing) the performance of code based on microarchitectural models
News
- January 2024: Our paper "Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors" has been nominated for the best-paper award at the Design Automation and Test in Europe Conference (DATE 2024). Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures.
- November 2023: Our paper "Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts" has received a distinguished paper award at the 30th ACM SIGSAC Conference on Computer and Communication Security (CCS 2023). In this paper we introduce LeaVe, a verification tool that verifies register-transfer level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction.
- November 2023: Our paper "Leveraging LLVM's ScalarEvolution for Symbolic Data Cache Analysis" has received an outstanding paper award at the 44th IEEE Real-Time Systems Symposium (RTSS 2023). In this paper we introduce a symbolic cache analysis technique. This work overcomes challenges of data cache analysis by introducing a symbolic program representation, developing a symbolic cache analysis for this representation, and by exploiting LLVM's ScalarEvolution to analyze real-world programs.
- June 2021: Our paper "Hardware-Software Contracts for Secure Speculation" has received a best paper award at the IEEE Symposium on Security and Privacy 2021 ("Oakland"). It introduces a framework for specifying hardware-software contracts, which is used to provide the first formalization and comparison of the security guarantees provided by a representative class of mechanisms for secure speculation.