Safe4U: Identifying Unsound Safe Encapsulations of Unsafe Calls in Rust using LLMs
Rust is an emerging programming language that ensures safety through strict compile-time checks. A Rust function marked as unsafe indicates it has additional safety requirements (e.g., initialized, not null), known as contracts in the community. These unsafe functions can only be called within explicit unsafe blocks and the contracts must be guaranteed by the caller. To reuse and reduce unsafe code, the community recommends using safe encapsulation of unsafe calls (EUC) in practice. However, an EUC is unsound if any contract is not guaranteed and could lead to undefined behaviors in safe Rust, thus breaking Rust’s safety promise. It is challenging to identify unsound EUCs with conventional techniques due to the limitation in cross-lingual comprehension of code and natural language. Large language models (LLMs) have demonstrated impressive capabilities, but their performance is unsatisfactory owing to the complexity of contracts and the lack of domain knowledge. To this end, we propose a novel framework, Safe4U, which incorporates LLMs, static analysis tools, and domain knowledge to identify unsound EUCs. Safe4U first utilizes static analysis tools to retrieve relevant context. Then, it decomposes the primitive contract description into several fine-grained classified contracts. Ultimately, Safe4U introduces domain knowledge and invokes the reasoning capability of LLMs to verify every fine-grained contract. The evaluation results show that Safe4U brings a general performance improvement and the fine-grained results are constructive for locating specific unsound sources. In real-world scenarios, Safe4U can identify 8 out of 11 unsound EUCs from CVE. Furthermore, Safe4U detected 22 new unsound EUCs in the most downloaded crates, 13 of which have been confirmed.
Thu 26 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:15 | |||
11:00 25mTalk | Enhanced Prompting Framework for Code Summarization with Large Language Models Research Papers Minying Fang Qingdao University of Science and Technology, Xing Yuan Qingdao University of Science and Technology, Yuying Li Qingdao University of Science and Technology, Haojie Li Qingdao University of Science and Technology, Chunrong Fang Nanjing University, Junwei Du Qingdao University of Science and Technology DOI | ||
11:25 25mTalk | CrossProbe: LLM-empowered Cross-Project Bug Detection for Deep Learning Frameworks Research Papers Hao Guan University of Queensland, Southern University of Science and Technology, Guangdong Bai University of Queensland, Yepang Liu Southern University of Science and Technology DOI | ||
11:50 25mTalk | Safe4U: Identifying Unsound Safe Encapsulations of Unsafe Calls in Rust using LLMs Research Papers Huan Li Zhejiang University, China, Bei Wang Zhejiang University, China, Xing Hu Zhejiang University, Xin Xia Zhejiang University DOI |
This is the main event hall of Clarion Hotel, which will be used to host keynote talks and other plenary sessions. The FSE and ISSTA banquets will also happen in this room.
The room is just in front of the registration desk, on the other side of the main conference area. The two large doors with numbers “1” and “2” provide access to the Cosmos Hall.