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.
Our paper, The New Costs of Physical Memory Fragmentation, won the Best Paper Award at the DIMES Workshop, co-located with the renowned SOSP'24 conference. Alexander Halbuer (LUH) presented our research, where we explore methods for energy savings in modern server systems by selectively powering down unused memory blocks. The study reveals that, while the operating system can effectively minimize fragmentation up to huge page sizes, it faces challenges with larger memory blocks. We also discuss the costs of memory in the cloud and advocate for more fine-grained price models. This work is part of the DFG-funded ParPerOS project.