Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report.

Despite significant progress made by runtime verification tools in recent years, memory errors remain one of the primary threats to software security. The present work is aimed at providing an objective up-to-date experience study on the capacity of modern online runtime verification tools to automatically detect security flaws in C programs. The reported experiments are performed using three advanced runtime verification tools (E-ACSL, Google Sanitizer and RV-MATCH) over 700 test cases belonging to SARD-100 test suite of the SAMATE project and Toyota ITC Benchmark, a publicly available benchmarking suite developed at the Toyota InfoTechnology Center. SARD-100 specifically targets security flaws identified by the Common Weakness Enumeration (CWE) taxonomy, while Toyota ITC Benchmark addresses more general memory defects, as well as numerical and concurrency issues. We compare tools based on different approaches - a formal semantic based tool, a formal specification verifier and a memory debugger - and evaluate their cumulative detection capacity. The results of the experiments indicate that the selected tools cumilatively detected 84% of all seeded defects. Although for several categories of errors detection rates are higher, we observed that applying several tools is beneficial for uncovering certain issues. For instance, in detecting concurrency issues of the Toyota ITC Benchmark, the highest per-tool result was 73%, whereas cumulative detection ratio of all three tools used together was 93%.