Lazart : Laser Attack and Robustness

Lazart is a tool based on concolic execution that evaluates the robustness of LLVM code against multi- fault attacks.

                                            

                                        Grenoble alpes
                    cybersecurity Software vulnerabilities

                                                                                       

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 by Lazart.
  • 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 and
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.

L. Dureuil, G. Petiot, M.-L. Potet, T.-H. Le, A. Crohen, Ph. de Choudens.
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