Am 9.April 2025 hat Alexander Willecke seine Promotion mit der Verteidigung seiner Dissertationsschrift erfolgreich abgeschlossen.
In our paper, Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics, presented at the DATE conference, we explore a novel approach to symbolic execution of binary code by leveraging formal languages to describe instruction set architecture (ISA) semantics. Traditional methods for symbolic execution rely on transforming code into an intermediate representation (IR), which can be complex and error-prone. We investigate the use of machine-readable formal semantics to achieve a more accurate representation of ISA semantics. Our prototype for the RISC-V ISA demonstrates the ease with which this approach can be extended to additional instructions, and our experimental comparison with existing methods led to the discovery of five previously unknown bugs in the ISA implementation of the IR-based symbolic executor angr.
In our paper, HyperAlloc: Efficient VM Memory De/Inflation via Hypervisor-Shared Page-Frame Allocators, presented at the renowned EuroSys conference, we address a major challenge in virtualization—provisioning the right amount of DRAM to virtual machines (VMs). Many VMs face highly volatile memory demands, leading to either overprovisioning or poor quality of service during peak demand. While techniques like memory hotplugging and ballooning exist, they often fail to be DMA-safe or flexible enough.
We introduce HyperAlloc, a DMA-safe memory reclamation technique that significantly accelerates VM de/inflation, shrinking virtual machines up to 362 times faster the state of the art. HyperAlloc’s automatic memory reclamation also reduces the average memory footprint of a virtual machine by 17% compared to existing methods.