Bomberman

Bomberman is a ticking timebomb (TTB) Trojan specific verification tool. It identifies suspicious state-saving components (SSCs) in a hardware design that could potentially be part of a TTB Trojan. Bomberman starts by assuming all SSCs are suspicious, and subsequently classifies each SSC as benign if it expresses values that violate a set of invariants during verification simulations.

TTBs are comprised of SSCs that incrementally approach a triggering value. The set of invariants that define TTB SSC behavior are as follows:

values must never be repeated without a system reset, and

all possible values must never be expressed without triggering the Trojan.

Bomberman leverages these two invariants while analyzing simulation results of a hardware design to classify whether or not an SSC is part of a TTB Trojan.

Bomberman consists of two main stages as shown in Figure 1:

SSC Identification

Simulation Analysis

Figure 1: Bomberman Architecture

The SSC Identification stage locates all SSCs in a hardware design described in Verilog. It does so by first generating a data-flow graph from the HDL using a custom Icarus Verilog (IVL) compiler back-end. The data-flow graph is encoded in the Graphviz .dot format, and passed to the next stage.

The Simulation Analysis stage parses: 1) the .dot file encoding the circuit data-flow graph generated by the SSC Identification stage, and 2) the verification simulation results, in the Value Change Dump (.vcd) format, generated by a hardware simulator (e.g., IVL). First, during SSC Enumeration, it enumerates all SSCs in the data-flow graph, marking each SSC as suspicious. There are two types of SSCs that are identified: coalesced and distributed. Next, during Invariant Testing, the values expressed by each SSC over the course of the simulation timeline are extracted from the simulation results. SSCs that violate either of the two invariants listed above are marked as benign.