Bomberman is a ticking timebomb Trojan (TTT) specific verification tool that identifies suspicious state-saving components (SSCs) in a hardware design that could potentially be part of a TTT. Bomberman starts by assuming all SSCs are suspicious, and subsequently classifies each SSC as benign if it expresses values that violate a set of TTT-specific invariants (below) during verification simulations. Specifically, the set of invariants that define TTB SSC behavior are:
- values must never be repeated without a system reset, and
- all possible values must never be expressed without triggering the Trojan.
Bomberman consists of two main stages as shown in Figure 1:
- SSC Identification
- SSC Classification
Figure 1: Bomberman Architecture
The SSC Identification stage locates all SSCs in a hardware design described
in Verilog. It is broken into two stages: 1) Data-Flow Graph (DFG) Generation,
and 2) SSC Enumeration. During DFG Generation, a data-flow graph describing
bit-level signal dependencies is generated from the HDL using a custom Icarus
Verilog (IVL) compiler back-end. The DFG is encoded in the Graphviz .dot
format, and passed to the SSC Enumeration stage. The SSC Enumeration stage
analyzes the DFG and enumerates all signals that are the direct output of SSCs.
There are two types of SSCs that are identified: coalesced and distributed.
This list of SSCs is then passed to the SSC Classification for further
processing.
The SSC Classification stage analyzes verification simulations, in the value change dump (VCD) format, to check if any SSC violates either invariant (above) that indicates it is benign. SSCs that do not violate either invariant are reported to the user (in the form of JSON files) to be further manually scrutinized.
A technical paper describing Bomberman has been accepted to appear at the 2021 IEEE Symposium on Security and Privacy.
We provide a Dockerfile and four example circuits to demonstrate Bomberman on. To use it, follow the steps below to build the Docker image (containing all required tools and dependencies) and run Bomberman in a container. The four example circuits we provide to demonstrate Bomberman on are: a 128-bit AES accelerator (TrustHub), an 8-bit UART module (OpenCores), an OR1200 CPU (OpenCores), and a PicoRV32 CPU.
git clone https://github.com/timothytrippel/bomberman.git
cd bomberman- install Docker
- add your user to the
dockergroup make build-infra- grab a cup of coffee, step 4 could take a while :)
Note: if you would like to setup your own environment to use our toolchain, take a look at the Dockerfile for all required dependencies.
make all
The above command invokes the analyze_all.sh shell script within a container.
This script navigates to each circuit directory (e.g., circuits/<circuit>),
and invokes a master Makefile: circuits/common.mk. This Makefile does three
things. First, it executes the data-flow graph generator, which generates a
.dot file encoding the data-flow graph for the given hardware design.
Second, IVL is invoked to simulate the hardware design and generate a .vcd
file encoding the simulation trace. Third, the Bomberman script is
invoked to: 1) Enumerate all SSCs in the target hardware design, and
2) Classify each SSC as suspicious or benign.
Lastly, the number of suspicious SSCs computed at different points
throughout the simulation are output into several .json files.
The circuits/ directory contains test bench harnesses and Makefiles for
four example hardware designs to test Bomberman on. These designs are: a
128-bit AES accelerator (CNTR mode only), a UART core, an OR1200 CPU, and the
PicoRV32 RISC-V CPU (see above).
The bomberman/ directory contains the Python scripts that implement the
SSC Enumeration and SSC Classification stages (Figure 1). The main
script is contained in bomberman.py.
The bomberman sub-directory contains three hardware designs and
corresponding test benches to exercise the Bomberman toolchain. See the
Testing section below for how to test bomberman on these designs.
The tgt-dfg sub-directory contains 62 regression tests (i.e., hardware
designs) to exercise the IVL compiler back-end data-flow graph generator and
verify its correctness. See the Testing section below for how to execute these
tests.
The tgt-dfg/ directory contains the IVL compiler back-end data-flow graph
generator that implements part of the SSC Identification stage.
The third_party directory contains the RTL and supporting software for the
four example circuits we provide (above) to demonstrate Bomberman's utility.
In our project-wide Makefile (in the root project directory) we include a target to launch a shell within a container and mount source directories into the container to jumpstart development. To use this target simply run (after the Docker image has been built):
make dev
There are 62 regression tests to verify the correctness of the data-flow graph
generator contained in the tgt-dfg IVL back-end target module. Each regression
test consists of a small circuit, described in Verilog, that exercises the
data-flow graph generator's ability to handle various Verilog syntax and
expressions. All 62 regression tests should run, but only 61 tests should pass.
This is due to a minor (known) error in the way the graph-generator handles
duplicate signals in a concatenation, and will be fixed in a future release.
Each regression test generates a .dot file describing a data-flow graph from a simple test circuit. The resulting graph is automatically checked for correctness against provided gold examples. Additionally a PDF respresentation is generated for manual inspection of correctness, but this requires Graphviz to be installed. If you run these tests within the provide Docker image, this dependency is already installed.
To run all 62 regression tests run:
make dev(launch shell in container)cd tgt-dfg && make && cd ..(compile and install tgt-dfg)cd tests/tgt-dfg && make test
There are three test circuits to verify the correctness of the entire Bomberman
toolchain, from the data-flow graph generator to the simulation analysis scripts
(Figure 1). Each test is comprised of a small circuit design, and an
associated test bench that excerises the design. The three circuits are: a
simple counter (counter/), a D flip-flop (d_ff/), and a simple combinational
circuit (split/).
To run all three tests run:
make dev(launch shell in container, if not launched already)cd tests/bombermanmake all
To run only a single regression test use: make <design>, where <design> is
either counter, d_ff, or split.
Bomberman's data-flow graph generator (DFGG) can be utilized independently of
Bomberman for performing various static analyses of a circuit's HDL. The DFGG is
simply an Icarus Verilog (IVL) compiler back-end that generates data-flow graphs
in the Graphviz .dot format. For an example of
how to invoke it, check out the circuits/common.mk Makefile.
There are several Jupyter Notebooks for plotting the output of Bomberman
(encoded in .json files). The notebooks are located in the circuits/plots
directory. These can be used to reproduce plots from the technical paper
(linked above).
DISTRIBUTION STATEMENT A. Approved for public release. Distribution is unlimited.
This material is based upon work supported by the Under Secretary of Defense for Research and Engineering under Air Force Contract No. FA8702-15-D-0001. Any opinions, findings, conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Under Secretary of Defense for Research and Engineering.
© 2019 Massachusetts Institute of Technology.
MIT Proprietary, Subject to FAR52.227-11 Patent Rights - Ownership by the contractor (May 2014)
The software/firmware is provided to you on an As-Is basis
Delivered to the U.S. Government with Unlimited Rights, as defined in DFARS Part 252.227-7013 or 7014 (Feb 2014). Notwithstanding any copyright notice, U.S. Government rights in this work are defined by DFARS 252.227-7013 or DFARS 252.227-7014 as detailed above. Use of this work other than as specifically authorized by the U.S. Government may violate any copyrights that exist in this work.