RSMC:A Safety Model Checker for Concurrency and Memory Safety of Rust  

作　　者：YAN Fei WANG Qizhong ZHANG Liqiang CHEN Yasha 

机构地区：[1]Key Laboratory of Aerospace Information Security and Trusted Computing,Ministry of Education,School of Cyber Science and Engineering,Wuhan University,Wuhan 430072,Hubei,China [2]Institute of Systems Engineering,Academy of Military Science of theChinese People’sLiberation Army,Beijing 100082,China

出　　处：《Wuhan University Journal of Natural Sciences》2020年第2期129-138,共10页武汉大学学报（自然科学英文版）

基　　金：Supported by the National Basic Research Program of China(973 Program)(2014CB340601)。

摘　　要：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 annotations to verify Rust programs.We evaluate RSMC on two categories of Rust programs,and the result shows that RSMC can effectively find concurrency bugs and memory safety errors in vulnerable Rust programs,which include unsafe code.

关 键 词：RUST memory safety concurrency safety model checking 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]