SafeOSL: Ensuring memory safety of C via ownership‐based intermediate language

Autor: Xiaohua Yin, Zhiqiu Huang, Shuanglong Kan, Guohua Shen, Zhe Chen, Yang Liu, Fei Wang
Přispěvatelé: School of Computer Science and Engineering
Rok vydání: 2021
Předmět:
Zdroj: Software: Practice and Experience. 52:1114-1142
ISSN: 1097-024X
0038-0644
DOI: 10.1002/spe.3057
Popis: The unsafe features of C make it a big challenge to ensure memory safety of C programs, and often lead to memory errors that can result in vulnerabilities. Various formal verification techniques for ensuring memory safety of C have been proposed. However, most of them either have a high overhead, such as state explosion problem in model checking, or have false positives, such as abstract interpretation. In this article, by innovatively borrowing ownership system from Rust, we propose a novel and sound static memory safety analysis approach, named SafeOSL. Its basic idea is an ownership-based intermediate language, called ownership system language (OSL), which captures the features of the ownership system in Rust. Ownership system specifies the relations among variables and memory locations, and maintains invariants that can ensure memory safety. The semantics of OSL is formalized in K-framework, which is a rewriting-logic based tool. C programs to be checked are first transformed into OSL programs and then detected by OSL semantics. Experimental results have demonstrated that SafeOSL is effective in detecting memory errors of C. Moreover, the translations and experiments indicate that the intermediate language OSL could be reused by other programming languages to detect memory errors. This work was supported by the National Natural Science Foundation of China (No. 61902180, 61772270, 62172217, U1533130), and National Key Research and Development Program of China (No. 2018YFB1003902).
Databáze: OpenAIRE
Externí odkaz: