Title
Precise Divide-By-Zero Detection with Affirmative Evidence
Abstract
The static detection of divide-by-zero, a common programming error, is particularly prone to false positives because conventional static analysis reports a divide-by-zero bug whenever it cannot prove the safety property - the divisor variable is not zero in all executions. When reasoning the program semantics over a large number of under-constrained variables, conventional static analyses significantly loose the bounds of divisor variables, which easily fails the safety proof and leads to a massive number of false positives. We propose a static analysis to detect divide-by-zero bugs taking additional evidence for under-constrained variables into consideration. Based on an extensive empirical study of known divide-by-zero bugs, we no longer arbitrarily report a bug once the safety verification fails. Instead, we actively look for affirmative evidences, namely source evidence and bound evidence, that imply a high possibility of the bug to be triggerable at runtime. When applying our tool Wit to the real-world software such as the Linux kernel, we have found 72 new divide-by-zero bugs with a low false positive rate of 22%.
Year
DOI
Venue
2022
10.1145/3510003.3510066
2022 ACM/IEEE 44TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2022)
DocType
ISSN
Citations 
Conference
0270-5257
0
PageRank 
References 
Authors
0.34
0
5
Name
Order
Citations
PageRank
Yiyuan Guo100.68
Jinguo Zhou200.34
Peisen Yao332.40
Qingkai Shi4447.50
Charles Zhang551228.97