key: cord-0047335-yjh6cb89
authors: Mogensen, Torben Ægidius
title: Hermes: A Language for Light-Weight Encryption
date: 2020-06-17
journal: Reversible Computation
DOI: 10.1007/978-3-030-52482-1_5
sha: 886be8a2e01428d497ece895d1dde01e97a92829
doc_id: 47335
cord_uid: yjh6cb89

Hermes is a domain-specific language for writing light-weight encryption algorithms: It is reversible, so it is not necessary to write separate encryption and decryption procedures, and it avoids several types of side-channel attacks, both by ensuring no secret values are left in memory and by ensuring that operations on secret data spend time independent of the value of this data, thus preventing timing-based attacks. We show a complete formal specification of Hermes, argue absence of timing-based attacks (under reasonable assumptions), and compare implementations of well-known light-weight encryption algorithms in Hermes and C.

Recent work [12] have investigated using the reversible language Janus [5, 19] for writing encryption algorithms. Janus is a structured imperative language where all statements are reversible. A requirement for reversibility is that no information is ever discarded: No variable is destructively overwritten in such a way that the original value is lost. Instead, it must be updated in a reversible manner or swapped with another variable. Since encryption is by nature reversible, it seems natural to write these in a reversible programming language. Additionally, reversible languages requires that all intermediate variables are cleared to 0 before they are discarded, which ensures that no information that could potentially be used for side-channel attacks is left in memory. But non-cleared variables is not the only side-channel attack used against encryption: If the time used to encrypt data can depend on the values of the data and the encryption key, attackers can gain (some) information about the data or the key simply by measuring the time used for encryption. Janus has control structures the timing of which depend on the values of variables, so it does not protect against timing-based attacks.

So we propose a new reversible language, Hermes, specifically designed to address these concerns. Although somewhat inspired by Janus, Hermes has some significant differences, as we shall see below. An early version of the Hermes language was presented in [7] . Experiments using this language have indicated a need for a type system that separates secret and public data. In the early version, the (informally specified) type system distinguishes constants, loop variables, and all else, with constants and loop variables being considered non-secret and all else being secret. This early language is, however, too restrictive in many cases and too permissive in other cases:

-Loop bounds and array sizes were constants, so algorithms with variable-size keys or data would have to have a procedure for each size. -Loop counters could in the early version of Hermes only be updated by constant values, which may also be too restrictive. -Procedure parameters are not distinguished by secrecy, so loop counters could not be passed as parameters. By classifying parameters as public or secret, loop counters can now be passed as public parameters. -Any value was allowed as index to an array, but since timing can depend on the index value (due to caching), this is a potential side channel. By limiting array indices to public values, this can be avoided.

So we propose a new version of Hermes that uses public and secret types, with strong restrictions on operations on secret values. Constants and loop counters are public, all other variables are by default secret, but can be declared public.

The type system not only tracks flow of information similar to binding-time analysis [3] , trust analysis [8] , and information flow analysis [11] but also imposes restrictions to ensure reversibility and (under reasonable assumptions) avoid timing-based side-channel attacks.

Decls → | T ype V arSpec ; Decls | const id = numConst ; Decls 

The core syntax of Hermes is shown in Fig. 1 . The grammar uses tokens specified in boldface. These are described below.

id denotes identifiers. An identifier starts with a letter and can contain letters, digits, and underscores. numConst denotes decimal or hexadecimal integers using C-style notation. IntType denotes names of integer types. These can be u8, u16, u32, and u64, representing unsigned integers of 8, 16, 32 or 64 bits. unOp denotes an unary operator on numbers. This can be bitwise negation (~). binOp denotes an unary operator on numbers. This can be one of +, -, *, /, %, &, |,^, ==, !=, <, >, <=, >=, <<, and >>. All arithmetic is modulo 2 64 . Comparison operators return 2 64 −1 (all ones) when the comparison is true and 0 when the comparison is false. Note that this is different from their behaviour in C, where they return 1 and 0, respectively. &, |, and^are bitwise logical operators. update denotes an update operator. This can be one of +=, -=,^=, <<=, and >>=. The first three operators have the same meaning as in C. <<= is a left rotate. The rotation amount is modulo the size of the L-value being rotated, so if, for example, x is an 8-bit variable, x <<= 13; will rotate x left by 5 bits.

