Machine-Learning-Guided Selectively Unsound Static Analysis
Authors:
- Kihong HeoKHKihong Heo
- Hakjoo OhHOHakjoo Oh
- Kwangkeun YiKYKwangkeun Yi
- 1 May 2017
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 519-529
Abstract
We present a machine-learning-based technique for selectively applying unsoundness in static analysis. Existing bug-finding static analyzers are unsound in order to be precise and scalable in practice. However, they are uniformly unsound and hence at the risk of missing a large amount of real bugs. By being sound, we can improve the detectability of the analyzer but it often suffers from a large number of false alarms. Our approach aims to strike a balance between these two approaches by selectively allowing unsoundness only when it is likely to reduce false alarms, while retaining true alarms. We use an anomaly-detection technique to learn such harmless unsoundness. We implemented our technique in two static analyzers for full C. One is for a taint analysis for detecting format-string vulnerabilities, and the other is for an interval analysis for buffer-overflow detection. The experimental results show that our approach significantly improves the recall of the original unsound analysis without sacrificing the precision.Keywords
This publication has 20 references indexed in Scilit:
- Learning a strategy for adapting a program analysis via bayesian optimisation2015
- A user-guided approach to program analysis2015
- An Experimental Evaluation of Deliberate Unsoundness in a Static Program AnalyzerLecture Notes in Computer Science, 2015
- Abstractions from tests2012
- Context- and path-sensitive memory leak detection2005
- Saturn: A SAT-Based Tool for Bug Detection2005
- Testing static analysis tools using exploitable buffer overflows from open source code2004
- ARCHER2003
- Extended static checking for Java2002
- A training algorithm for optimal margin classifiers1992