aboutsummaryrefslogtreecommitdiff

       +=-------------------------------------------=+
       | finja: fault injection analysis             |
       | <https://pablo.rauzy.name/sensi/finja.html> |
       +=-------------------------------------------=+

The finja (Fault INJection Analysis) tool is being developed as
part of my PhD work. It helps me to formally analyse some kinds
of fault injection attacks and countermeasures against them. It
uses modular arithmetic as a framework since it was first
developped to analyse BellCoRe attacks on CRT-RSA computations.

The name "finja" is awesome because it resembles "ninja".


INTSALL
=======

- finja depends on:

  - OCaml <https://www.ocaml.org/> 3.12.1+
  - Batteries <http://batteries.forge.ocamlcore.org/> 2.1+
  - menhir <http://gallium.inria.fr/~fpottier/menhir/>
  - Sexplib <https://github.com/janestreet/sexplib> (upto 113.00.00)

  These dependencies can be easily installed using the OCaml
  Package Manager, OPAM <https://opam.ocaml.org/>, with:

    opam install batteries menhir sexplib.113.00.00

- Once the dependencies are installed, compile finja with:

    ocamlbuild -use-ocamlfind finja.native


USAGE
=====

- Command line options:

  finja [options] <input-file>
    -o <output-file> HTML report (defaults to input-file.html)
    -l Only check syntax
    -a Only simplify the input term (no attacks)
    -s Print only successful attacks in the html report
    -t Enable transient faults (default is only permanent fault)
    -r Inject randomizing fault (default)
    -z Inject zeroing fault
    -n Specify the number of faults (default is 1).
       If specified, you can use the -r or -z option for each
       fault (last one is repeated).

- Input file formats:

  Input files are text files (which use the .fia extension by
  convention) which first contain a description of the
  computation term to analyze, then a line with a single '%%'
  symbol, then an attack success condition.

  The BNF of the syntax is given below.

    fia     ::= term '%%' cond
    term    ::= ( stmt )* 'return' mp_expr ';'
    stmt    ::= ( decl | assign | verif ) ';'
    decl    ::= 'noprop' mp_var ( ',' mp_var )*
              | 'prime' mp_var ( ',' mp_var )*
    assign  ::= var ':=' mp_expr
    verif   ::= 'if' mp_cond 'abort with' mp_expr
    mp_expr ::= '{' expr '}' | expr
    expr    ::= '(' mp_expr ')'
              | '0' | '1' | var
              | '-' mp_expr
              | mp_expr '+' mp_expr
              | mp_expr '-' mp_expr
              | mp_expr '*' mp_expr
              | mp_expr '^' mp_expr
              | mp_expr 'mod' mp_expr
    mp_cond ::= '{' cond '}' | cond
    cond    ::= '(' mp_cond ')'
              | mp_expr '=' mp_expr
              | mp_expr '!=' mp_expr
              | mp_expr '=[' mp_expr ']' mp_expr
              | mp_expr '!=[' mp_expr ']' mp_expr
              | mp_cond '/\' mp_cond
              | mp_cond '\/' mp_cond
    mp_var  ::= '{' var '}' | var
    var     ::= [a-zA-Z][a-zA-Z0-9_']*

  The "mp" in "mp_var", "mp_expr" and "mp_cond" stands for
  "maybe protected". A variable name at declaration time, an
  expression, or a condition surrounded by "{" and "}" can't be
  faulted.

  The attack success condition can use all the variables
  introduced in the computation term, plus two special variables
  "_" and "@" which respectively represent the returned
  expression of the computation term as given in the input file,
  and the returned expression of the computation term with
  injected faults.

  Examples of input files can be found in the "tests" directory.

Pablo Rauzy — generated by cgit