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 st...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.展开更多
Due to the absence of validity detection on pointers and automatic memory rubbish reclaim mechanisms in programming languages such as the C/C++language,software developed in these languages may have many memory safety...Due to the absence of validity detection on pointers and automatic memory rubbish reclaim mechanisms in programming languages such as the C/C++language,software developed in these languages may have many memory safety vulnerabilities,such as Use-After-Free(UAF)vulnerability.An UAF vulnerability occurs when a memory object has been freed,but it can still be accessed through a dangling pointer that points to the object before it is reclaimed.Since UAF vulnerabilities are frequently exploited by malware which may lead to memory data leakage or corruption,much research work has been carried out to detect UAF vulnerabilities.This paper investigates existing UAF detection methods.After comparing and categorizing these methods,an outlook on the future development of UAF detection methods is provided.This has an important reference value for subsequent research on UAF detection.展开更多
基金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.
文摘Due to the absence of validity detection on pointers and automatic memory rubbish reclaim mechanisms in programming languages such as the C/C++language,software developed in these languages may have many memory safety vulnerabilities,such as Use-After-Free(UAF)vulnerability.An UAF vulnerability occurs when a memory object has been freed,but it can still be accessed through a dangling pointer that points to the object before it is reclaimed.Since UAF vulnerabilities are frequently exploited by malware which may lead to memory data leakage or corruption,much research work has been carried out to detect UAF vulnerabilities.This paper investigates existing UAF detection methods.After comparing and categorizing these methods,an outlook on the future development of UAF detection methods is provided.This has an important reference value for subsequent research on UAF detection.
