Skip to content

Changes

Page history
Updated doc links. authored by etienne boespflug's avatar etienne boespflug
Hide whitespace changes
Inline Side-by-side
Overview/Tutorial-1:-Get-started-with-verify_pin-analysis.md
View page @ 00d01698
...@@ -138,9 +138,9 @@ The `initialize` function sets the `try_counter` to `TRY_COUNT` and uses fixed v ...@@ -138,9 +138,9 @@ The `initialize` function sets the `try_counter` to `TRY_COUNT` and uses fixed v
_note: **Lazart** supports symbolic input for the analysis._ For more information, please check [tutorial 2](Overview/Tutorial-2:-Symbolic-Inputs,-Equivalence-and-Redundancy). _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)). After initialization, the studied function `verify_pin` is called, and the attack objective is specified using the macro [`_LZ__ORACLE`](https://securitytools.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://securitytools.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/)). _note: [`_LZ__ORACLE`](https://securitytools.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 # Creating the analysis script
...@@ -174,22 +174,22 @@ verify.traces_parsing(a) ...@@ -174,22 +174,22 @@ 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. 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 [`lazart.script.install_script`](https://securitytools.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://securitytools.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.script.html#lazart.script.get_parser)). [`install_script`](https://securitytools.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)). The analysis object, named `a`, is created through the [`lazart.io.read_or_make`](https://securitytools.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://securitytools.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)). [`read_or_make`](https://securitytools.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://securitytools.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). Let's take a look at the analysis parameters. The full list is available in the [Analysis constructor documentation](https://securitytools.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")`). 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). 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://securitytools.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. 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://securitytools.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 `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: The analysis `flags` determines which analyses are possible. Use [`AttackAnalysis`](https://securitytools.gricad-pages.univ-grenoble-alpes.fr/lazart/python-api/lazart.core.analysis.html#lazart.core.analysis.AnalysisFlag.AttackAnalysis) (default) for attack analysis. [`execute`](https://securitytools.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://securitytools.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 ```python
compile(a) # Compilation + preprocessing compile(a) # Compilation + preprocessing
...@@ -203,7 +203,7 @@ print(a) # Prints results ...@@ -203,7 +203,7 @@ 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. 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). The module [`lazart.verify`](https://securitytools.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 # Running your analysis
...@@ -247,7 +247,7 @@ verify: attacks tests passed ...@@ -247,7 +247,7 @@ verify: attacks tests passed
verify: traces tests passed verify: traces tests passed
root@lazart:/opt/lazart/use-cases/examples/get-started/# 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)). 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://securitytools.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: 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). - 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).
......