Language

QUAIL features its own language for writing programs, which is a simple imperative language, with standard control flow statements, and with additional randomized procedures. The processor of the tool compiles the program written in this language into a simplified language that is briefly described at the end of this page.

Content of this page:

Syntax

The QUAIL tool takes as input programs written in a specific language whose syntax is described by the following grammar:

program := (declaration)* (statement)*
declaration := const_declaration | public_declaration | private_declaration
declaration := 'const' IDENTIFIER ':=' expression ';'
public_declaration := public_type var_type IDENTIFIER ';'
      | public_type var_type IDENTIFIER ':=' init_val ';'
public_type := 'public' | 'observable'
private_declaration := private_type var_type IDENTIFIER ';'
      | private_type var_type IDENTIFIER ':=' (init_interval)+ ';'
private_type := 'private' | 'secret'
var_type := INT | 'array[' expression ('..' expression)? ']' 'of' var_type
init_val := expression | '{' number_list '}'
number_list := expression (',' expression)*
init_interval := '[' expression ',' expression ']'
statement := assignment_st | return_st | random_st | while_st | for_st | if_st
assignment_st := 'assign' public_variable ':=' expression ';'
return_st := 'return' ';'
random_st := 'random' public_variable ':=' 'randombit' '(' FLOAT ')' ';'
      | 'random' public_variable ':=' 'random' '(' expression ',' expression ')' ';
while_st := 'while' '(' guard ')' 'do' (statement)* 'od'
for_st := 'for' '(' IDENTIFIER 'in' IDENTIFIER indices ')' 'do' (statement)* 'od'
if_st := if_case (elif_case)* (else_case)? 'fi'
if_case := 'if' '(' guard ')' 'then' (statement)*
else_case := 'else' (statement)*
elif_case := 'elif' '(' guard ')' 'then' (statement)*
guard := leaf_term comp_operator expression
comp_operator := '<=' | '>=' | '>' | '<' | '==' | '!='
expression := expression binary_operator expression | unary_expression
binary_operator := '||'|'&&'|'^'|'+'|'-'|'*'|'/'|'%'
unary_expression := unary_operator term | term
unary_operator := '!'|'-'
term := '(' expression ')' | public_variable | NUMBER
leaf_term := NUMBER | IDENTIFIER (index)*
public_variable := IDENTIFIER (index)*
index := '[' expression ']'

The lexical terms of the grammar are:

INT := 'int''0'..'9'+
IDENTIFIER := ('a'..'z'|'A'..'Z'|'_')('a'..'z'|'A'..'Z'|'0'..'9'|'_')*
NUMBER := '0'..'9'+
FLOAT := '0''.'('0'..'9')+

The keywords of the language are: const, public, observable, private, secret, array, of, int, return, assign, random, randombit, if, elif, else, fi, then, while, for, do, od.

Comments in the program starts with //. Then the rest of the line is ignored.

Variable declarations

  • All variables must be declared at the beginning of the program, before any statement.
  • All variables are integers or arrays of integers. The type of integer is declared like int4 for a 4 bits integer.
  • Constants can be used with the following declaration:

    const N := [expr];

    where expr is any valid expression from the syntax, provided that it evaluates to an integer.
    Constants are used as a replacement for integer values in the program.

  • Public variables are either public or observable. In the latter case the attacker will be able to distinguish their value. They are declared in the following manner:

    public int4 var;
    observable int4 var;

    declare a 4 bits integer variable whose name is var, either public or observable.

    public int4 var := 5;

    declares var and initializes it to value 5. Any expression can be used to initialized a variable, provided that the variables used in the expression are public or constants and have been previously declared. Variable not initialized are implicitly initialized to the value 0.

  • Private variables are either private or secret. The attacker will only infer knowledge on the latter. They are declared in the following manner:

    private int4 var;
    secret int4 var;

    declare a 4 bits integer variable whose name is var, either private or secret.

    private int4 var := [0,1][2,5];

    declares var and restricts the range of var to the two intervals [0,1] and [2,5].
    Again any expression can be used in the bounds of the intervals.