>>= is a right rotate using similar rules. Note that the meaning of <<= and >>= differ from their meaning in C, where they represent shift-updates.

Values in Hermes are all 64 bit unsigned integers, and they can be secret or public. Scalar and array variables additionally impose a number size (8, 16, 32 or 64 bits). A constant just has the type constant, which is implicitly a 64-bit number. So we have:

We use t with optional subscript to denote a value type, τ with optional subscript to denote a variable type, and z with optional subscript to denote a size. So t z denotes the special case of variable types where the variable is a scalar nonconstant. We define a partial order as the reflexive extension of public < secret and a least upper bound operator induced by this partial order. We use this to make the result secret when secret and public values are mixed.

Variable environments, denoted by ρ with optional subscript, bind identifiers (denoted by x with optional subscript) to variable types. Environments are functions, so ρ(x) is the variable type that x is bound to in ρ. We update environments using the notation ρ[x → τ ], which creates a new environment that is identical to ρ, except that x is bound to τ .

Sequents for typing expressions, denoted by e with optional subscript, are of the form ρ E e : V alT ype, and sequents for typing L-values (denoted by l with optional subscript) are of the form ρ L l : V arT ype. In order to make updates, swaps, and parameter passing reversible, we must impose restrictions to avoid aliasing and similar clashes. To do this, we introduce functions that find variables in expressions or parts of expressions. V () finds the variables in an expression or L-value, R() finds the root variable of an L-value, and V () I finds the variables in index expressions in an L-value.

Note that V () does not include variables in size-expressions, as these are harmless in terms of aliasing. We specify rules for L-values and expressions in Fig. 2 . For L-values, the rule for variables says that a variable has the type specified by the environment. The rule for array access says that the array variable must have an array type and the index expression must be public. This ensures that timing of memory accesses (which can depend on the address, but not the accessed value) does not leak secret information. The rules for constants state that a constant is public. n denotes an integer constant. The rule for non-constant L-values say that the L-value must be a scalar and that the expression type is the value type part of the type of the L-value. The rule for an unary operator ¬ just say that the result has the same type as its argument. The rules for a binary operator is more complex. If any of the arguments are secret, the result is also secret. Additionally, some potentially time-variant operations are not allowed on secret values. We assume a set T V of time-variant operators is given. This will typically contain division and modulo operators, but can also contain multiplication if the target architecture does not have a constant-time multiplication instruction. The last rule states that the size of an array is a public value.

A seqent for a statement s is of the form Γ, ρ S s and states that given a procedure environment Γ and variable environment ρ, the statement s is well typed. A procedure environment binds procedure names to lists of variable types. The type rules for statements are shown in Fig. 3 .

The first rule says that the empty statement is well typed. To ensure reversibility, the rule for updates (where ⊕= denotes an update operator) says

that the root variable of the L-val must not occur in the expression. Furthermore, if the expression is secret, the L-Val must also be secret. The rule for a swap states that the two L-values must have exactly the same type, and that the root variable of one side can not occur in index expressions on the other side. The rule for conditional swap additionally requires that the root variables of the L-values do not occur in the condition and that the condition is no more secret than the L-values. The rule for loops state that the loop bounds must be public, and that the loop variable is implicitly declared to be a public 64-bit variable local to the loop body. The rules for procedure calls state that the types of the argument L-values must match those found in the procedure environment. Furthermore, to avoid aliasing and ensure reversibility, the root variable of one argument can not occur in another argument. The rule for blocks states that all statements in the block must be well typed in the environment that is extended by the local declarations. Static scoping is used. The bottom of Fig. 3 show the rules for extending environments. Sequents for declarations are of the form ρ D d ; ρ 1 , and state that the declaration d extends the environment ρ to ρ 1 . The first rule state that an empty declaration does not change the environment. The rule for constant declarations extends the environment with the constant name bound to constant. The rules for variable declarations are straightforward. The rules for array declarations require that the expression that determines the size of an array must be public, and that the array variable can not shadow any variable used in this expression.

