SAMVA

SAMVA is a framework for efficiently searching vulnerabilities in applications under multiple instruction-skip faults with various widths. SAMVA relies on static analysis to determine attack paths and simulation to evaluate them. It is configurable with the fault injection capacity of the attacker and the attacker’s objective.

The current version of SAMVA supports two fault models:

• Instruction-Skip: where instructions can be considered as replaced by NOP. This model is named "TrueNOP" in SAMVA.
• Instruction-Replay: where instruction words can be replayed in order to skip the following instructions. This model corresponds to the one observed by perturbing the clock through glitching or EM attacks. This model is named "Replay" in SAMVA.

Citation

An article has been published at COSADE 2023. Read it if you want further explanations about the algorithms used.

Gicquel et al. "SAMVA: Static Analysis for Multi-Fault Attack Paths Determination." International Workshop on Constructive Side-Channel Analysis and Secure Design. Cham: Springer Nature Switzerland, 2023.

Legal Information

This project is licensed under the GNU Affero General Public License v3.0 (AGPLv3). See the LICENSE file for details. The authors provide this project as-is and make no guarantees.

This software is the property of Inria. This project has been deposited with the Agence pour la Protection des Programmes (APP) and is the property of Inria.

This software is under active development. Some bugs can be present.
For any question, contact Antoine Gicquel at antoine.gicquel@inria.fr.

How does it work?

First, the analysis automatically generates the control-flow graph (CFG) of the binary. Then the CFG is extended and annotated to reflect the effects of possible fault injections. Finally, the analysis infers a set of attack paths that meet the attacker capacity. Each output attack path takes the form of a list of instruction with the faults to inject (location, width).

Since SAMVA does not rely on data-flow for performance concerns, the attack-paths found must be validated through simulation, by using the unicorn emulator (default and recommended) or a modified version of the gem5 simulator.

SAMVA is built in a modular way with extensibility in mind. It can be used directly with the commands that are already included, but it can also be used as a library for your own fault models and attacker models. The information gathering, the CFG annotation process and attack-path search all work in passes, that can be easily added or removed according to specific needs.

Installation

SAMVA requires Python 3.13 and is not compatible with Pypy because of PyGhidra dependency. It uses uv to manage the Python dependencies, Python versions, and run tasks.

uv (Python package manager)

To install dependencies and run tasks in this project, SAMVA relies on uv. It is a fast Python package manager and virtual environment tool written in Rust.

It may be available through your system package manager (e.g. dnf for Fedora or brew for MacOS).
Otherwise, download and install uv from official website:

https://github.com/astral-sh/uv

Install dependencies

Python libraries

uv is used to install SAMVA Python dependencies, symply run:

uv sync

Ghidra

SAMVA requires Ghidra, versions > 12.0.

1. Install Ghidra from the official distribution : Ghidra releases on GitHub.
2. Set the environment variable GHIDRA_INSTALL_DIR to the Ghidra installation directory. For example:

export GHIDRA_INSTALL_DIR=/path/to/ghidra

Documentation

The documentation is available at: https://samva-project.gitlabpages.inria.fr/samva/

It is possible also to generate the project documentation locally:

uv run task docs

Find the generated documentation at: docs/build/index.html

Usage

SAMVA runs through a command-line interface that defines analysis and validation workflows by chaining commands. Some commands need to be chained to work properly while others can used as standalone. The main SAMVA command is evaluate. It runs security evaluation against multi-fault attacks. Then this command can be chained with hardware validation commands to easily create evaluation workflow and fault injection campaigns. This command can be chained with other hardware validation commands to create complete evaluation workflow. See the documentation to learn more.

evaluate command

The command takes two positional parameters:

• BIN_PATH: an ELF file, or a folder containing .elf files.
• SAMVA_CONFIG_PATH: a SAMVA configuration file, or a folder containing configuration files.

Main options are:

• --result_folder to choose where results are stored. By default, they are stored in samva_results folder.
• --fault_model to define the fault model. Options are TrueNOP for traditional instruction skip, and Replay for word replay.
• --fault_parameters to define the attacker capacities: the minimum and maximum fault widths, and the minimum distance between two faults.
• --max_paths_per_segment, --max_cost_per_segment, --max_cost_for_simulation, and --max_attack_paths to limit the search and evaluation effort.
• --evaluator (unicorn, gem5, or none) and --log_variable for simulation and logging.
• --hardware_injector, --hardware_injector_port, --hardware_target, and --hardware_target_port to conduct physical attacks.
• --timeout, --stop_at_robustness, and --verbose for execution control and debugging.

Run the following command for the full option list: uv run samva evaluate --help.

Configuration file

To analys a binary, SAMVA requires a configuration file describing the attacker objectives (which program locations must be reached or avoided) and the simulation validation criteria (initial and final states). A program location can be a single instruction, a basic block or a whole function. An example is shown and all the fields are explained below.

The configuration file is sensitive to address layout. If a program is recompiled, the configuration may require updates to match the new addresses.

{
  "starting_point": "func",
  "attack_script": [
    { "target": "instruction", "address": "func+0x8A" },
    { "target": "instruction", "address": "func+0x96", "policy": "execute" }
  ],
  "attack_points": [
    { "target": "instruction", "address": "0xDEADBEEF" },
    { "target": "block", "address": "func+0x10" },
    { "target": "function", "address": "func" }
  ],
  "global_avoid": [
    { "target": "block", "address": "func+0x20" }
  ],
  "forced_types": [
    { "target": "instruction", "address": "func+0x30", "type": "neutral" },
    { "target": "instruction", "address": "func+0x32", "type": "execute" },
    { "target": "instruction", "address": "func+0x34", "type": "skip" }
  ],
  "simulation": {
    "memory_map": [
      { "name": "db", "address": "0x80001000", "size": 4096 },
      { "name": ".stack", "address": "0x01002000", "size": 4096 }
    ],
    "initial_state": [
      { "symbol": "var_a", "size": 1, "value": 1 },
      { "symbol": "var_b", "size": 1, "value": 2 }
    ],
    "final_state": [
      { "symbol": "var_c", "size": 1, "value": 3 }
    ]
  }
}

Fields for SAMVA configuration file:

• starting_point: address or name of the block where the control-flow analysis begins. SAMVA assumes that the control flow does not need to be hijacked to reach this block.
• attack_script: ordered list of code locations and their associated policy. The policy indicates whether the code section must be executed or skipped to realize the exploit.
• attack_points (will be deprecated in future release): Specify, in order, which code locations must be reached during the attack. target indicates if the location is a block or an instruction. The address can be defined as a hex address (e.g. 0xCAFE) or relative with the beginning of another block of function, such as illustrated in the example. This parameter is replaced by attack_script parameter.
• global_avoid: (Optional) code locations that must be avoided during the attack.
• forced_types: (Optional) force the type of specific code locations when SAMVA is too pessimistic, especially on conditional jumps.
• simulation: (Optional) options related to simulation, used to validate the attack paths found by the analysis.
  • memory_map: extra memory sections to map during simulation, for example for embedded targets with I/O regions.
  • initial_state: expected values of program variables before starting the attack.
  • final_state: expected values of program variables after the attack, used for validation.

Development

Multiple tasks are prepared to facilitate development. We use ruff to lint and format the Python code, and sphinx to generate the documentation.

• Lint the whole project: uv run task lint
• Format every project file according to the defined style: uv run task format

Examples

Two PIN code verification programs are attacked in the example folder. Learn more about SAMVA application on the related documentation.