Arrays

Variables can also be arrays of integers or multi-dimensional arrays.
Arrays are declared in addition to the integer type of a variable.

public array[4] of int4 tab;

declares a public variable tab that is an array of 4 bits integer of size 4 (therefore its indices range from 0 to 3).

public array[1..4] of int4 tab;

declares tab as an array of size 4 whose indices range from 1 to 4.
The size of an array can be any expression that evaluates to an integer.

An array variable named tab, whose indices range from 0 to 3, declares 4 variables, whose name are tab[0], tab[1], tab[2] and tab[3]. They have the same publicity and the same integer type as the array. Expressions
can also be used to compute indices, thus allowing in the statements to use variables whose name are tab[expr].

An array can be initialized with a set of initial values:

public array[1..4] of int4 tab := {1,1,2,2};

initialized tab such that tab[1] and tab[2] are equal to 1, tab[3] and tab[4] are equal to 2. Expressions that evaluate to integers can also be used in the set of values. Private arrays can also be initialized in the same manner as any private variable, with a set of intervals:

private array[1..4] of int4 tab := [0,1];

In that case all the variables in the array are initialized to the same range of integers.

Expressions

Expressions are used in guards, assignments, initialization and indices. Binary operators (||,&&,^,+,-,*,/ and %) and unary operators (-,!) can used. Classical operators precedence is assumed. For boolean operations (||,&&,^,!), integer variables are considered as a true value if non null, and false if null.

Only public variables can be used in expressions or constants or integers values.

Guards

Guards are limited to a single comparison between a variable on the right side (either public or private, or a constant, or an integer value) and an expression on the left side. Any comparison operator among <, >, <=, >=, == and != can be used.

Assignments

An assignment statement is written in the following manner:

assign var := expr;

where var is a public variable (with possibly indices) and expr an expression containing no private variables.

Random assignments

The program can used two types of random primitives to assign values to a variable.

random var := random(expr_min,expr_max);

assigns to a public variable var a random value, chosen between the values of expr_min and expr_max, with a uniform probability distribution.

random var := randombit(p);

where p is a float value lower than 1, assigns to a public variable var a random bit value, that is 1 with probability p, and 0 with probability 1-p.

If statements

If conditional statements starts with the keyword if, possibly followed by elif and else, and closes with fi. The consequent statements are listed after the keyword then. For example the following structure are allowed:

if (h <= l) then assign var:=1;
fi

if (h <= l) then assign var:=1;
else assign var:=2;
assign var:=var+1;
fi

if (h <= l) then assign var:=1;
elif (h==l) then assign var:=2;
fi

if (h <= l) then assign var:=1;
elif (h==l) then assign var:=2;
elif (h==l+1) then assign var:=2;
else assign var:=2;
fi

While statements

Conditional while loop starts with the keyword while, followed by a guard, and the statements included in the loop are listed between the keywords do and od. For example the following structure are allowed:

while (h <= l) do
assign l := 1;
assign var := 2;
od

For statements

A for loop can be used to browse all the elements of an array. The syntax is:

for (var in tab) do
// statements
od

The variable var is a local variable that must be only used inside the for loop. It will take successively each value in the array tab. Note that if tab is a multi-dimentional array var is also an array.

Return statements

The program ends when a return statement is reached. Its syntax is simply:

return;

Programs must end with a return statement.

QUAIL compiled language

The analyser takes as input a program written in a simplified lower level language. Briefly, the differences are the following:

  • It has no array and no constant variable.
  • All the terms in expressions must be enclosed within brackets.
  • It has only ‘if’ conditional (no ‘while’ and no ‘for’), without ‘elif’ case, that are not closed with ‘fi’.
  • And additional goto statement is used whose syntax is:

    goto line;

    where line is a line number in the program.\

  • if and else consequences are limited to a single goto statement.
  • The program has no comments and no blank line.

The preprocessor compiles automatically a QUAIL program to this language.

Leave a Reply