The rules for declarations of procedures and programs are shown in Fig. 4 . A sequent of the form pgm states that pgm is a valid program. P p ; Γ states that a procedure p generates a procedure environment Γ , Γ P p states that, given the procedure environment Γ , the procedure p is valid, and A a ; V /τ states that the argument list a generates the variable list V and the type list τ . We use to append two (variable or type) lists and ∩ to represent the set of elements common to two lists.

The rule for programs first builds a procedure environment, ensuring that no procedure is declared twice, and then checks that all procedures are well typed in this procedure environment. Procedures can all call each other. The P rocedure1 rule builds a procedure environment for a single procedure, and P rocedure2 checks that a single procedure is well typed. Both use rules for building a list of argument names and types, ensuring no name occurs twice. 

The run-time semantics of Hermes does not distinguish secret and public values -type checking ensures that no secrets leak into public variables -so values in Hermes are just sized numbers. Expressions all evaluate to 64 bit numbers, which are only truncated when used to update variables or array elements, which can be 8, 16, 32, or 64 bits in size. An array has an element size, a vector size, and a vector of elements of the vector size. The sizes of scalar variables and the element sizes of array are known at compile time, but for specification convenience they are part of the run-time environments. A compiler can check sizes at compile time, so the run-time environments bind names (or offsets) to locations only. Similarly, named constants can be eliminated at compile time, so they do not need to be part of the run-time environments.

Environments (η) bind constants to their value and variables to their integer sizes (8, 16 , 32, or 64) and locations. Stores (σ) bind locations to values. The value of a scalar variable is an 8, 16, 32, or 64 bit integer, and the value of an array is a record (struct) of its vector size and its vector. The elements of the vector are locations holding 8, 16, 32, or 64 bit integers, according to the integer size of the array. We use the same notation for environments as in the type semantics, but we also use the update notation as a pattern: If η 1 is known, we use the notation η 2 [x → v] = η 1 to say that η 2 is equal to η 1 with the latest binding of x removed. This means that earlier bindings of x are retained in the environment and can be retrieved. The environments are stack-like: Bindings are removed in the opposite order in which they are created. Stores, on the other hand, do not need to retain older bindings of locations, so when a new value is bound to a location, the old value can be forgotten. We use the notation σ[λ :

= v] when updating stores. While this is not immediately evident from the semantic rules, there is only be one store in use at any given time, and locations are disposed of in the opposite order of their creation, so the store acts like and can be implemented as a global stack, allocating new zero-initialised locations on the top of the stack and removing them in the opposite order of their allocation. We use a family of functions newlocation z where z an integer size (8, 16 , 32, or 64) that takes a store σ returns a new store σ 1 and location λ of size z such that λ is bound to zero in σ 1 , and the dual function disposelocation z that takes a storeσ 1 and a location λ and returns a store σ obtained by removing (unstacking) λ from σ 1 , after checking that the contents of λ in σ 1 is 0. If not, the result is undefined. If (σ 1 , λ) = newlocation z (σ), then σ = disposelocation z (σ 1 λ) .

