-
Notifications
You must be signed in to change notification settings - Fork 14
Home
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 function definitions. Since FaCT code compiles to an object file, and not an executable, no main function is necessary.
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.
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 of unknown static length.
Unlike pointers, arrays cannot be reassigned -- an array variable will always point to the same array.
If a struct has been previously defined with name <name>, its corresponding type can be referred to as struct <name>.
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.
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.
FaCT supports the following basic expressions:
These are the boolean literals true and false, as well as integer literals. Literals are always considered public expressions.
The label of a variable expression is the declared label of the variable being referenced.
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.
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.
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.
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 casted 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.
- Integer negation (e.g.
-xor-(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.
- 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.
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).
E.g. returns_some_value(arg1, arg2, arg3).
The resulting type and label are the type and label specified by the function's definition/declaration.
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.