1
1
# angr-viz
2
2
3
- This is a visualization tool for symbolic execution traces generated by hungr .
3
+ This is a visualization tool for symbolic execution traces generated by cozy .
4
4
You can use it to explore the tree of possible behaviors of a binary, before
5
5
and after the application of a patch.
6
6
@@ -19,19 +19,21 @@ cozy's `server.py`—check the documentation for that.
19
19
20
20
### Loading Traces
21
21
22
- Once you have the application running in your browser, you need JSON exports of
23
- two symbolic execution traces. Some example pairs of traces are available under
24
- example-traces. Drag and drop one export into the left "prepatch" pane, and one
25
- into the right "postpatch" pane. After a moment, you should see two trees,
26
- representing the possible execution paths in the two traces.
22
+ Once you have the application running in your browser, you need a JSON export
23
+ of a comparitive symbolic execution. Example traces are available as artifacts
24
+ from Cozy's CI builds,
25
+ [ here] ( https://github.com/draperlaboratory/cozy/actions/ ) . Drag and drop the
26
+ trace into the browser window that where you've opened cozy-viz. After
27
+ a moment, you should see two trees, representing the possible execution paths
28
+ in the two traces.
27
29
28
30
### Comparing Branches
29
31
30
32
To compare two execution paths, you can start by mousing over nodes in the
31
33
prepatch tree. A tooltip will let you see information associated with each
32
34
node: blocks of assembly, logical constraints on arguments, stdout and stderr
33
35
contents, and any error messages associated with failed states (failed states
34
- are highlighted in a light red color).
36
+ are highlighted in a light red color), and potentially some other properties .
35
37
36
38
Once you've found an interesting execution path in the prepatch tree, click on
37
39
the terminal node of the path. The right tree will then highlight the branches
@@ -109,7 +111,6 @@ The basic format is:
109
111
}
110
112
```
111
113
112
- angr-viz consolidates non-branching sequences of nodes, so there are likely
113
- more nodes listed in the JSON that will actually appear in the visualization.
114
114
Depending on how cozy was configured to generate the JSON, not every field
115
- above will necessarily appear.
115
+ listed under ` elements.nodes.data ` will necessarily appear, and some fields not
116
+ explicitly listed may occur.
0 commit comments