We also use a family of functions newarray z that each take a store σ and a vector size vs and returns a new store σ 1 and a location λ that in the new store is bound to two fields: σ 1 (λ) = (vs, ve), where vs is the vector size at this location, and ve is a vector of new locations for the elements of the vector, all of which are bound to zero in the new store. We use array notation to access elements of a vector. newarray z also have duals, disposearray z , that each take a store σ 1 , a vector size vs, and a location λ and returns a new store σ where the array at λ has been removed (unstacked). It checks that the vector size at the location matches vs, and that all vector elements are locations with zero as content. If either of these is not true, the result is undefined. If (σ 1 , λ) = newarray z (σ, vs), then σ = disposearray z (σ 1 , vs, λ). Figure 5 shows the evaluation rules for L-values and expressions. L-values evaluate to locations, and expressions to 64-bit integers. Sequents for L-values are of the form σ, η |= L l @ (z, λ) and state that the L-value l is stored at location λ which is of size z. We use a special case for constants: When λ = null, l is a constant equal to z. null is a null location where no values are stored. The rule for variables and constants says that the size and location of a scalar variable or constant is found in the environment. The rule for array elements states that the location of the variable is bound in the store to a pair of vector size and vector elements, that the index expression must evaluate to a value less than the vector size, and that the location of the array element is found in the vector of elements. The type system guarantees that the location is not null and that it is bound to a pair, but it does not ensure that the index is within bounds, so this is checked at runtime. If the index it out of bounds, the effect is undefined.

The two first rules for expressions handle constants. The first handles simple number constants, which evaluate to themselves, and the second handles named constants that are bound to pairs of values and null locations. The rule for L-values finds the location of the L-value and gets its contents from the store, and then extends the value to 64 bits. For this, we use a postfix operator ↑ z that extends a z-bit value to 64 bits. The rules for unary and binary operators evaluate the operand(s) and then applies the semantic operator to the value(s) of the operand(s). Finally, the rule for size finds the size of the array in the store. The type system ensures that the location is not null and that it is bound to a pair.

To handle uncall in the semantics for statements, we need to "run" statements backwards. To this end, we use the function I in Fig. 6 to invert statements:

In a type-correct program, the effect of first executing s and then I(s) is, if s terminates without error, a null effect: The store is in the same state as before s was executed. Proving this is tedious, but relatively uncomplicated. The main complications are declarations and that some statements are only reversible if the aliasing constraint in th etype system hold. We do, however, not at the time have a complete proof written down.

Statements transform stores into stores, while keeping the environment unchanged. Sequents for running statements are of the form Δ, η |= S s : σ 0 σ 1 and state that, given a procedure environment Δ and a variable environment η, a statement s reversibly transforms a store σ 0 to a store σ 1 .

The rules for statements are shown in Fig. 7 . The rule for the empty statement states that it does not change the store. The rule for updates finds the value v of the L-value and the value w of the expression. It then truncates w to s bits (using the ↓ s operator), performs the operation (restricted to s bits) between the two values, and stores the result in the location of the L-value.

The rule for swap finds the values of the two L-values in the store and updates the store with these swapped. There are two rules for conditional swap: The first rule states that if the condition evaluates to 0 (false), there is no change in the store. The other rule states that if the condition evaluates to a non-zero (true) value, the effect on the store is like an unconditional swap. Note that this does not imply that the condition is evaluated twice if it is non-zero, nor that the timing differs. It is up to the implementation to ensure invariant timing.

The rule for loops first evaluate the loop bounds, allocates a new location in the store, and stores the first bound at the location, applies helper rules |= F using an environment where the loop counter is bound to the location, and then disposes of the location in the resulting store. There are two helper rules: One for when the loop counter is equal to the second bound, and one where it does not. Both use the location and the value of the second bound.

The rule for call finds the sized locations of the arguments, looks the procedure up in the procedure environment to get the list of parameter names and the body of the procedure. It then creates a new environment that binds the parameter names to the argument locations and executes the body in this environment. This implements call-by-reference parameter passing. The rule for uncall is similar, but it is the inverse of the body that is executed. The type system guarantees that the sizes of the given parameters are the same as the sizes of the declared parameters.

The rule for blocks uses the declarations to extend the environment and store, executes the body, and uses the declarations to restrict the store.

The rules for declarations is shown in Fig. 8 . There are two kinds of sequents for declarations: η 0 , σ 0 |= D d ; η 1 , σ 1 says that the declaration d extends η 0 and σ 0 to η 1 and σ 1 . Conversely, η 0 , σ 0 |= inv D d ; η 1 , σ 1 says that "undoing" the declaration d restricts η 0 to η 1 and σ 0 to σ 1 .

