Abstract
We present a tool, called SHOVEL, that assists the user to quickly classify, as true or false, alarms reported by information flow analyzers. Specifically, SHOVEL helps the user by finding a shortest function call-return path from the source to the sink that satisfies a given user constraint. In this paper, we empirically show that our approach is very effective by classifying 351 alarms for 42 open-source C programs and identifying 48 true alarms with crash bugs, three of which were assigned CVE numbers. We also report the patterns of using SHOVEL during our manual alarm classification.
SHOVEL finds a shortest path using an off-the-shelf MaxSAT solver taking as user constraint a Boolean formula on the call/return edges of the call graph. For this, we develop a novel algorithm that encodes the constrained shortest path problem into a Boolean formula in a counter-example guided refinement fashion. Our algorithm is very easy to implement but also very efficient. In our empirical study, SHOVEL responded mostly within a few seconds even for programs of 100K LOC.