Publikation
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, USA, 2021.
Zusammenfassung
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.