The first two rules say that the empty declaration has no effect. The next two rules state that a constant declaration extends the environment but leaves the store unchanged. Recall that constants are stored in the environment by using a null location. The rules for variable and array declarations do not distinguish secret and public values. In the forwards direction, a new location (bound to zero) is created for the variable and the variable is bound to the location. In the backwards direction, disposelocation z verifies that the location is bound to zero before it is removed from the store. In the forwards direction, a new zeroed array is created in the store and the variable is bound to its location in the environment. In the backwards direction is it verified that the expression evaluates to the array size, and disposearray z checks that the elements of the array are all bound to 0 in the store and removes the array from the store. Note that the rules for undeclaring things treat the declarations in reverse order.

The rules for procedures and programs are shown in Fig. 9 . There is no main function and no input/output in Hermes, so it is assumed that procedures are called from outside Hermes. Therefore, the semantics of a program is just creating a procedure environment Δ. The external program can call (or uncall) a procedure in this environment by providing a store and a list of locations for the procedure parameters. The rule for procedures creates a procedure environment for a single procedure. This binds the procedure name to a list of (name, integer size) pairs and the body of the procedure. The environments are combined using in the rule for programs. Additional rules describe external calls to Hermes. These are very like the rules for calls in statements, except that the locations are given directly instead of being derived from a list of L-values. 

In the examples, we use some syntactic sugar that the Hermes compiler expands into the core syntax during parsing. The statements Lval++;, Lval--;, and if (Exp) Lval update Exp; are expanded to Lval += 1;, Lval -= 1;, and Lval update (Exp != 0) & (Exp);, respectively. The latter works because 0 is a neutral element for all the update operators used in Hermes. A declaration that specifies a number of variables and arrays of the same type is expanded to a sequence of individual declarations, and if secret or public is omitted from a declaration, secret is assumed. For example, the declarations public u32 x, a[n]; u64 z; is just a shorter way to write the equivalent public u32 x; public u32 a[n]; secret u64 z;. Operator precedences can be overridden by parentheses. Figure 10 (top) shows Hermes code for the TEA encryption algorithm [14] , a simple cypher used mainly for teaching. Only the encryption function is showndecryption is done by uncalling the encryption function. The sizes of v and k are 2 and 4, respectively. Compare to the equivalent program in C [17] at the bottom of Fig. 10 . Apart from using updates and swaps, the main difference is that the C version requires an explicit decryption function, which is not needed in Hermes. Also, the local variables are in Hermes cleared to 0 by "uncomputation", where the C version leaves these uncleared. Figure 11 shows Hermes and C code for the central part of RC5 [9] , another simple algorithm. The Hermes program shows size s being used as a loop bound, which makes the procedure independent of the size of the expanded key. Since C does not have a rotate operator, the C version [15] uses a macro for this. And since C does not have a swap operator, the central loop is unrolled so one iteration in the C version correspond to two iterations in the Hermes version. Again, C needs an explicit decryption function (not shown), which is not required in Hermes. Key expansion in RC5 (not shown) is not reversible, so to implement this in Hermes requires storing additional values i "garbage" array. Th garbage array is reset to zeroes when the expanded key (after calling the central procedure) is uncomputed by uncalling the key expansion procedure. Figure 12 shows Hermes code for speck128 [1, 18] (a cypher used by NSA). Again, only encoding is shown. The main thing to note is that the R procedure are found in two copies, one (Rs) where the k parameter is secret, and one (Rp) where it is public. This is because two of the calls pass a public loop counter to k, while the other two calls pass part of a secret key to k. An extension to the type system that avoids this codeduplication is being investigated. Some uncomputation is needed to restore a and b to 0. This is not found in the standard C implementation, where these are left uncleared.

We have implemented several other encryption algorithms in Hermes, including Red Pike [16] (a cypher used by GCHQ) and Blowfish [10] (designed as a replacement for DES). With the exception of key expansion, this was relatively straight forward.

