Documentation

In the following, documentation for the available transformation passes and the necessary steps to analyze an executable are given. Please consider the examples in the testeval directories as well. A number of verified gadgets have been published in a separate repository which can serve as blueprint. Please be warned: this academic prototype can easily be applied incorrectly, leading to erroneous conclusions, e.g. due to incorrect or incomplete annotations, missing transformations or leakage annotations. It is good practice to check the configuration and verification results by deliberately causing leakage and inspecting the output of partial evaluation using the print command described below.

Commands and Transformations

Analysis script for scVerif are developed in two environments, a mode for specifying programs, state and annotations (IL mode) and a separate mode for instructing the framework to analyze programs (SCV commands). The default environment is IL when running in interactive mode scverif -i or passing files via scverif --il <file>.

IL commands

The language for specifying gadgets is described in our paper. The following IL commands are supported:

include

To include IL, GAS (gnu assembler) or ASM objdump files at point. Support for GAS is limited, e.g. branching, as the instruction addresses are not available.

include il "models/leakyisa-cortex-m0plus.il"
include asm "testasm/secmult-cortex-m0plus-O3.objdump"
include gas "gnu-unified-assembler.s"

var

For declaring (typed) global variables. Possible types are bool, w8, (eight bits), w16, w32, w64, int (signed integers), uint (unsigned integers). Arrays of a specific type are declared by appending a range [start:end] where the integer “start” must be less or equal to “end”, bounds are inclusive. Global memory is declared by an identifier without type and empty square brackets <name>[].

<type> <varname>;

w32 r0;
int loopcounter;
bool flagOne;
memory[];
w32 table[-1:20];

macro

Macros are globally available functionality with typed parameters and local variables. These are not “functions”, i.e. variables outside the scope can be accessed and parameters passed when calling macros can be changed by the called macro.

macro <name> (<type> <paramname1>, <type> <paramname2>, ...)
  <type> <localvariablename1>, <type> <localvariablename2>
{
  <instruction>;
}

macro noOperation () {}

macro mult (w32 a, w32 b)
  label loopstart
{
  loopstart:            // definition of label
  a <- a +w32 a;        // leakage free assignment, "+w32" addition of w32-typed variables
  leak(a, b);           // explicit leakage of a and b separately

  if (b != ((w32) 0)) { // "(w32) 0" is a cast of integer to w32
    goto loopstart;
  }
}

IL instructions

A number of instructions are available in IL:

If conditional

Conditionals are available with optional false case.

if (<expr>) {
  <instruction>;
}

if (<expr>) {
  <instruction>;
} else {
  <instruction>
}

Loop

Conditional while.

while (<expr>) {
  <instruction>
}

Do-While variant

while {<instruction>} (<expr>)

IL expressions

A number of expressions can be used:

Unary operations

Binary operations

annotate

The IL command annotate is used to specify an initial state and input/output behavior of a macro which is subsequently used by partial evaluation and verification of side-channel resilience.

Four kinds of annotations for state and memory can be made:

  1. Memory regions within a specific memory, declaring names of the regions at the same time.
  2. Inputs and outputs
  3. Initialization of state
  4. Security type (secret independent (public), masked (sharing), uniform random (urandom) and secret dependent (secret))

An example annotation is provided below:

annotate examplegadget
  region mem w32 stack[0:10]       // memory "mem" contains a "stack" area of 11 positions with w32 type
  region mem w32 inpt[0:3]         // "mem" contains 4 input words in a region called "inpt"
  region mem w32 outpt[0:1]
  region mem w32 entropy[0:1]
  init metric_cyclecount 0         // specific value
  init r0 [inpt 0]                 // r0 is a pointer to region "inpt" at offset 0
  init r1 [outpt 0]
  init r2 [entropy 0]
  init r4 w32 0x1234               // set r4 to a specific value, this can also be done for arrays [w32 1, w32 2, ...]
  init sp [stack 0]
  input public r0                  // r0 is a secret independent input to "examplegadget"
  input public r1                  // input annotations cannot be checked for correctness by scVerif, be careful.
  input public r2
  input public stack               // values in the "stack" region are secret independet inputs
  input sharing ina [in[0:1]]      // the masked input "ina" is a subpart of the "in" region
  input sharing inb [in[2], in[3]] // a list of subparts is possible
  output public in                 // the entire region "in" must be secret independent (scrubbed) after execution
  output sharing out outpt[0:1]    // the output named "out" is located in region "outpt" and contains 2 secret shares
  output secret stack              // values in the "stack" region are allowed to be secret outputs
  output public r0                 // r0 must be secret independent after execution
  input urandom entropy            // the region "entropy" contains randomness sampled from uniform
  ;

