Selfie: Towards Minimal Symbolic Execution
Selfie is a self-contained 64-bit implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, and (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine. Selfie is implemented in a single 8k-line file and can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. Selfie has originally been developed just for educational purposes but has recently become a research platform as well. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. In this paper, we report on an ongoing effort in designing and implementing a symbolic execution engine for RISC-U within selfie that is supposed to explore non-trivial parts of the system including itself. The idea is to identify the set of ingredients that are necessary to do this such as the data structures for representing traces, path conditions, and symbolic states as well as algorithms for SAT and SMT solving. The key difference to other more advanced projects is that we are interested in reasoning just about selfie, for now, and are able to change selfie if necessary, as reasoning target but also as integrated platform for compilation, (symbolic) execution, and virtualization. Since selfie generates unoptimized code we are also exploring ways to leverage our symbolic execution engine in code optimization.
|Extended Abstract (paper.pdf)||360KiB|
Mon 9 Apr
|11:00 - 11:30|
|11:30 - 12:00|
Alireza S. Abyaneh, Simon Bauer, Christoph Kirsch, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, Manuel WidmoserFile Attached
|12:00 - 12:30|