Binary Translation Group

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

Sebastian Reimers

PhD student

Simon Kammermeier

Student assistant

Theofilos Augoustis

Student assistant

Previous Members

Prof. Redha Gouicem

Associate Professor

Dr. Rodrigo Rocha

Senior Researcher

Ongoing & Past MSc/BSc theses, GRs, IDPs

You can find reports, theses, and final presentations of finished projects in our research work archive.

Execution State Comparison for Emulators using Symbolic ExecutionNicola Crivellin
Automated Test Case Generation for Emulators using Symbolic ExecutionAlp Berkman
Emulation of x86 Binaries on the RISC-V architectureSimon Kammermeier
Arancini Hybrid Binary Translator: Design of the Dynamic Binary Translators for ARM64 and RISC-VTheofilos Augoustis