SafeOSL: Ensuring memory safety of C via ownership‐based intermediate language
SafeOSL: Ensuring memory safety of C via ownership‐based intermediate language
复制标题
DOI：
10.1002/spe.3057
复制
发表时间：
2021-12
期刊：
影响因子：
--
通讯作者：
Xiaohua Yin;Zhiqiu Huang;Shuanglong Kan;Guo-hua Shen;Zhe Chen;Yang Liu;Fei Wang
中科院分区：
文献类型：
--
作者：
Xiaohua Yin;Zhiqiu Huang;Shuanglong Kan;Guo-hua Shen;Zhe Chen;Yang Liu;Fei Wang
C语言的不安全特性给确保C程序的内存安全带来了很大的挑战，并且经常导致内存错误，从而导致漏洞。为了保证C语言的内存安全，已经提出了各种形式的验证技术。然而，它们中的大多数要么开销很大，比如模型检查中的状态爆炸问题，要么存在误报，比如抽象解释。在本文中，我们创新性地借鉴了Rust的所有权系统，提出了一种新颖而健全的静态内存安全分析方法，命名为SafeOSL。它的基本思想是一种基于所有权的中间语言，称为所有权系统语言（OSL），它捕获了Rust中所有权系统的特性。所有权系统指定变量和内存位置之间的关系，并维护可以确保内存安全的不变量。OSL的语义在K - framework中形式化，K - framework是一个基于重写逻辑的工具。要检查的C程序首先转换为OSL程序，然后由OSL语义进行检测。实验结果表明，SafeOSL可以有效地检测c语言的内存错误，并且翻译和实验表明，中间语言OSL可以被其他编程语言重用来检测内存错误。
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.