Towards Reliable Spatial Memory Safety for Embedded Software by Combining Checked C with Concolic Testing

Sören Tempel, Vladimir Herdt, Rolf Drechsler

In: 58th Design Automation Conference (DAC). Design Automation Conference (DAC-2021) December 5-9 San Francisco CA United States 2021.


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.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence