Sleuth: Automated Verification of Software Power Analysis Countermeasures

Yesterday's study group was led by Elisabeth and was about the work contributed by Bayrak et al. to CHES 2013:

Ali Galip Bayrak, Francesco Regazzoni, David Novo, Paolo Ienne, "Sleuth: Automated Verification of Software Power Analysis Countermeasures", Cryptographic Hardware and Embedded Systems - CHES 2013, Lecture Notes in Computer Science 8086, 2013, pp 293-310 (http://dx.doi.org/10.1007/978-3-642-40349-1_17)

In a nutshell, if one tries to implement a block cipher in a straightforward manner, the implementation may be leaky and susceptible to side-channel attacks. To increase the system's security against attacks of this nature, hardware and software countermeasures can be employed. In the aforementioned work, the authors present a method for automated verification of the security against side-channel attacks of a protected software implementation.

The authors discuss the notions of sensitivity and insensitivity of security-critical applications against power analysis. An operation or group of operations is defined as sensitive, if it depends on secret data but not on any random data. As an example, the authors mention this operation:

st = pt xor key

This operation is vulnerable to power analysis when executed on embedded devices, because power consumption characteristics depend on the secret key, which can therefore be recovered through Differential Power Analysis. This vulnerability can be avoided by applying a random mask to the secret variable. Intermediate calculations are randomized and the mask is removed at the end of the calculation before outputting the ciphertext. However, a secret intermediate value may be leaked if a mask is removed too early and problems of this nature are difficult to detect manually in long and complex implementations.

For their "Power Analysis Sensitivity" method, the authors define four elements:

• A Straight Line Program, which is a sequence of branch-free operations.
• Additions to the Type System, whereby the developer tags each variable as public, secret, or random.
• A Leakage Model.
• Sensitivity of a vector of operations and the leakage related to it.

In this context, a set of operations is sensitive if it has both of the following characteristics:

• It statistically depends on at least one secret input variable
• It does not depend statistically on any random input variables

Verification is a two-step process. Firstly, the authors convert a program to a Data Flow Graph (DFG). Subsequently, the DFG is analysed for the detection of sensitive operations.

Each DFG node represents either an arithmetic/logic operation (x = y op z) or an array handing operation (x = y[z] or y[z] = x). The former node type will have two incoming edges (y and z) and one outgoing edge (for x).

Nodes handing array operations are somewhat more complex, because the accessed address may or may not depend on an input variable. The address is statically-determinable if it depends on a constant (e.g. y[0] = x), since the program will always access element 0 regardless of inputs. Conversely, x = y[z] is not statically-determinable if z is a node input. If all accesses to an array are statically-determinable the array is called directly accessed and all its accesses are treated as if they were ordinary assignment operations (as above). Otherwise, it is called indirectly accessed and its behaviour is represented in the DFG through a Look-Up-Table (LUT). To achieve perfect accuracy, the LUT is formed by all inputs influencing either data in the array or the array element being accessed. Therefore, the LUT is a 2^m : 1 multiplexer, whereby m is the total width in bits of the aforementioned inputs.

A DFG can compute the univariate leakage of an operation as, for example, the Hamming Weight (HW) of the result of the lookup operation. Similarly, bivariate leakage caused by the sequential execution of two operations can be calculated as a Hamming Distance (HD). HW and HD are only examples of leakage models.

As discussed above, sensitivity has been defined in terms of statistical dependence between variables. To test these conditions, the authors formulate the problem as a satisfiability query (SAT) and argue that the statistical dependence condition is analogous to don't care analysis of logic synthesis. Their solution first checks the second sensitivity condition (dependence on random variables) before testing dependence on a secret variable (first condition).

Sleuth has been implemented in the back-end of the LLVM open source compiler. Sleuth uses LLVM assembly as its input. The authors discuss that machine-specific assembly can be converted to LLVM assembly in a straightforward fashion and mention as an example a script developed by themselves to perform such conversion from AVR assembly. High-level languages (e.g. C) can be analysed by first compiling them into LLVM assembly using off-the-shelf compilers. As discussed above, the verification algorithm works on straight line programs. To this end, Sleuth converts LLVM assmebly to a straight line program by unrolling loops and inlining function calls, without applying any optimizations. The output of this conversion is used to generate the DFG and operations are then queried for sensitivity based on security types and leakage models provided by the user.