Skip to content

lowRISC/synfi

Folders and files

NameName
Last commit message
Last commit date

Latest commit

author
Pascal Nasahl
Aug 29, 2023
2d08c4c · Aug 29, 2023

History

90 Commits
Aug 4, 2023
May 15, 2023
Nov 30, 2021
Apr 22, 2022
Nov 30, 2021
Jan 31, 2022
Jan 31, 2022
Nov 2, 2021
Sep 21, 2022
May 15, 2023
Apr 22, 2022
May 15, 2023
Jan 19, 2022
Nov 25, 2021
Feb 1, 2022
May 15, 2023
Feb 25, 2022
Jan 19, 2022
May 3, 2023

Repository files navigation

SYNFI: FI Formal Verification Framework

Introduction

This framework is capable of analyzing the effects of faults induced into synthesized gate-level netlists. The tool automatically extracts the circuit to analyze based on a fault specification file and injects multiple faults with different effects into this subcircuit. The effectiveness of the injected faults are evaluated and the tool verifies that the installed fault countermeasures detect these faults.

The framework is broken into three phases:

  1. a preprocessing phase,
  2. a fault injection phase, and
  3. an evaluation phase.

Further details can be found in the paper [0].

Usage

Install python3 and the corresponding packages:

$ pip3 install -r requirements.txt

The examples/circuit.json file contains the netlist for the aes_cipher_control module synthesized with the provided Yosys flow.

To convert a cell library (e.g., the NANGATE45 library), adapt the examples/config.json file and start the cell library generator:

$ ./cell_lib_generator.py -l NangateOpenCellLibrary_typical.lib -n 16 \
    -c examples/config.json -o cell_lib_nangate45_autogen.py

To start the preprocessing phase for this example netlist, create the output directory and invoke the parser:

$ ./parse.py -j examples/circuit.json -m aes_cipher_control \
    -o output/circuit.pickle

The parser preprocesses the provided netlist and creates a directed graph, which is then used by the fault injector to evaluate the effects of the induced faults. To run the fault injector with the example netlist and the example fault specification file, execute the fi_injector tool:

$ ./fi_injector.py -p output/circuit.pickle -f examples/fault_model.json -n 16 \
    -c cell_lib_nangate45_autogen.py

Publication

[0]: Nasahl, P., Osorio, M., Vogel, P., Schaffner, M., Trippel, T., Rizzo, D. and Mangard, S., 2022. SYNFI: Pre-Silicon Fault Analysis of an Open-Source Secure Element. IACR Transactions on Cryptographic Hardware and Embedded Systems.

Licensing

Unless otherwise noted, everything in this repository is covered by the Apache License, Version 2.0 (see LICENSE for full text).