Verification of Embedded Software Binaries using Virtual Prototypes

Abstract

This chapter presents efficient Virtual Prototype (VP) based approaches for Software (SW) verification. They improve the existing VP-based SW verification flow by integrating stronger coverage metrics and providing automated test-case generation techniques as well as leverage formal methods. Ensuring correct functional behavior is very important to avoid errors and security vulnerabilities (such as buffer overflows). The first approach integrates concolic testing into the VP. Essentially, concolic testing is an automated technique that successively explores new paths through the SW program by solving symbolic constraints, that are tracked alongside the concrete execution. However, an integration of concolic testing with VPs is challenging due to complex HW/SW interactions and peripherals. The proposed solution enables a high simulation performance with accurate results and comparatively little effort to integrate peripherals with concolic execution capabilities. The second approach leverages state-of-the-art CGF in combination with VPs to enable a scalable and efficient verification of embedded SW binaries. To guide the fuzzing process the coverage from the embedded SW is combined with the coverage of the SystemC-based peripherals of the VP.