Skip to content

FaCT Language Reference

Jump to bottom
scauligi edited this page Mar 17, 2018 · 15 revisions

This document is a detailed reference document for the FaCT language. If you’re just looking for some example code patterns, head to the Useful FaCT Patterns page.

FaCT is a domain-specific language with a C-like syntax. Programs are written in one or more *.fact files, and compiled into a single C object (*.o) file.

A FaCT file consists of a sequence of struct definitions, C extern declarations, and FaCT function definitions. Since FaCT code compiles to an object file, and not an executable, no main function is necessary.

Table of Contents

Language Specification

Types

Basic types

FaCT supports the following basic types:

  • bool

  • uint8, uint16, uint32, uint64, uint128

  • int8, int16, int32, int64

Just as in many other languages, the FaCT compiler tracks the types of expressions and enforces type safety. An expression of type uintN can be silently upcast to an expression of type uintM, where M > N. Similarly, an expression of type intN can be silently upcast to an expression of type intM where M > N.

Integer types and bool types cannot be cast to each other, implicitly or otherwise.

Array types

FaCT supports arrays of any basic type with a fixed known size, e.g. int32[4] for an array of four int32 values. If the length of the array is not known at compile time, empty brackets may be used, e.g. uint8[] for an array of unsigned bytes with length determined at runtime.

Unlike pointers (e.g. in C), arrays cannot be reassigned — an array variable will always point to the same array.

Struct types

If a struct has been previously defined with name <name>, its corresponding type can be referred to as struct <name>.

Labels

FaCT has two labels: public and secret. All variables are required to have a label. The label of a variable is given at the variable’s declaration and cannot change.

The FaCT compiler keeps track of the labels of expressions, just as it keeps track of the types of expressions. The label of any expression derived from a secret expression is itself secret. Otherwise, if the expression is composed entirely of public expressions, then its label is public.

Mutability

All variables in FaCT are either immutable (const), or mutable (mut). If not specified, a variable is const by default. Variables that are const may not be reassigned. Similarly, array variables that are const may not have their elements be reassigned through that array variable, and structs that are const may not have their fields updated through that struct variable.

Expressions

Basic expressions

FaCT supports the following basic expressions:

Literals

These are the boolean literals true and false, as well as integer literals. Literals are always considered public expressions.

Hexadecimal and binary integer literals can be expressed using the prefixes 0x and 0b respectively, e.g. 0xfd3a or 0b1001101.

Variables

The label of a variable expression is the declared label of the variable being referenced.

Array indexing

E.g. array_var[7] or buf[i - 1]. The indexing expression must have label public. The label of the resulting expression is the declared label of the array.

Struct fields

E.g. struct_var.c or state.ctx[8].num_buffers. The label of the resulting expression is the declared label of the field in the struct’s definition.

Array length

E.g. len array_var. The len keyword followed by an array variable gives the length of the array. If the size is known at compile time, this is treated just like an integer literal. If the size isn’t known until runtime, this is the runtime length of the array. This value is always considered to be public.

Casting

E.g. (uint8)var_of_type_uint16 or (int32)(byte_buf[2] + 5). Any integer type may be explicitly cast to any other integer type. If the new type is smaller than the old type, the expression is truncated. If the new type is larger than the old type, the expression is either sign- or zero-extended, depending on whether the expression being cast is an int type or uint type, respectively. Truncation always happens, even if an expression is immediately cast back to its original size. The label of a casted expression is the label of the original expression.

Unary operators

  • Integer negation (e.g. -x or -(len arr_var + 3))

  • Logical not (e.g. !cond)

  • Bitwise not (e.g. ~expr)

The type and label of a unary expression is the type and label of the original expression.

Binary operators

  • Arithmetic (+, -, *, /, %)

  • Comparison (==, !=, <, ⇐, >, >=)

  • Boolean arithmetic (&&, ||)

  • Bitwise arithmetic (&, |, ^)

  • Bit manipulation (<<, >>, <<<, >>>)

If either operand of a binary expression is secret, the resulting expression is secret. Otherwise, the expression is public.

The division (/) and modulo (%) operators can only operate on public expressions.

If both operands of an arithmetic operation share the same integer type, the resulting expression will also have that same type. Note that this means arithmetic operations will silently wrap around. If the operands do not have the same type, but one operand can be implicitly upcast to the other, the upcast will take place before the operation.

The operands for the equality operators (==, !=) must either both be bool or both be compatible integer types.

The type of a bitwise-and (&) operation is the type of the smaller-typed operand, for convenience. E.g. the type of uint32_variable & uint8_variable is uint8.

The type of bit-shifting (<<, >>) and bit-rotating (<<<, >>>) operations are the type of the left operand.

Ternary operator

E.g. cond ? expr_if_true : expr_if_false. This is the same as the ternary operator from C.

If any of the three operands are secret, the resulting expression is secret. Otherwise, the expression is public.

If the first operand (the condition) is secret, then the expression will be transformed during compilation such that the selection is done in constant time. This ensures that the value of the condition is not leaked via timing.

The first operand must be a boolean, and the second and third operands must have compatible types. The type of the ternary expression is the type of the second/third operands (after implicit upcasting in the case of different, but compatible, types).

Function calls

E.g. some_fn(arg1, arg2, arg3).