Incorrect annotations can quickly lead to invalid verification results, e.g. providing initial values for secret shares.

Comments

// can be used for line-comments and /* to */ for commented regions.

SCV Commands

The scv mode is entered via --- and exited with ..., similar to YAML. In general the scv commands are build from dictionaries and lists. The top-level command must always be a dictionary with an identifier corresponding to the transformation or action to be applied.

The following SCV commands are available:

verbosity

The comand verbosity allows to suppress the output of transformations or increase their verbosity.

verbosity:          // set the verbosity of scVerif
  verbosity: 3;     0 = off, 1 = normal, 2 = debug, 3 = full

print

Multiple intermediates of scVerif can be printed to stdout at various points in the analysis.

  1. “macrodef” for definitions of macros
  2. “globals” for global variables
  3. “state” for variable values in the state of the partial evaluator
  4. “initials” for macro annotations
  5. “evaltrace” for the IL trace resulting from partial evaluation
  6. “maskverif” for a program which reminds of the maskverif language but is intended for debugging purposes only
print:
  kind: [macrodef]
  target: ["macro1", "macro2"]  // target: "macro*"  for simple pattern matching
  verbosity: 1;

addleakage

Augments a program with leakage by adding (prepending) a call to <macroname>_leak(a, b, c) whenever encountering <macroname>(a, b, c). Must be called before inlinecall.

addleakage:
  target: "*";

inlinecall

Inlines all calls to macros to enable partial evaluation.

inlinecall:
  target: "*";

partialeval

Perform the partial evaluation according to the specified annotations.

partialeval:
  target: [secxor];

filter

Ability to filter out leakages selectively, applied to the evaluated trace, i.e., after partial evaluation.

To remove all leakages which do not contain “CompResult” in their name:

filterleak:
  inverse: true            // remove all but matching leakage
  leaks: "*CompResult*"
  target: [secxor];

To remove only leakages which contain “OperandEffect” in their name:

filterleak:
  inverse: false           // remove all matching leakage
  leaks: "*OperandEffect*"
  target: [secxor];

It is a good idea to check the outcome with print statements and ensure a consistent naming of leakages in the models.

infertaint

Automated transformation to add annotations for variables which have not been annotated so far, often required for verification. The transformation does not alter (i.e. overwrite) existing annotations.

infertaint:
  inputsAsPublic: true       // whether the verification should assume inputs to be secret independent
  outputsAsPublic: true      // whether all outputs should be secret independent after execution
  memoryAsPublicOut: true    // whether all memory should be secret independent after execution
  target: [secxor];

check

Finally, the goal of analysis is to verify notions of security.

check:
  kind: "Stateful SNI"          // alternatively "Stateful NI"
  target: [secand];

Analyzing an executable

The common process to analyze an executable is to include an execution model, a leakage model, the program code (GAS, objdump, IL), specify an annotation (annotate) and subsequently switch to SCV mode using ---. Using addleakage the leakage is added to the execution model and the program. For further analysis the program has to be flattened using inlinecall on the program to be analyzed. If an annotation was given the partialeval pass produces an evaluated trace of the program which needs to be annotated with filterleak and can finally be analyzed by the check pass.

Troubleshooting

Evaluation

Sometimes it is necessary to adopt the bounds of arrays and memory regions, e.g. stack size: The error message eval_load region out of bound (stack:[-1:-1]) [-5] means that the memory region stack is accessed at position -5, the initial position is defined in an annotation, e.g. init sp [stack 0].

