Skip to content

README_pathfinder.md

Latest commit

 

History

History
258 lines (167 loc) · 9.72 KB

README_pathfinder.md

File metadata and controls

258 lines (167 loc) · 9.72 KB

Pathfinder

Pathfinder logo

Installation and Dependencies

Dependencies

Do not forget to clone all submodules: git submodule update --init --recursive

Python packages

pandas six graphviz vcdvcd (our fork: https://github.com/comsec-group/vcdvcd)

Other

For viewing the graphs stored as .dot files: xdot

Yosys dependencies: see Yosys README.md

git-lfs ... for loading the VCDs used in the case studies (tests).

Building the TIFG pass

Call 'make' in the repository root of the repository (basically, follow Yosys' build steps).

Usage

The easiest is to follow one of the examples. See section Experiments.

Adding a new Design

  1. Create a copy of the "design_template" directory
  2. Add your design, copy structure of Ibex
  3. Copy ibex scripts and modify for new design
  4. Add the design's code to the "inputs/verilog_codes" directory
  5. Create a yosys script based on the template in "inputs/scripts"

Temporal Information Flow Graph (TIFG) generation

  1. In the repostiory root run "source ./env_pathfinder.sh" (in bash)
  2. Enter some design directory in designs, e.g. designs/Ibex, and run: source ibex_env.sh
  3. Place a verilog design into designs/<design_name>/inputs/verilog_codes and run source <design_name>_tifg.sh <./path/to/verilogfile> <topmodule> <output_name>

Generating a Taint Graph (TG)

First, prepare a VCD file and a corresponding configuration file. Place the VCD file into design/<design_name>/inputs/vcd, e.g., designs/Ibex/inputs/vcd/ibex_pc_taint.vcd Create a configuration file next to it, with the same filename stem, but ending in _config.sh. E.g., ibex_pc_taint_config.sh

  1. In the repository root run: "source ./env_pathfinder.sh"
  2. Go to designs folder, and enter the subdirectory of a design.
  3. In, e.g., designs/Ibex: "source ibex_env.sh"
  4. In, e.g., designs/Ibex: source "ibex_taint_graph.sh <tifg_name_without_ending> <vcd_name_witout_ending>

You find the generated graph in the dot/png file matching the input vcd file name.

Configuration options

Configure the taint path options in the beginning of the <vcd_name>_config.sh:

method=bottom #choices: combined or bottom - default = combined. 'combined' produces the isolated taint path between a given source and sink. The 'bottom' option is interesting if there are unconstrained taint inputs (or abstracted and unconstrained, e.g. this could happen in 𝜇CFI if we abstract a forwarding signal, but forget the no-taint assumption). The second option will reveal taint flows coming from these 'unknown' sources.

delay_type=default #choices: default or total - default = default. 'default' shows the clock cycle delay between nodes. 'total' is more interesting, as it shows the exact clock cycles at which information propagated between nodes.

add_flow_ctrl=ignore #choices: re-add or ignore - default = ignore. 're-add' adds flow control signals (i.e. untainted signals that directly interfere with the Path) to the taint graph. These are interesting for understanding why information propagated. Adding them adds some (often negligble) overhead to the genration. The graph can become large if they are added, so we recommend to first examine the graph without flow control signals, find the unexpected locations that taint reached, and then examine the graph with added flow control signals and focus on these identified unexpected locations.

ctrl=ignore #choices: re-add or ignore - default = ignore. 're-add' adds all flow control signals that have an edge marked as 'control' in the TIFG between the flow control signal and the tainted signal.

version=reduced #choices: time_sequence or reduced - default= reduced. 'reduced' is the more compact version.

Options to be configured for taint_graph.sh as environment variables (e.g. in a _config.sh file corresponding to a VCD):

TOP_MODULE_NAME

CLK_SIG_NAME

TAINT_SOURCE_NAME

TAINT_SINK_NAME

MITER ... set to True if the input VCD is obtained from a miter/self-composed design.

MITER_PREFIX1 MITER_PREFIX2 ... The prefixes that differ between the two miter copies.

MAX_N_CYCLES .. Specify the maximum of cycles that the bottom or top graph should span.

VCD_PREFIX_TO_REMOVE

CGRAHP_PREFIX_TO_ADD

PICKLED_VCD ... If the VCD file has already been analyzed once, a .pickle file with the same name was created next to it. With this option you can load it, which speeds up the loading of large traces.

XZ_UNTAINTED ... set to 1 if signals with X or Z value should be treated as tainted.

START_AT_LAST_TAINT ... By default Pathfinder starts path construction at the first clock cycle in which taint is found. This option lets it start at the last cycle.

Examples

Here you find a taint tracking example, obtained via formal verification.

Here you find a miter example, obtained via formal verification.

Here you find a taint tracking example, obtained via simulation.

Here we use VCD_PREFIX_TO_REMOVE because we generated the TIFG for a submodule of the module hierarchy used in the simulation test bench.

Experiments

The experiments of the paper can be reproduced as follows.

First, in the repository root, call source ./env_pathfinder.sh

Then, enter the design/<design_name> directory of which you want to run the experiment.

You can also run all experiments from the repository root, using this script: source ./run_experiments.sh. When you run this script for the first time, you will get some FileNotFoundErrors, for example: designs/Ibex/outputs/taint_paths/ibex_top_opentitan_941315_rst_sec1_slow_no_ls_rem_op1_prev.dot' not found. This is because the script tries to copy exsiting versions of Pathfinder's outputs before generating new ones. Afterwards it tries to compare the existing vs. the new output. The script is useful for developers to ensure that your changes did not change the output for the case studies (in case you did not intend to change them).

AES-400

Set up the environment: source aes_env.sh

Create the TIFG: source paper_tifg_cs.sh

Create the TG: source paper_cs_1.sh

Kronos

Set up the environment: source kronos_env.sh

Create the TIFG: source paper_tifg_cs.sh

Create the TG: source paper_cs_1.sh

Ibex custom

Set up the environment: source ibex_env.sh

Create the TIFG: source paper_tifg_cs_custom.sh

Create the TG: source paper_cs_1.sh

Ibex small

Set up the environment: source ibex_env.sh

Create the TIFG: source paper_tifg_cs_small.sh

Create the TG: source paper_cs_1.sh

CVA6 (new trace)

Set up the environment: source cva6_env.sh

Create the TIFG: source paper_tifg.sh

Create the TG: source paper_cs_1.sh

CVA6

Set up the environment: source cva6_env.sh

Create the TIFG: source paper_tifg.sh

Create the TG: source paper_cs_2.sh

BOOM

Set up the environment: source boom_env.sh

Create the TIFG: source paper_tifg.sh

Create the TG: source paper_cs_1.sh

Code organization

Folder structure

designs

Here are the examples for generating taint graphs based on VCDs for different hardware designs.

passes/tifg

The Yosys pass that generates the TIFG.

pathfinder

Here are the Python scripts that generate the taint graph, based on the TIFG and a VCD with matching signal names.

Classes

Needed information:

-VCD(s) -Clk signal -Taint sources -Taint sinks -Full TIFG of the design -Format of the output -The output graph configuration

VCD_information class:

Represents one counter example (VCD) Contains: -VCD Path -VCD object (from vcdvcd library) -List of taint sources -List of taint sinks -Clk signal name -VCD <-> TIFG name mapping Functions to use the mapping -List of taint signals and normal signals -List of tainted and untainted signals Does: -Import VCD (to be seen if its better to close it and reopen it when multiple VCDs are handled) -Make name_mapping -Access name_mapping -Identify signals to be removed from TIFG -Return clk time -Return the first taint time for a taint source or sink

TIFG_information class:

Represents a TIFG Contains: -TIFG (csv) path -TIFG as a pandas dataframe Does: -Find all connections involving a signal -Find all connections of form "signal" -> other -Find all connections of form other -> "signal" -Find all ctrl connections of form: ctrl_signal -> "signal"

Taint_path class:

Represents the taint path found by the tool Can stores multiple representations -Time sequence -Reduced time sequence

Contains: -A local copy of the design's TIFG. (A TIFG_information object) -The configuration of the taint graph -List of taint sources (TIFG naming convention) -List of taint sinks (TIFG naming convention)

TODOs

Improvements or known bugs.

In case the prefixes in the vcd and tifg don't match

Find the right ones and include a check into the tool that tells the user what the problem is. E.g. check for mismatching prefixes in vcd and graph and print a warning. For example check for matching signal names where there is a prefix in one of the two. Suggest to user how to fix it.

Use only one taint_path variable in the Taint_path graph

Currently we have an isolated_taint_path and reduced_taint_path attribute in the Taint_path graph. Ideally, merge them into one variable. Ensure that collapse_taint_path() is only called for the reduced graph and make sure not to break it!