We have presented a language Hermes for writing light-weight encryption functions. Hermes ensures reversibility, so decryption can be done by executing encryption procedures backwards, and can (given a suitable implementation) protect against certain forms of side-channel attacks, such as timing based attacks and leaks to memory. Hermes has a formal semantics for both the type system and runtime behavior. These semantics can be used to prove both that secret information does not leak into publica variables and that type-correct programs are, indeed, reversible, but we do not have complete proofs for this at the moment, mainly because we expect Hermes to evolve over time, so we have postponed proofs until Hermes settles to a more stable form. The semantic rules do not specify what happens if a condition in a rule fails, for example when an array bound is exceeded. For the type rules, the obvious behaviour is an error message. For the run-time semantics, it is less clear. Run-time error messages can be helpful in locating errors, but they can potentially leak information about secret values. So it might be better to continue execution with some default behaviour.

We have in Standard ML made a reference interpreter for Hermes which closely follows the semantic rules. The interpreter does not guarantee timeinvariant operations, and it reports errors when run-time errors are detected. We also have an implementation of Hermes in WebAssembly [2] . We are working on extending this to target CT-Wasm [13] , a variant of WebAssembly that has a public/secret type system similar to the one used here. Targeting CT-Wasm should preserve the safety features of Hermes. Note that the aliasing restrictions in Hermes make call-by-reference indistinguishable from call-by-value-return, so this can be used as an optimisation when WebAssembly, as planned, supports multiple return values.

We are currently working on implementing the Advanced Encryption Standared (AES) in Hermes. An issue with AES is that it uses secret information as array indexes, which the current Hermes does not allow, so to implement it may require a relaxation of this restriction, for example by ensuring the array is fully cached, so access time is independent of the index. We are also considering other extensions to Hermes, including sized boolean types (with values 0 and 2 z −1) and read-only parameters to procedures. The latter will avoid the need of duplicating the R procedure in Fig. 12 . We are also considering additional control structures, but will only add them by need. A more precise alias analysis could relax some of the restrictions on parameter passing, but we have not found any examples where this matters. At the moment, index checks and checks that variables and arrays are zeroed before being disposed are done at run time. Static verification of these would be beneficial, for efficiency and safety both.

Some side-channel attacks (such as Spectre [4] ) target speculative execution. By partially evaluating [3, 6] Hermes programs with all public values (typically key and block lengths) considered static will leave a straight-line unconditional sequence of operations only involving secret values and constants, thus avoiding speculative execution. This has the added benefit that it is easier to eliminate index checks and checks for variables being zero at the end of blocks.

Public-key cyphers are not trivially reversible -that would defeat the purpose -so implementing these in Hermes it not obvious. A possibility is to let the encryption function return not only the cypher text, but also additional "garbage" information that must be discarded before transmitting the cypher text. Similarly, decryption also produces garbage in addition to the original text. As such, the reversibility of Hermes is not exploited, but is rather a hindrance. The safety features still apply, though.

The SIMON and SPECK families of lightweight block ciphers

Bringing the web up to speed with Webassembly

DIKU 1998

Exploiting speculative execution

Janus: a time-reversible language. A letter to Landauer

AE: Partial evaluation of the reversible language Janus

Hermes: a reversible language for writing encryption algorithms (work in progress)

Trust in the λ-calculus

The RC5 encryption algorithm. Dr. Dobb's

Description of a new variable-length key, 64-bit block cipher (Blowfish)

Principles of secure information flow analysis

Encryption and reversible computations

CT-Wasm: type-driven secure cryptography for the web ecosystem

TEA, a tiny encryption algorithm

Wikipedia: Red pike (cipher)

Wikipedia: Tiny encryption algorithm

Principles of a reversible programming language

We thank our colleagues Ken Friis Larsen and Michael Kirkedal for co-supervising some student projects about Hermes and for fruitful discussions, and we thank the students who worked on these projects.