| Title | Towards Reliable Spatial Memory Safety for Embedded Software by Combining Checked C with Concolic Testing |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Tempel, Sören, Herdt, Vladimir, Drechsler, Rolf |
| Conference Name | 2021 58th ACM/IEEE Design Automation Conference (DAC) |
| Keywords | Checked C, codes, Computer bugs, Concolic testing, Embedded Software, Human Behavior, human factors, memory safety, Metrics, Operating systems, Policy Based Governance, pubcrawl, resilience, Resiliency, RIOT, RISC-V, Runtime, Safe Coding, Safety, software reliability, Virtual Prototype, Writing |
| Abstract | 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. |
| DOI | 10.1109/DAC18074.2021.9586170 |
| Citation Key | tempel_towards_2021 |
Towards Reliable Spatial Memory Safety for Embedded Software by Combining Checked C with Concolic Testing