Showcase

S²E is currently being used for several scientific projects across the world. This page lists some of them.
We’ll be happy to list yours as well, just drop us a line!

  • Symbolic Execution for BIOS Security at Intel Corporation (Oleksandr Bazhaniuk, John Loucaides, Lee Rosenbaum, Mark R. Tuttle, and Vincent Zimmer).

    We are building a tool that uses symbolic execution to search for BIOS security vulnerabilities including dangerous memory references (call outs) by SMM interrupt handlers in UEFI-compliant implementations of BIOS. Given a snapshot of SMRAM, the base address of SMRAM, and the address of the variable interrupt handler in SMRAM, the tool uses S2E to run the KLEE symbolic execution engine to search for concrete examples of a call to the interrupt handler that causes the handler to read memory outside of SMRAM. We discuss our approach, our current status, our plans for the tool, and the obstacles we face.

  • Testing Linux Device Drivers at University of Wisconsin-Madison (Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift). SymDrive is a system for testing Linux and FreeBSD drivers without their devices. The system uses symbolic execution to remove the need for hardware, and provides three new features beyond prior symbolic-testing tools. First, SymDrive greatly reduces the effort of testing a new driver with a static-analysis and source-to-source transformation tool. Second, SymDrive allows checkers to be written as ordinary C and execute in the kernel, where they have full access to kernel and driver state. Finally, SymDrive provides an execution-tracing tool to identify how a patch changes I/O to the device and to compare device driver implementations. In applying SymDrive to 21 Linux drivers and 5 FreeBSD drivers, we found 39 bugs.

  • Chef at EPFL (Stefan Bucur and George Candea). Chef is a platform for obtaining symbolic execution engines for interpreted languages. It works by reusing the interpreter itself as an executable language specification, thus reducing the effort of obtaining an engine to a matter of days. The resulting engines can be used like any other engine for finding bugs, generating high-coverage test suites, assisting in debugging, and more.

  • Finding Trojan Message Vulnerabilities in Distributed Systems at EPFL (Radu Banabic, George Candea, and Rachid Guerraoui). Achilles helps developers discover Trojan Messages in distributed systems, i.e., messages that are accepted as valid by receiver nodes, but cannot be generated by any correct sender node. Achilles uses S2E to analyze both the client and server nodes of a target distributed system. It extracts predicates that define the messages that can be generated and accepted, respectively. In a sense, one can think of these predicates as representations of the grammar of messages in the protocol, as implemented in the client and in the server. The predicates are stored in the form of symbolic expressions and constraints. After extracting the server and client predicates, Achilles computes the predicate that defines Trojan messages as the difference between the two. In our evaluation, we show how Achilles can discovered Trojan messages in FSP, a file transfer system, and PBFT, a Byzantine-Fault-Tolerant State Machine Replication library. The Trojan messages discovered by Achilles lead to subtle bugs in the respective distributed systems.

  • File Systems Equivalence Checking at Max Planck Institute for Software Systems (Carreira João, Rodrigo Rodrigues, Rupak Majumdar). The goal of this project is to find functional bugs in systems code by checking the equivalence of multiple implementations that obey the same specification. Checking the equivalence of the different systems is performed by comparing the outputs and the logical state of different systems after executing the operations in their specification. Symbolic execution will allows us to reason about all possible executions and results of these operations. We specifically intend to apply this approach to find functional bugs in file systems.

  • Corruption Impact Analysis at University of Wisconsin (Subramanian Sriram, Sundararaman Swaminathan, Andrea C. Arpaci-Dusseau, Remzi Arpaci-Dusseau). Corruption Impact Analysis is a novel technique to understand the impact of memory corruptions in file systems. We employ selective symbolic execution to exhaustively explore the impact of memory corruptions on other in-memory data structures, disk and the user. Our technique emphasizes the importance of the location of corruption in addition to the corrupted data structure. We present a detailed case study of applying our technique to Ext2. We identify the data structures and code regions most sensitive to corruption and present corruption spectrums for each scenario. Thus, our technique offers developers the opportunity to improve file system reliability without sacrificing performance.

  • KleeNet project at Chair of Communication and Distributed Systems (ComSys), RWTH Aachen University (Raimondas Sasnauskas, Klaus Wehrle). Within KleeNet project, we are symbolically executing unmodified sensornet applications to generate distributed execution paths at high-coverage. However, the symbolic execution of Internet communication protocols is difficult since the software is not self-contained and hence heavily interacts with its surrounding environment (OS, libraries). Using S2E, we are able to switch between symbolic and native execution in a flexible way with low manual effort. Therefore, it allows us to drive the analysis towards interesting software parts.

  • Improving Automation in Developer Testing: Cooperative Developer Testing at North Carolina State University (Xie Tao). Developer testing, a common step in software development, involves generating sufficient test inputs and checking the behavior of the program under test during the execution of the test inputs. This project develops novel techniques and tools for improving automation in developer testing focusing on improving automation in test generation and test oracles. This project also investigates the methodology of cooperative developer testing: developers and tools cooperate in effectively accomplishing challenging tasks in software testing.

  • Exploiting Parallelism for Effective Low-Level Software Analysis at Institute of Software Chinese Academy of Sciences (Jian Liu, Bin Li, Sunlv Wang). In this project, one goal is to analyze typical application software and system code such as embedded OS or hypervisor. For example, we use S2E to analyze hypercalls in the Xen hypervisor. This project also plans to improve performance of S2E. We introduce concurrency algorithms and build a framework of scheduling rules to maximize the multi-path processing efficiently using multi-threading and multi-core processors. We are also devising heuristics to reduce the search time and to enhance efficiency.