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

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

연구 분야: Verification

학회: DAC '21: Proceedings of the 58th Annual ACM/IEEE Design Automation Conference

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.