Shovel Demo

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


Tutorial

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.

  1. 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.
  2. 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.
  3. 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.
  4. Press the "Run Shovel" button, then the page will present the generated shortest call-return path in several seconds.

Example

Suppose that we want to inspect a call-return path that has GPIC_vector as source and KTEK40reset as sink, from gnuplot program. Also let's assume that we want the path to visit AED_graphics and AI_reset, but not visit term_initialise.

  1. Choose gnuplot program from the select box of 1. Callgraph section.
  2. Choose GPIC_vector as source and KTEK40reset as sink in the select box of 2. Information flow section.

    1. Choose AED_graphics from the select box beside "Visit:" and press the "Add" button. This will enforce the call-return path to visit AED_graphics function.
    2. Press && button so you can continue adding conjunctive constraints.
    3. Similarly add the constraint to visit AI_reset, and insert &&
    4. Press ~ button, and choose term_initialise from the select box beside "Visit:" and press the "Add" button. This will prevent the path from visiting term_initialise function.
  3. Finally, you can trigger Shovel by hitting the "Run Shovel" button.

1. Callgraph

  View callgraph | Download dot file

Upload your callgraph dot file:

2. Information flow

Select source function:
Select sink function:

3. User constraint

Visit:
HaveCallEdge:
HaveRetEdge:
And:   Or:   Not:

Full syntax of user constraint
ex1) True
ex2) Visit "main"
ex3) HaveCallEdge "output_file" "output" &&
~ (VisitWith Any Incoming "compile_range")


Demo result description


Visit Shovel hompage for more information.