A SAT-based Tool for Information Flow Alarm Classification
Jong-Gwon Kim*, Woosuk Lee**, Jaeseung Choi*, Chung-Kil Hur*, Kwangkeun Yi*
* Seoul National University & ** Georgia Tech
This page demonstrates Shovel, which finds a shortest function
call-return path from the source to the sink that satisfies a
given user constraint. For this demo, we allowed an arbitrary
function to be selected as a source or sink. The detailed
steps to use Shovel is described below.
Select a callgraph of program you want to test with. All
the benchmark programs we used in our experiment are
available from the select box. Also you can upload your own
callgraph in dot file format.
Choose the source and sink function from the select box,
which are going to be the start and end of the shortest
call-return path respectively.
Now provide the constraint you want to impose on the
function call-return path. For example, you can enforce the
call-return path to visit a specific function, or to include
a specific call/return edge. Also you can use &&(And),
||(Or), and ~(Not) to express your constraint.
Press the "Run Shovel" button, then the page will present the generated
shortest call-return path in several seconds.
Suppose that we want to inspect a call-return path that has
GPIC_vector as source and
as sink, from
gnuplot program. Also let's assume that we want the path to visit
AI_reset, but not visit
gnuplot program from the select box of 1. Callgraph section.
GPIC_vector as source
KTEK40reset as sink in the select box of
2. Information flow section.
AED_graphics from the select box
beside "Visit:" and press the "Add" button. This will
enforce the call-return path to
Press && button so you can continue adding conjunctive constraints.
Similarly add the constraint to
AI_reset, and insert &&
Press ~ button, and choose
from the select box beside "Visit:" and press the "Add"
button. This will prevent the path from
Finally, you can trigger Shovel by hitting the "Run
Demo result description
_G_': an imaginary function initializing
- Solid black arrow: call edge
- Dotted arrow: return edge
- Green arrow: branch (pair of call & return)
- For details, see II-A.'Backbone-Branch Decomposition' section of our paper.
Visit Shovel hompage for more information.