Lazart : Laser Attack and Robustness
Lazart is a tool based on concolic
execution that evaluates the robustness of LLVM code
against multi- fault attacks.
Lazart is an academic project developed at VERIMAG
laboratory, at the University of Grenoble-Alpes,
France. Its development has been supported by two
projects: the Sertif
project (project ANR-14-ASTR-0003-01) and The
FUI SecurIoT project (2017-2020).
Lazart is a high level tool targeting developers and auditors. It allows to identify vulnerable paths et could be used to evaluate the accuracy of countermeasures, relatively to a given faul model. The particularies of Lazart are the following ones :
- Lazart takes into account multi-faults, according to the state of the art in attacks. Multi-fault is also a way to encompass low-level attacks.
- Lazart is based on a (efficient) concolic engine, Klee, allowing to establish correctness results (relatively to a given fault model)
- Attacks scenarios characterizing successful
attacks are stated by assertions. Combining attack
scenarios and fault models give a flexible way to
evaluate codes and countermeasures.
3 fault models are supported:
- Test inversion (modification of the branch resulting on the evaluation f a condition). It is a very powerful fault model that encompasses several low-level fault models (nopping a JUMP, modifying a register, modifying the arget of a JMP ...)
- Modification of value that are read. This a
classical volatile data modification fault model.
Thanks to the symbolic engine, value can be chosen
- No execution of a call. This fault model corresponds to classical attacks where we try to not consider the result of a function (for instance a new random number)
We are currently developing a new version of Lazart allowing to efficently combine fault models and attacks scenarios.
Results on an example
Here is an example of verify-pin with attacks against authentication. We aim a maximum of 4 faults:
- the source code: Verify-pin2
- number of founded attacks : out.txt
- attacks scenarios:
fault_graph_appli_1_test_test000011.replay.pdf (with a single fault injection)
fault_graph_appli_1_test_test000012.replay.pdf (with a single fault injection)
fault_graph_appli_2_test_test000006.replay.pdf (with a double fault injection)
fault_graph_appli_4_test_test000017.replay.pdf (with four fault injections)
More examples can be found in the FISSC collection
Publications about Lazart:Marie-Laure Potet, Laurent Mounier, Maxime Puys and Louis Dureuil.
Lazart: a symbolic approach to evaluate the impact of fault injections by test inverting.
ICST 2014, International Conference on Software Testing.
Lionel Rivière and Marie-Laure Potet and Thanh-Ha Le
and Julien Bringer and Hervè Chabanne and Thanh-Ha Le
Maxime Puys. Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks. International Symposium on Foundations and Practice of Security, FPS 2014,
Lecture Notes in Computer Science.
FISSC: a Fault Injection and Simulation Secure Collection.
In International Conference on Computer Safety, Reliability and Security (SAFECOMP), 2016.
If you are interested for more information please contact Marie-Laure.Potet@univ-grenoble-alpes.fr