Symbolic execution is an SMT-based software verification and testing technique. Symbolic execution requires tracking performed computations during software simulation to reason about branches in the software under test. The prevailing approach on symbolic execution of binary code tracks computations by transforming the code to be tested to an architecture-independent intermediate representation (IR) and then symbolically executes this IR. However, the resulting IR must be semantically equivalent to the binary code, making this process complex and error-prone. The semantics of the binary code are specified by the targeted instruction set architecture (ISA), commonly given in natural language and requiring a manual implementation of the transformation to an IR. In recent years, the use of formal languages to describe ISA semantics in a machine-readable way has gained increased popularity. We investigate the utilization of such formal semantics for symbolic execution of binary code, achieving an accurate representation of instruction semantics. We present a prototype for the RISC-V ISA and conduct a case study to demonstrate that it can be easily extended to additional instructions. Furthermore, we perform an experimental comparison with prior work which resulted in the discovery of five previously unknown bugs in the ISA implementation of the popular IR-based symbolic executor angr.

The development process for new embedded systems relies increasingly on simulation, e.g. to develop hardware and software components in parallel using virtual prototyping. The central component of a virtual prototype is the instruction set simulator (ISS) which implements instruction execution for a specific instruction set architecture (ISA). To avoid erroneous behavior during software simulation, it is paramount to ensure that the provided ISS implements the ISA exactly as specified, i.e. that there are no discrepancies between the hardware and the VP. In order to increase confidence in the correctness of the VP's ISS, it is advantageous to generate it automatically from a formal model of the ISA instead of implementing it manually. While a variety of formal ISA models have been proposed in prior work, they are presently not widely used in the VP domain. We attempt to ease employment of formal models for ISS generation in this domain. To this end, we reduce the integration effort through a simulator-agnostic ISS generation approach that integrates well with existing simulators and existing vendor-supplied VP components. Our approach leverages a formal RISC-V ISA model which exclusively describes instruction semantics and abstracts interactions with hardware components through an interface model, thus encapsulating interactions with simulator-specific code. As part of our experiments, we were able to generate an ISS for the popular RISC-V implementations Spike and RISC-V VP, thereby replacing their manually written implementations. Performed benchmarks indicate that the generated ISS offers the same simulation performance as a manually written one, while still passing the official RISC-V tests.

IoT devices offer insufficient protections against exploitation of critical programming errors (such as buffer overflows) it is therefore paramount to sufficiently test IoT software before deployment. A central source of these errors is the implementations of stateful network protocols used in the IoT (e.g., MQTT-SN). Unfortunately, comprehensive automated testing of such protocol implementations is challenging due to their large state space. Furthermore, prior work on automated testing of protocol implementations focuses on conventional desktop systems and does thus not address challenges specific to the IoT domain (e.g., handling of peripheral interactions). In this publication, we leverage symbolic execution (an automated software testing technique) for testing stateful network protocol implementation in the IoT domain. To mitigate issues regarding the state-space explosion, we propose a novel symbolic execution approach which is based on created protocol state and message format specifications and specifically tailored to the IoT domain. We employ our specification-based symbolic execution approach to test protocol implementations provided by two popular IoT operating systems. Our experiments indicate that a significant increase in code coverage can be achieved using our automated software testing approach. We were further able to discover three critical and previously unknown bugs in network protocol implementations provided by the RIOT operating system.

Software written for constrained devices, commonly used in the Internet of Things (IoT), is primarily written in C and thus subject to vulnerabilities caused by the lack of memory safety (e.g. buffer overflows). To prevent these vulnerabilities, we present a systematic approach for finding spatial memory safety violations in low-level code for constrained embedded devices. We propose implementing this approach using SystemC-based Virtual Prototypes (VPs) and illustrate an architecture for a non-intrusive integration into an existing VP. To the best of our knowledge, this approach is novel as it is the first for finding spatial memory safety violations which addresses challenges spe-cific to constrained devices. Namely, limited computing resources and utilization of custom hardware peripherals. We evaluate our approach by applying it to the IoT operating system RIOT where we discovered seven previously unknown spatial memory safety violations in the network stack of the operating system.

