We are a part of the Systems Research Group, working on the interoperability of different system architectures. Our research spans multiple areas, including emulation, correctness, operating systems and compilers.
We build binary translators to safely use programs built for one architecture on different and usually incompatible systems. We also explore hardware extensions (such as ARM MTE) to improve performance of existing emulators. Furthermore we test emulators (including our own) for correctness, using techniques such as fuzzing, symbolic execution and formal methods.
NOTE: we’re looking for students who want to write BSc/MSc theses or participate in Guided Research. If you are interested, please send us your application by following our application instructions.
NOTE: we’re specifically (but not exclusively) looking for computer science or math students who want to write a MSc thesis / do Guided Research in formal verification.
Ongoing Research Projects
Arancini: Hybrid binary translation
New computer architectures are emerging in cloud environments and consumer products. Not all software is compatible with those systems.
This project aims at running unmodified binaries on a different platform, by combining static translation, a lightweight runtime and on-demand dynamic translation.
Keywords: Binary translation, CPU architecture, Formal verification, RISC-V
Focaccia: Correctness framework for binary translators
Binary translators are complex pieces of software and very error prone. Debugging them is a difficult endeavor, due to hidden internals, transient bugs and hard to test edge-cases.
This project aims at finding errors in any stage of a translators pipeline. To do so, we use symbolic execution and formal methods. The framework is tool agnostic and tries to support different kinds of binary translators.
Keywords: Binary translation, Formal verification, Fuzzing, Symbolic execution
Gelato: Hardware assisted shared memory detection
Concurrent memory accesses often require expensive synchronization operations to behave correctly. However, compilers and binary translators might overestimate the number of synchronization operations, due to a lack of runtime information.
This project aims at using hardware extensions like ARM MTE to find pairs of threads that access memory concurrently. Using this information, synchronization can be en-/disabled on demand, improving performance without sacrificing safety.
Keywords: Binary translation, Hardware extensions, Transaction algorithms
Group Members
Theofilos Augoustis
Student assistant
Previous Members
Ongoing & Past MSc/BSc theses, GRs, IDPs
You can find reports, theses, and final presentations of finished projects in our research work archive.
| Type | Semester | Title | Student |
| MSc | Summer 2024 | Execution State Comparison for Emulators using Symbolic Execution | Nicola Crivellin |
| BSc | Winter 2023/24 | Automated Test Case Generation for Emulators using Symbolic Execution | Alp Berkman |
| BSc | Summer 2023 | Emulation of x86 Binaries on the RISC-V architecture | Simon Kammermeier |
| GR | Winter 2022/23 | Arancini Hybrid Binary Translator: Design of the Dynamic Binary Translators for ARM64 and RISC-V | Theofilos Augoustis |