Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions
Abstract interpretation is widely used to determine programs’ numerical properties. However, current abstract domains primarily focus on mathematical semantics, which do not fully capture the complexities of real-world programs relying on machine integer semantics and involving extensive bit-vector operations. This paper presents a solution that combines a bit-level abstraction and a word-level abstraction to capture machine integer semantics. First, we generalize the bit-level abstraction used in the Linux eBPF verifier for determining known and unknown bits of real-world programs, by supplementing all required operations as a standard abstract domain. Based on this abstraction, we design an abstract domain that is signedness-aware and simultaneously retains both the above bit-level and the world-level bound information. These two levels of information cooperate via a standard reduced product operation to improve analysis precision. We implement the proposed domains in the Crab analyzer and the out-of-kernel eBPF verifier PREVAL. Experiments demonstrate their effectiveness in analyzing SV-COMP benchmark programs, assisting hardware designs, and eBPF verification.
Thu 26 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:15 | Program Analysis 1Research Papers at Cosmos 3B Chair(s): Martin Kellogg New Jersey Institute of Technology | ||
14:00 25mTalk | Bridge the Islands: Pointer Analysis for Microservice Systems Research Papers Teng Zhang Nanjing University, Yufei Liang Nanjing University, Ganlin Li Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Yue Li Nanjing University DOI | ||
14:25 25mTalk | Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions Research Papers Guangsheng Fan National University of Defense Technology, Liqian Chen National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Wenyu Zhang National University of Defense Technology, Peisen Yao Zhejiang University, Ji Wang National University of Defense Technology DOI | ||
14:50 25mTalk | Type-Alias Analysis: Enabling LLVM IR with Accurate Types Research Papers Jinmeng Zhou Zhejiang University, Ziyue Pan Zhejiang University, Wenbo Shen Zhejiang University, Xingkai Wang Zhejiang University, Kangjie Lu University of Minnesota, Zhiyun Qian University of California at Riverside, USA DOI |
Cosmos 3B is the second room in the Cosmos 3 wing.
When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.