Verification of RISC-V Embedded Software by Integrating Concolic Testing with SystemC-based Virtual Prototypes
![Druckversion Druckversion](/sites/all/modules/print/icons/print_icon.gif)
![Per E-Mail senden Per E-Mail senden](/sites/all/modules/print/icons/mail_icon.gif)
![PDF-Version PDF-Version](/sites/all/modules/print/icons/pdf_icon.gif)
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.