|
|
|
<div>
|
|
|
|
|
|
|
|
{width="386" height="193"}
|
|
|
|
|
|
|
|
**Lazart** is an [**LLVM**](https://llvm.org/)-level robustness evaluation framework targeting multi-faults injection. It relies on **Dynamic-Symbolic Execution (DSE)** using [KLEE](https://klee.github.io/), to explore the attack paths depending on user-provided [**attack model**](Attack-Model) and [**attack objective**](Core/Attack-objective).
|
|
|
|
|
|
|
|
</div>This page is the index of Lazart wiki. It contains links to the main sections of the documentation, guides and tutorials.
|
|
|
|
|
|
|
|
## Overview
|
|
|
|
|
|
|
|
Lazart works with several steps described in the figure below:
|
|
|
|
|
|
|
|
1. **Preprocessing and compilation:** user describes the attack model and attack objectives in Python API and/or by instrumenting program.
|
|
|
|
2. **Mutation (Wolverine):** all possible _Injection Points_ (IP) (depending on the attack model) are added inside the LLVM-bytecode.
|
|
|
|
3. **DSE (KLEE)**: symbolic exploration of attacks path.
|
|
|
|
4. **Trace parsing**: conversion of KLEE's ktest files inside Lazart's [traces](Core/Traces).
|
|
|
|
5. **Analysis**: analysis steps, working with attacks traces.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
To get started with lazart, please consider the following guides and tutorials:
|
|
|
|
|
|
|
|
- [Install Lazart:](Environement/Install-Lazart) how to install Lazart using docker.
|
|
|
|
- [Tutorial 1:](Overview/Tutorial-1:-Get-started-with-verify_pin-analysis) Get started with `verify_pin` analysis.
|
|
|
|
- [Tutorial 2:](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy) Symbolic Inputs, equivalence and redundancy.
|
|
|
|
- [Tutorial 3:](Overview/Tutorial-3:-Data-Load-and-model-combination-on-memcmps) Data Load and modelcombination on memcmps.
|
|
|
|
- [~~Tutorial 4~~:](Overview/Tutorial-4:-Experimentations-automated-analysis-campaign-utilitary) Experimentation analysis campaigns utility.
|
|
|
|
- [Analysis page: ](Analysis)Description of analysis parameters and steps.
|
|
|
|
|
|
|
|
## Modules
|
|
|
|
|
|
|
|
**Lazart** is separated into several modules:
|
|
|
|
|
|
|
|
- [**Python API**](Analysis): the _Python API_ corresponds to the core of **Lazart**. It includes the user interface to define and run analysis, algorithms and results manipulation features. [documentation](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/index.html)
|
|
|
|
- [**Lazart CLI**](Environement): the command line interface is constituted of several utility commands for working with **Lazart** and _Lazart's docker_.
|
|
|
|
- [**Mutation Module**](Mutation/Wolverine): the mutation module, mainly compound of the tool **Wolverine**, works on _LLVM bytecode_ to generate mutated bytecodes embedding symbolic faults injection mechanism to be analyzed by a _concolic engine_ (_KLEE_). [documentation](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/wolverine/index.html)
|
|
|
|
- [**Instrumentation API**](Instrumentation/Instrumentation-API): the Instrumentation API is a small module of **Lazart** providing utility headers for instrumenting analyzed programs. [documentation](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/cpp-api/index.html)
|
|
|
|
- [**FISSC**](https://lazart.gricad-pages.univ-grenoble-alpes.fr/fissc/): the _Fault Injection and Simulation Secure Collection_ is not directly part of **Lazart**. However, this collection is also developped at **Verimag** and is heavily used as use case for fault injection and countermeasure analysis. For more information, please consult the FISSC's [home page](https://lazart.gricad-pages.univ-grenoble-alpes.fr/fissc/).
|
|
|
|
|
|
|
|
## Publication about Lazart
|
|
|
|
|
|
|
|
**2023**
|
|
|
|
|
|
|
|
* E. Boespflug, L. Mounier, M-L. Potet, A. Bouguern, "A compositional methodology to harden programs against multi-fault attacks" - _2023 Workshop on Fault Detection and Tolerance in Cryptography (FDTC)_, \[[PDF](https://hal.science/hal-04231496/document)\] \[[Slides](https://fdtc.deib.polimi.it/FDTC23/slides/FDTC2023-slides-1-3.pdf)\]
|
|
|
|
* E.Boespflug, "Tools for code and countermeasures analysis against multiple faults attacks" - _2023 PhD thesis (French),_ \[[PDF (FR)](https://github.com/EBoespflug/phd-thesis-manuscript-fr/blob/main/phd-thesis-manuscript-fr.pdf)\]
|
|
|
|
* G. Lacombe, D. Feliot, E. Boespflug and M-L. Potet, "Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities" - _2023_ _Journal of Cryptographic Engineering (JCE)_, pp. 1-18, \[[PDF](https://arxiv.org/pdf/2303.03999.pdf)\]
|
|
|
|
|
|
|
|
**2021**
|
|
|
|
|
|
|
|
* G. Lacombe, D. Feliot, E. Boespflug and M-L. Potet, "Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities" - _2021 PROOF Workshop_, \[[PDF](https://www.proofs-workshop.org/2021/papers/paper2.pdf)\]
|
|
|
|
|
|
|
|
**2020**
|
|
|
|
|
|
|
|
* E. Boespflug, C. Ene, L. Mounier and M-L. Potet, "Countermeasures Optimization in Multiple Fault-Injection Context" - _2020 Workshop on Fault Detection and Tolerance in Cryptography (FDTC),_ pp. 26-34, doi: 10.1109/FDTC51366.2020.00011. \[[Slides](https://fdtc.deib.polimi.it/FDTC20/shared/Boespflug.pdf)\]
|
|
|
|
|
|
|
|
**2014**
|
|
|
|
|
|
|
|
* M-L. Potet, L. Mounier, M. Puys, "Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections" - _22014 IEEE Seventh International Conference on Software Testing, Verification and Validation_ , doi: 10.1109/ICST.2014.34.
|
|
|
|
|
|
|
|
## More resources
|
|
|
|
|
|
|
|
- [Lazart Interactive](Environment/Lazart-Interactive)
|
|
|
|
- [Security property and oracle](Core/Attack-objective)
|
|
|
|
- [Traces in Lazart](Core/Traces)
|
|
|
|
- [Symbolics inputs](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy)
|
|
|
|
- [Analysis and results](Analysis)
|
|
|
|
- [Attacks model, fault space and fault models](Attack-model)
|
|
|
|
- [FAQ](Overview/Frequently-Asked-Questions-(FAQ)) |
|
|
\ No newline at end of file |