Symbolic execution is a powerful software testing technique for finding bugs in complex software. Unfortunately, following the symbolic execution and understanding its results is challenging. However, since symbolic execution is commonly not complete (i.e. due to path explosion) it is important to understand the limitations of the performed analysis. Otherwise, insufficiently tested code parts may not be identified and bugs remain unnoticed. Prior work attempts to address this problem via 2D visualizations which communicate properties of the performed analysis to the verification engineer. Since symbolic execution requires a visualization of several properties, such 2D visualizations often lack important information or end up being dense and difficult to understand.In order to overcome this limitation, we propose a novel 3D visualization of symbolic execution which allows visualizing additional properties via the third dimension. For this purpose, we have implemented a 3D visualization for the symbolic execution of RISC-V machine code and evaluate this implementation by comparing it to an existing 2D visualization. Our results demonstrate that the third dimension allows us to include additional information which is not captured by the existing 2D visualization. In order to stimulate further research on 3D visualization of symbolic execution, we have released our implementation as open source software.

Constrained Internet of Things (IoT) devices with limited computing resource are increasingly employed in security critical areas. Therefore, it is important for the firmware of these devices to be tested sufficiently. On non-constrained conventional devices, dynamic testing techniques (e.g. fuzzing, symbolic execution, or concolic testing) are successfully utilized to discover critical bugs in tested software. Unfortunately, the diverse ecosystem and the dependence on low-level details of a wide range of peripherals makes it difficult to use these techniques in the IoT context. In order to address these challenges, we present SymEx-VP an open source emulation-based approach for concolic testing of IoT firmware. SymEx-VP is a virtual prototype for RISC-V hardware platforms and allows concolic testing of RISC-V machine code. To support a wide range of different peripherals, SymEx-VP utilizes SystemC, a hardware modeling language for C++. By employing a SystemC extension mechanism, SymEx-VP can inject concolic inputs into the emulated firmware through the memory-mapped I/O peripheral interface of existing SystemC peripheral models. This allows us to support different operating systems and libraries used in the IoT with minimal integration effort. We provide an extensive description of SymEx-VP, illustrate peripheral modeling and firmware testing using it by example, and perform tests with four operating systems to demonstrate the advantages of our OS-agnostic firmware testing method.

Compliance testing for RISC-V is very important. Essentially, it ensures that compatibility is maintained between RISC-V implementations and the ever growing RISC-V ecosystem. Therefore, an official Compliance Test-suite (CT) is being actively developed. However, it is very difficult to achieve that all relevant functional behavior is comprehensively tested.

In this paper we propose to combine the safe C dialect Checked C with concolic testing to obtain an effective methodology for attaining safer C code. Checked C is a modern and backward compatible extension to the C programming language which provides facilities for writing memory-safe C code. We utilize incremental conversions of unsafe C software to Checked C. After each increment, we leverage concolic testing, an effective test generation technique, to support the conversion process by searching for newly introduced and existing bugs.Our RISC-V experiments using the RIOT Operating System (OS) demonstrate the effectiveness of our approach. We uncovered 4 previously unknown bugs and 3 bugs accidentally introduced through our conversion process.

We propose an effective methodology for integrating Concolic Testing (CT) with SystemC-based Virtual Prototypes (VPs) for verification of embedded SW binaries. Our methodology involves three steps: 1) integrating CT support with the Instruction Set Simulator (ISS) of the VP, 2) utilizing the standard TLM-2.0 extension mechanism for transporting concolic values alongside generic TLM transactions, and 3) providing lightweight concolic overlays for SystemC-based peripherals that enable non-intrusive CT support for peripherals and thus significantly reduce the CT integration effort. Our RISC-V experiments using the RIOT operating system demonstrate the effectiveness of our approach.

Constrained IoT devices with limited computing resources are on the rise. They utilize low-end multithreaded operating systems (e.g. RIOT) where each thread is assigned a fixed stack size during the development process. In this regard, it is important to choose an appropriate stack size which does not cause stack overflows and at the same time does not waste scarce memory resources by overestimating the required thread stack size. In this paper we propose an in-vivo technique for stack overflow detection and stack size estimation that leverages Virtual Prototypes (VPs) and is specifically tailored for low-end multithreaded IoT operating systems. We focus on SystemC-based VPs which operate on the TLM abstraction level. VPs are an industrial proven modeling standard to enable early software development and testing. We propose a non-intrusive extension for existing VPs which allows detecting stack overflows and provides a stack size estimation, which is beneficial to a VP-based development process. Our analysis works in-vivo, hence no modification of the executed software binary is required between testing and deployment. Our evaluation using the RIOT operating system revealed two previously unknown stack overflows in RIOT and identified potential stack size overestimation.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high simulation performance and at the same time yield accurate results, which are two conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-V ISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments, using bare-metal and operating system based benchmarks, demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high performance and at the same time yield accurate results, which are conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-VISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.