首页|RSMC: A Safety Model Checker for Concurrency and Memory Safety of Rust
RSMC: A Safety Model Checker for Concurrency and Memory Safety of Rust
扫码查看
点击上方二维码区域，可以放大扫码查看
原文链接
NETL
NSTL
万方数据
Rust is a system-level programming language that provides thread and memory safety guarantee through a suite of static compiler checking rules and prevents segmentation errors.However,since compiler checking is too strict to confine Rust's programmability,the developers prefer to use the keyword "unsafe" to bypass compiler checking,through which the caller could interact with OS directly.Unfortunately,the code block with "unsafe" would easily lead to some serious bugs such as memory safety violation,race condition and so on.In this paper,to verify memory and concurrency safety of Rust programs,we present RSMC (Safety Model Checker for Rust),a tool based on Smack to detect concurrency bugs and memory safety errors in Rust programs,in which we combine concurrency primitives model checking and memory boundary model checking.RSMC,with an assertion generator,can automatically insert assertions and requires no programmer annota tions to verify Rust programs.We evaluate RSMC on two categories of Rust programs,and the result shows that RSMC can effectively fmd concurrency bugs and memory safety errors in vulnerable Rust programs,which include unsafe code.
Rustmemory safetyconcurrency safetymodel checking
YAN Fei、WANG Qizhong、ZHANG Liqiang、CHEN Yasha
展开 >
Key Laboratory of Aerospace Information Security and Trusted Computing, Ministry of Education, School of Cyber Science and Engineering, Wuhan University, Wuhan 430072, Hubei,China
Institute of Systems Engineering, Academy of Military Science of the Chinese People's Liberation Army, Beijing 100082, China
Supported by the National Basic Research Program of China (973 Program)
NETL
NSTL
万方数据
