Overview/Tutorial-1:-Get-started-with-verify_pin-analysis.md

+[_Lazart documentation_](Home)
+
+This tutorial presents how to create a simple analysis with **Lazart**, how to describe the attack objectives, the fault model and run the analysis with the Python API. More detailed examples and concepts are presented in other sections.
+
+The following considers that you have a working installation of Lazart. The complete example analysis folder can be found in `use-cases/tutorial-1-2/` (in `/opt/lazart/` if you are running the docker container).
+
+Ìf you want to run the analysis directly, use `./analysis.py -r -o=4` (see [this section](#running-your-analysis)).
+
+**Summary**:
+
+- [An example function: `verify_pin`](#an-example-function-verify_pin)
+- [Instrumenting the code](#instrumenting-the-code)
+- [Creating the analysis script](#creating-the-analysis-script)
+- [Running your analysis](#running-your-analysis)
+- [Going Further](#going-further)
+
+# An example function: `verify_pin`
+
+We will test an example function `verify_pin` which corresponds to the verification of an user PIN (see the [FISSC collection](https://lazart.gricad-pages.univ-grenoble-alpes.fr/fissc/)). Here is the content of the file _verify_pin.c_ :
+
+```c
+// verify_pin.c
+#include "verify_pin.h"
+#include "lazart.h"
+
+sec_bool_t compare(uint8_t* a1, uint8_t* a2, uint8_t size)
+{
+    int result = TRUE;
+
+    for (int i = 0; i < size; i++) {
+        if (a1[i] != a2[i]) {
+            result = FALSE;
+        }
+    }
+
+    return result;
+}
+
+bool verify_pin(uint8_t* user_pin, uint8_t* card_pin)
+{
+    if(try_counter > 0) {
+        if (compare(user_pin, card_pin, PIN_SIZE) == TRUE) {
+            // Authentication
+            try_counter = TRY_COUNT;
+            return true;
+        } else {
+            try_counter--;
+            return false;
+        }
+    }
+
+    return false;
+}
+```
+
+The `verify_pin` function first verifies the `try_counter`, representing the remaining tries for the user (`TRY_COUNT` is 3).
+Then, it compares the `user_pin` array to the `card_pin`. If the comparison (performed in the `compare` function) is successful, the function returns `true`, otherwise it returns `false`.
+
+The `compare` function performs the comparison of the two array in constant time and returns a `sec_bool_t`, corresponding to hardened booleans using `uint8_t` value with high hamming distance (`TRUE` is `0xAA` and `FALSE` is `Ox55`).
+
+We define here the _attack objectives_ to be authenticated with an incorrect PIN or to not decrement the try counter.
+
+In this example, we will use the _test inversion_ fault model, allowing the attacker to inject faults inverting the result of a test (conditional branch at LLVM level) at any time in the considered functions (̀`verify_pin` and `compare`).
+
+The following file corresponds to _verify_pin.h_, containing defines and includes for the analysis.
+
+_note_: `lazart.h` does include several files by defaults, such as `<stdio.h>`, `<stdbool.h>`, `<stdint.h>` and `<klee/klee.h>` (unless the macro `_LZ__NO_STD` is defined).
+
+```c
+// verify_pin.h
+#pragma once
+
+#ifndef VERIFY_PIN_H
+#define VERIFY_PIN_H
+
+#include <lazart.h>
+
+typedef int sec_bool_;
+typedef enum { TRUE = 0xAA,
+    FALSE = 0x55 } sec_bool_t;
+
+#define PIN_SIZE 4
+#define TRY_COUNT 3
+
+extern int authenticated;
+extern int try_counter;
+
+bool verify_pin(uint8_t* user_pin, uint8_t* card_pin);
+
+#endif
+```
+
+# Instrumenting the code
+
+The first step will consist in instrumenting the code to have a program exploitable by **Lazart**. For more information, please consult the [attack model](Attack-Model#description-with-instrumentation) and [attack objective](Core/Attack-objective) sections.
+
+Create a _main.c_ file corresponding to the entry point of the analysis, and put all source files (_verify_pin.c_, _verify_pin.h_ and _main.c_) in a _src_ subfolder. 
+
+_main.c_ will contain a `main` function to initialize the inputs and define our _attack objectives_:
+
+```c
+#include "lazart.h"
+#include "verify_pin.h"
+
+int try_counter;
+
+void initialize(uint8_t* user_pin, uint8_t* card_pin)
+{
+    try_counter = TRY_COUNT;
+    // card PIN = 1 2 3 4...
+    for (int i = 0; i < PIN_SIZE; ++i)
+        card_pin[i] = i + 1;
+    // user PIN = 0 0 0 0...
+    for (int i = 0; i < PIN_SIZE; ++i)
+        user_pin[i] = 0;
+}
+
+
+bool oracle(bool ret) { return ret | (try_counter >= TRY_COUNT); }
+
+int main()
+{
+    // Initialize entries.
+    uint8_t user_pin[PIN_SIZE];
+    uint8_t card_pin[PIN_SIZE];
+    initialize(user_pin, card_pin);
+    
+    bool ret = verify_pin(user_pin, card_pin); // Run studied program.
+    _LZ__ORACLE(oracle(ret)); // Attack success predicate.
+
+    return 0;
+}
+```
+
+Our main function is separated into three steps : initialization, call of the studied function and the attack objective's oracle.
+
+The `initialize` function sets the `try_counter` to `TRY_COUNT` and uses fixed values for `card_pin` and `user_pin`, respectively [0, 0, 0, 0] and [1, 2, 3, 4]. 
+
+_note: **Lazart** supports symbolic input for the analysis._ For more information, please check [tutorial 2](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy).
+
+After initialization, the studied function `verify_pin` is called, and the attack objective is specified using the macro [`_LZ__ORACLE`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/cpp-api/df/d42/lazart_8h.html) (included in `"lazart.h"`), taking a boolean predicate in parameter. With other words, all execution paths in which the predicate is unsatisfied will be excluded from the list of attacks generated by Lazart. Thus, the attack objective can be described using several calls to [`_LZ__ORACLE`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/cpp-api/df/d42/lazart_8h.html)).
+
+_note: [`_LZ__ORACLE`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/cpp-api/df/d42/lazart_8h.html) use internally the function `klee_assume` and should thus be avoid court-circuiting operation inside the evaluation of the predicate (see KLEE's tutorial [here](https://klee.github.io/tutorials/testing-regex/)).
+
+# Creating the analysis script
+
+We are done with instrumentation, the last step is the analysis script using the **Lazart Python API**. 
+
+**_note:_** _in the current version, running analysis will remove_ `.bc` and `.strat` files in the folder of the script.
+
+```python
+#!/usr/bin/python3
+
+from lazart.lazart import *
+
+# Parse CLI parameters
+params = install_script()
+
+# Create analysis or load from path if available
+a = read_or_make(["src/verify_pin.c", "src/main.c"], # Source files
+    functions_list(["verify_pin", "compare"], ti_model()), # Attack model: test inversion for the two specified function 
+    path="results", # Pass in which analysis file will be stored
+    flags=AnalysisFlag.AttackAnalysis, # Attack analysis (default)
+    compiler_args="-Wall", # Compiler arguments
+    params=params, # Pass CLI params to the analysis
+    klee_args=""
+)
+
+execute(a) # Execute analysis, print results and generate report
+
+verify.attack_analysis(a)
+verify.traces_parsing(a)
+```
+
+This script first declares itself as python executable script (line 1) and imports the _Python API_ with `from lazart.lazart import *`. This module of the Lazart package is a convenience module containing all primitives usually used in an analysis script. Each module can also be imported separately.
+
+The [`lazart.script.install_script`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.install_script) function, exported to global namespace by the previous import, allows your script to have an unified arguments management. It provides some generic arguments (such as verbosity choices, faults limit selection or output folder specification for instance). Use the `-h` option with your script to see the available options (if you need a custom option parser, see [`lazart.lazart.get_parser`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.get_parser)). [`install_script`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.install_script) returns a namespace object containing command line parameters.
+
+The analysis object, named `a`, is created through the [`lazart.io.read_or_make`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.io.html#lazart.core.io.read_or_make) function. This object is of type [`lazart.analysis.Analysis`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.analysis.html#lazart.core.analysis.Analysis) and contains all parameters required to run any analysis in Lazart (see the [dedicated section](Analysis)).
+
+[`read_or_make`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.io.html#lazart.core.io.read_or_make) enables caching features and will try to read existing cache before running again the analysis, avoiding making the analysis computation at execution. When you need to recompute the results, use the `-r` (recompute all) or `-R=step` (restart at specific step) command-line option with your script (provided by [`install_script`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.install_script)).
+
+Let's take a look at the analysis parameters. The full list is available in the [Analysis constructor documentation](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.analysis.html#lazart.core.analysis.Analysis).
+
+Two arguments are required: the input files of the program and the attack model. The input file  is the list of each file path. You can also use the Python's `glob` package to open all source file in a folder (`glob.glob("src/*.c")`).
+
+The second argument is the attack model, it contains a specification of the fault that can be applied by the attacker. In this case, the [`functions_list(fcts, models)`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.attack_model.html#lazart.core.attack_model.functions_list) function creates an attack model in which a list of models is applied on each specified function. More complex attack models can be defined, see the [tutorial 3](Overview/Tutorial-3:-Data-Load-and-model-combination-on-memcmps) and [attack model section](Attack-Model). 
+
+Several optional parameters can be specified. The `max_order` argument specifies the fault limit of the analysis (default to 2). The `params` parameter accepts the [`install_script`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.install_script) argument namespace overriding some argument depending on the CLI, for instance `max_order` will be set by `params` if the option `--order` (`-o`) is specified.
+The `path` argument specifies in which folder the analysis files will be generated. It's often better to have your analysis files in a subfolder to separate the analysis script. If not specified, an auto-generated fresh folder name is used. Additionally, `compiler_args` allows to specify additional arguments to the compiler and `klee_args`allows to give parameters to KLEE.
+
+The analysis `flags` determines which analyses are possible. Use [`AttackAnalysis`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.analysis.html#lazart.core.analysis.AnalysisFlag.AttackAnalysis) (default) for attack analysis. [`execute`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.util.exec.html#lazart.util.exec.execute) function performs all the operations required for the analysis. This function behaves differently depending on the analysis's flags. For attack analysis, the call to [`execute`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.util.exec.html#lazart.util.exec.execute) will be roughly equivalent to the following code:
+
+```python
+compile(a) # Compilation + preprocessing
+run(a) # Mutation and DSE.
+traces_results(a) # Gathering traces information.
+attacks_results(a) # Computing attacks.
+hotspot_results(a) # Computing hotspots.
+
+print(a) # Prints results
+```
+
+All analysis steps (*compilation*, *DSE*, *trace parsing*, *analysis* ...) use a cache internally, making the computations to occur only one time, even if the script is executed again. You can use the `-r` option on the analysis script to force an analysis to restart completely or `-R` to restart from a specific step.
+
+The module [`lazart.verify`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.util.verify.html#module-lazart.util.verify) contains utility functions which are used to check basic errors in an analysis. In this example we call `verify.attack_analysis` and `verify.traces_parsing(a)`. Thoses function show a message if abnormal results are found (for instance 0-faults attacks).
+
+# Running your analysis
+
+You can now try your analysis by simply execute your script:
+
+```console
+root@lazart:/opt/lazart/use-cases/examples/get-started# ./analysis.py -r -o=4 -V=quiet
+Mutation file parsing ended. 0 warning(s) and 0 error(s) generated.
+mutation ended. 0 warning(s) and 0 error(s) generated.
+module clean.
+module saved.
+                                                                                               
+Program:                                                                                       Full attacks results
++---------+--------+-------+-------+--------+                                                  +-----------+------+------+------+------+------+---------+
+| Name    |   Ins. |   BRs |   IPs |   Dets |                                                  | Attacks   |   0F |   1F |   2F |   3F |   4F |   Total |
+|---------+--------+-------+-------+--------|                                                  |-----------+------+------+------+------+------+---------|
+| unammed |    468 |    18 |     4 |      0 |                                                  | atk:      |    0 |    3 |    8 |   12 |    9 |      32 |
++---------+--------+-------+-------+--------+                                                  +-----------+------+------+------+------+------+---------+
+                                                                                               
+Attacks analysis:                                                                              Execution:
++-----------+------+------+------+------+------+---------+                                     +-------+------+-------+------+------+------+------+
+| Attacks   |   0F |   1F |   2F |   3F |   4F |   Total |                                     |   Trs |   PP |   IgT |   KT |   CP |   EP |   EI |
+|-----------+------+------+------+------+------+---------|                                     |-------+------+-------+------+------+------+------|
+| atk:      |    0 |    3 |    8 |   12 |    9 |      32 |                                     |    32 |   44 |     2 |   34 |   32 |   76 | 8012 |
++-----------+------+------+------+------+------+---------+                                     +-------+------+-------+------+------+------+------+
+                                                                                               
+Hotspots:                                                                                      Time metrics:
++---------+-------------------+-----------+-----------+-----------+-----------+-----------+    +-------+-------+--------+-------+------+
+|   Order | Info              |   0-order | 1-order   | 2-order   | 3-order   | 4-order   |    |    TT |   TLz |   TDSE |   TTr |   TA |
+|      IP |                   |           |           |           |           |           |    |-------+-------+--------+-------+------|
+|---------+-------------------+-----------+-----------+-----------+-----------+-----------|    | 0.178 | 0.064 |   0.08 | 0.058 |    0 |
+|       0 | ti [l:9, bb:bb1]  |         0 | 1 (mc:1)  | 4 (mc:1)  | 6 (mc:1)  | 4 (mc:1)  |    +-------+-------+--------+-------+------+
+|       1 | ti [l:10, bb:bb2] |         0 | 0         | 5 (mc:1)  | 19 (mc:2) | 25 (mc:4) |    
+|       2 | ti [l:20, bb:bb7] |         0 | 1 (mc:1)  | 0         | 0         | 0         |    Coverage:
+|       3 | ti [l:21, bb:bb8] |         0 | 1 (mc:1)  | 7 (mc:1)  | 11 (mc:1) | 7 (mc:1)  |    +-----+-----------+-----------+-------+-------+-------+
++---------+-------------------+-----------+-----------+-----------+-----------+-----------+    | S   |   ICov(%) |   BCov(%) | ITr   |   FBr |   PBr |
+                                                                                               |-----+-----------+-----------+-------+-------+-------|
+                                                                                               | ok  |     97.86 |     88.89 | err   |    14 |     4 |
+                                                                                               +-----+-----------+-----------+-------+-------+-------+
+verify: attacks tests passed
+verify: traces tests passed
+root@lazart:/opt/lazart/use-cases/examples/get-started/# 
+```
+In this example, the analysis was run with quiet verbosity mode (`-V=quiet`), forcing the re-computation of each step despite the cache (-r). The fault limit was set to 4 in the CLI (`-o=4`), which was forwarded with the (`params` argument of [`read_or_make`](https://lazart.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.io.html#lazart.io.read_or_make)).
+
+All results are stored inside the analysis folder, named `results` (specified in the `path` field in `read_or_make`). Lazart produces several results tables:
+- Program: static information about the program: total LLVM instructions (*Instr.*), total branches (*BRs*), total injection points (*IPs*) and detectors count (*Dets*, only used in countermeasures analysis).
+- Attack Analysis: the number of attacks for each order (up to 4 here) and the total number of attacks. 
+- Full attacks results: extended table of attack analysis for redundancy and equivalence analysis (see [tutorial 2](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy)).
+- Execution: execution metrics of the analysis: traces generated (*Traces*), partial paths (*PP*), ignored ktests (*IgT*), total ktests (*KT*), completed paths (*CP*), explored paths (*EP*) and total executed LLVM instructions (*EI*).
+- Time metrics: total time (*TT*), total lazart time (*TLz*), total DSE duration (*TDSE*), traces parsing duration (*TTr*) and total analysis duration (*TA*).
+- Coverage: instruction and basic blocs coverage (*ICov(%)* and *BCov(%)*), incomplete traces (*ITr*), full branches (*FBr*) and partial branches (*PBr*). 
+- Hotspots analysis results: providing information about injection points (see the [dedicated section](Analysis/Hotspot-Analysis)).
+
+**Lazart** will generate an _analysis report_ in the analysis folder. You can find the report of this analysis [here](https://gricad-gitlab.univ-grenoble-alpes.fr/lazart/lazart/-/raw/master/use-cases/examples/get-started/results/report.md).
+
+The complete results CSV file can be found inside the `res.csv` file in the analysis folder, the `results` binary file contains the `Metric` object for the Analysis. The analysis folder structure is presented [here](Analysis#analysis-folder-structure).
+
+# Going further
+
+You have done your first analysis with **Lazart**. [Tutorial 2: Symbolic Inputs, Equivalence and Redundancy](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy) shows how to use symbolic input with Lazart. [Tutorial 3 on ](Overview/Tutorial-3:-Data-Load-and-model-combination-on-memcmps)`memcmps` presents the [Data Load (DL)](Attack-Model/Data-Load-(DL)-Fault-Model) model and model combination on `memcmps3` example.
+
+For more information about analysis scripts and Lazart tools and environement, see [this section](Environment).
+
+The **[Python API](/lazart/lazart/-/wikis/Core/Analysis)** contains features for manipulating *analysis*, *traces*, *attacks*, *faults* etc. You can write much more complex scripts and your own analysis.
+
+If you want to contribute to this project, please consult the **[corresponding guide](/lazart/lazart/-/wikis/Dev/Devlopment-Resources)**.
+
+***note:*** *This wiki is still under development and some sections are not written for now.*
\ No newline at end of file