Towards Reliable Spatial Memory Safety for Embedded Software by Combining Checked C with Concolic Testing
Hosted in Virtual Platform
DescriptionIn 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 that 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. We demonstrate the effectiveness of our approach by applying it to the RIOT operating system.