Verification of RISC-V Embedded Software by Integrating Concolic Testing with SystemC-based Virtual Prototypes

Sören Tempel, University of Bremen, D

Abstract

In this presentation we show an effective methodology for verification of RISC-V embedded software by integrating concolic testing with SystemC-based virtual prototypes. The integration involves extending the instruction set simulator to support concolic execution and utilizing TLM extensions to support propagation of concolic values over the TLM-2.0 bus. Our RISC-V based experiments using the RIOT operating system demonstrate the effectiveness of our approach. Using a path analyzer for spatial memory safety we found several new bugs in the network stack of the RIOT operating system.

Biography

Sören Tempel is pursuing a PhD degree at the University of Bremen with the Group of Computer architecture. His research interests include verification of embedded RISC-V software using symbolic execution techniques and virtual prototyping as well as security aspects of constrained devices used in the Internet of Things.