The resulting type and label are the type and label specified by the function’s definition/declaration.

If a function expects a mut variable or array, the corresponding argument must be passed with the ref keyword. E.g. foobar(ref x). The argument must be mutable itself — it is illegal to pass a const variable with ref.

For convenience, array views (see "Array declaration" section below) can be passed directly as arguments. E.g. takes_4byte_array(arrview(buf, 0, 4)) or mutates_buffer(ref arrview(buf, 2, 26)).

Declassify

E.g. declassify(some_secret_expr).

A secret expression can be explicitly declassified to become public. This is not recommended. Only do this if absolutely necessary.

For the sake of future clarity, both for yourself and for developers who will be reading your code later, we highly recommended that you leave detailed comments about why this declassify is necessary and an explanation of why the resulting code is still secure.

If the code is indeed secure, and can be proven statically, consider submitting an issue (or pull request) to the FaCT compiler so that it can prove this property itself and obviate the need for the declassify call.

Statements

Basic variable declaration

E.g. public uint8 x = 8; or secret mut int32 y = x - 6;

Must of the form LABEL [mut] TYPE NAME = EXPR;. If mut is not given, the variable is assumed to be const. An initializing expression is mandatory; uninitialized variables are not allowed.

Array declaration

E.g. public uint8[16] buf = arrzeros(16); or secret mut uint32[] copied = arrcopy(other_array);.

Similar to a basic variable declaration, but with an array initializer instead of a normal expression.

Valid array initializers are:

  • An array literal, e.g. { 2, 4, 3, 1 }

  • A variable (must be the same array type and length)

  • arrzeros(length), which results in a fully zeroed-out array

  • arrcopy(array), which copies the specified array

  • arrview(array, index, length), which creates a "view" into the specified array starting at index

  • noinit(length), which does not initialize the array (only use if you will be initializing the array later in the function!)

In the above initializers, length and index must be public expressions.

The arrview initializer does not create a new array; if an element of the view is modified, the corresponding element of the original array is also modified. Views can be used to create subarrays of larger arrays, or for creating a const view of a mut array.

Assignment

E.g. x = 5; or buf[i] = x + 3;

Assignment works as with other C-like languages, provided the types are compatible.

It is illegal to assign a secret expression into a public variable, and it is illegal to assign anything into a public variable when in a secret control flow context (see Conditionals below).

The "operator-equals" form of binary operators (x += expr, etc.) is allowed, and is syntactic sugar for x = x + expr etc.

Conditionals (if statements)

E.g. if (x > 5) { …​ }

Just as in C, multiple conditionals can be chained using else if and else blocks.

If the expression is public, the conditional works just like a C-style if block.

If the expression is secret, the conditional block is evaluated under a secret control flow context: all statements with side effects (such as assignment) are transformed into semantically equivalent constant-time form. Any information that would indicate whether or not the branch was taken is prevented from being leaked.

Loops (for loops)

E.g. for (uint32 i = 0; i < nblocks + 2; i += 1) { …​ }

The first section of the for loop must be a numeric variable declaration. The label is implicitly public. The second section can be any public boolean expression. The final section must be an assignment into the loop variable of a public expression.

Returning from a function

E.g. return x + 5;

The type and label of the returned expression must match the return type of the surrounding function.

If a return statement is within a secret control flow context, the statement is transformed so that the value is stored in a variable and returned at the end of the function, so that the function’s timing does not end immediately. The rest of the function is evaluated in a secret control flow context. Be aware!

Function definitions

E.g. export secret int32 foo(secret uint8[32] buffer, public mut int32 outval) { …​ }

A FaCT function definition is similar to a C definition, but with additional annotations.

The return value (if not void) must have a label. Each parameter must also have a label, and must be marked mut if it will be an output parameter.

A function will not be exposed to the generated C API unless it is marked export. The C interface works as follows:

  • FaCT arrays correspond to C pointers

    • Arrays with unknown static length correspond to two parameters: a pointer and a length

  • FaCT simple types marked mut correspond to C pointers

  • FaCT simple types not marked mut correspond to C simple types from stdint.h

    • Note: the FaCT bool type corresponds to the C uint8_t type

If a function has the inline attribute, then the FaCT compiler will force inlining at every call site. This is most useful for small helper utilities, and is a replacement for macros in C. A function cannot be both inline and export.

If a function has no attribute, it will not be exposed to the generated C API.

If a function has any mut parameters (and thus has side effects), it can only be called from a secret context (e.g. within a secret branch) if it is not exported.

Extern function declarations

E.g. extern secret int32 foo(secret uint8[32] buffer, public mut int32 outval);

An extern declaration allows FaCT functions to call the declared function as if it were defined with the stated signature. The function is assumed to be defined elsewhere (usually in a C file elsewhere in the project).

Struct definitions

E.g.

struct sample_type {
    secret int32 field1;
    public uint8 field2;
    public uint8[3] spacing;
    secret uint8 array_field[32];
}

void foo(struct sample_type x, mut struct sample_type y) { ... }

Struct definitions are intended for FaCT to be able to effectively interface with external code that depends on specific structure layouts. A struct does not have a label of its own; each instance of a struct has fields with the labels specified in the struct’s definition.

Structs in FaCT are always considered packed. If you need unpacked structs, you must manually add additional fields to fill out the proper spacing.

Clone this wiki locally