VeriOover: A Verifier for Detecting Integer Overflow by Loop Abstraction
Abstract—When verifying software properties by using automatic formal verification methods, loop structures require manually provided loop invariants to enable automatic verification. To solve the difficulty of manually writing loop invariants in automated verification, we propose a novel approach to abstract the behavior of the loop structure. Through this abstraction method, the trends and ranges of variables in loop structures can be obtained. The verifier utilizes the abstracted information to automatically verify whether integer overflow vulnerabilities exist in the program. We implemented an automated formal verification tool, VeriOover, based on this method for detecting integer overflow in C language programs. The tool parses input programs into abstract syntax trees, converts the nondeterministic values into symbolic variables, and leverages symbolic execution and loop abstraction for program state analysis. VeriOover generates program assertions based on each program state to determine if an integer overflow exists in the program at that time. VeriOover is implemented and publicly available as an open-source project at https://github.com/Rw1nd/VeriOover.
Index Terms—software security, integer overflow, vulnerability detection, program verification
Jian Fang, Haipeng Qu
School of Computer Science and Technology, Ocean University of China, CHINA
Cite: Jian Fang, Haipeng Qu, "VeriOover: A Verifier for Detecting Integer Overflow by Loop Abstraction" Proceedings of 2023 the 13th International Workshop on Computer Science and Engineering (WCSE 2023), pp. 13-19, June 16-18, 2023.