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.展开更多
The development of flight software for Unmanned Aerial Systems(UAS)is challenging due to the absence of an established development process defined by aerospace certification authorities.This research paper outlines ou...The development of flight software for Unmanned Aerial Systems(UAS)is challenging due to the absence of an established development process defined by aerospace certification authorities.This research paper outlines our methods and tools for analyzing flight-criticalUAS control software on the target hardware.We present our toolchain and methodology for evaluating the flight control computer stack,runtime memory,and timing characteristics.Additionally,we compare the performance of the flight control computer under various hardware and cache settings to justify,which hardware features should be enabled.The tools and processes employed in this research are deployable to any other development environment and are not restricted to the specific target hardware used in this paper.展开更多
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.
基金funding enabled and organized by Projekt DEALfunded by the Bavarian Ministry of Economic Affairs,Energy and Technology.
文摘The development of flight software for Unmanned Aerial Systems(UAS)is challenging due to the absence of an established development process defined by aerospace certification authorities.This research paper outlines our methods and tools for analyzing flight-criticalUAS control software on the target hardware.We present our toolchain and methodology for evaluating the flight control computer stack,runtime memory,and timing characteristics.Additionally,we compare the performance of the flight control computer under various hardware and cache settings to justify,which hardware features should be enabled.The tools and processes employed in this research are deployable to any other development environment and are not restricted to the specific target hardware used in this paper.
文摘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.