The partial evaluator has a limited set of rules to evaluate a program representation. eval_mem_index: cannot evaluate pointer _ in (int) address means that a memory access was performed which cannot be evaluated since the address is an unknown (_) pointer. Above the error message a trace of the so far executed program is displayed, which usually helps to find the location causing trouble. Further up, more information, such as the current state (content of all variables) is displayed as well (_ means unknown value) which can for example arise when performing pointer arithmetic which is not always possible since addresses are represented with symbols to memory regions.

Verification

Successful verification displays a statement like “xorOrder1 is NI at order 1”. It is a good idea to check the validity of this message by (1) reading trough the entire output and react to warnings displayed there (2) review the annotations (3) review filterleak transformations and (4) check the sensitivity of verification by changing the model and implementation to cause leakage.

The error message Cannot check indicates that maskVerif was not able to simulate a set of probed leakages. In the error message the selected probes are given, in below case two probes are placed; first, the output a[0] (SNI output probe) and, second, the intermediate explicit leakage “strMemOperand” which allows to observe the leakage state opW, containing share a0 xor’ed with randomness ($) rnd1, and register r0, containing a1 ^ r1. It can be cleared by inserting a dummy instruction (e.g. storing a secret independent value) before the causing instruction at testasm/secref-cortex-m0plus-O3.objdump line 13, as indicated next to the probe. Mitigation depends on the used leakage model. For the provided model more intuition is given in the paper.

$ scverif --il testeval/secref-cortex-m0plus.il
Start checking of ki = 0, ko = 2                            // checking with ki = 0 internal, and ko = 2 output probes
1 list to process
3 tuples to check
3 tuples checked
Checking of ki = 0, ko = 2 done                             // check was successful
Start checking of ki = 1, ko = 1                            // checking with 1 internal and one output probe
3 list to process
54 tuples to check
r = $rnd[1]; p = a.[0]/a[0]/#
r = $rnd[2]; p = $rnd[1]#
No rnd rule
Cannot check                                                // Simulation failed, error state is given below
probe on
  (* output a[0] *)                                         // this is a probe on output a0 at the cost of one probe; 
  a.[0]/a[0]/ ^w32 $rnd[1] ^w32 $rnd[2]                     // this is the expression probed, $<var> means random.

probe on                                                    // a second probe with complete origin given
  (* models/leakyisa-cortex-m0plus.il: line 56 (2-32)
     leak strMemOperand(opW, r0) at testasm/secref-cortex-m0plus-O3.objdump: line 13 (2) to line 14 (0)
models/leakyisa-cortex-m0plus.il: line 50 (0) to line 61 (1)
 *)
  (a.[0]/a[0]/ ^w32 $rnd[1], a.[1]/a[1]/ ^w32 $rnd[1])

reduce to                                                   // the resulting observation after rewriting and simplification in maskVerif consisting of two observations split by ","
a.[0]/a[0]/ ^w32 $rnd[1] ^w32 $rnd[2],
(a.[0]/a[0]/ ^w32 $rnd[1], a.[1]/a[1]/ ^w32 $rnd[1])

Verifying stateful notions usually requires to remove secret dependent residue in outputs annotated as public, these have to be simulated in addition to t intermediate and output probes, allowing more than t probes in total. probe on (* public output r0 *) ... may indicate that r0 contains secret dependent data despite being specified to be public, similar for other registers, leakage state and stack.

Please be aware that the language based verification approach of maskVerif allows for verification at higher orders and for relatively large programs, but is not free of false negatives.

Adopting a leakage model

Two possibilities exist to model side-channel behavior of programs using scVerif and IL. The leakage can be specified together with the semantic execution model as in isa/pseudoisa.il or the execution model is split from the leakage behavior as in isa/isa-cortex-m0plus.il and isa/leakyisa-cortex-m0plus.il. Latter requires to include the leakage with the addleakage pass. More detail is given in the paper referenced above.