Selfie: Towards Minimal Symbolic Execution
| Autor: | Abyaneh, Alireza, Bauer, Simon, Kirsch, Christoph, Mayer, Philipp, Mösl, Christian, Poncelet, Clement, Seidl, Sara, Sokolova, Ana, Widmoser, Manuel |
|---|---|
| Přispěvatelé: | Universität Salzburg, Poncelet Sanchez, Clément |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]
[INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC] [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS] [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS] RISC-V [INFO] Computer Science [cs] [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation Symbolic Execution Compilers Interpreters [INFO]Computer Science [cs] [INFO.INFO-MO] Computer Science [cs]/Modeling and Simulation Virtual machines Self-Referentiality |
| Zdroj: | MoreVMs 2018 MoreVMs 2018, Apr 2018, Nice, France. pp.70-77 |
| Popis: | International audience; Selfie is a fully 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 10k-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 in-memory linker, a RISC-U disassembler and debugger with replay, and a 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 a minimal 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 related 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 RISC-U code optimization. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|