Please use this identifier to cite or link to this item:
Title: SafeOSL: ensuring memory safety of C via ownership-based intermediate language
Authors: Yin, Xiaohua
Huang, Zhiqiu
Kan, Shuanglong
Shen, Guohua
Chen, Zhe
Liu, Yang
Wang, Fei
Keywords: Engineering::Computer science and engineering
Issue Date: 2022
Source: Yin, X., Huang, Z., Kan, S., Shen, G., Chen, Z., Liu, Y. & Wang, F. (2022). SafeOSL: ensuring memory safety of C via ownership-based intermediate language. Software: Practice and Experience, 52(5), 1114-1142.
Journal: Software: Practice and Experience
Abstract: 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.
ISSN: 0038-0644
DOI: 10.1002/spe.3057
Schools: School of Computer Science and Engineering 
Rights: © 2021 John Wiley & Sons, Ltd. All rights reserved.
Fulltext Permission: none
Fulltext Availability: No Fulltext
Appears in Collections:SCSE Journal Articles

Citations 50

Updated on Apr 18, 2024

Web of ScienceTM
Citations 50

Updated on Oct 27, 2023

Page view(s)

Updated on Apr 21, 2024

Google ScholarTM




Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.