PROOFS: Security Proofs for Embedded Systems

Leuven, Belgium — Thursday, September 13rd, 2012

Goal of the Workshop

The goal of the PROOFS workshop is to promote methodologies that increase the confidence level in the security of embedded systems.

Embedded system security too frequently consists in security by obscurity solutions (except, of course, for high-security solutions produced by specialized firms, for instance in the smartcard industry). This has obvious drawbacks:

it requires costly black-box evaluation,
there is no certainty about the correctness of the security, etc.

Formal methods allow to increase the trust level of digital systems. They are very appealing, for the following reasons:

they are mature in theory, and there are off-the-shelf tried and tested methods and tools,
they have been applied both on software and hardware for a long time, mainly for safety and conformance tests, but also sometimes for security assessment.

Some important security features (random number generation, physically unclonable functions, side-channel resistance, etc.) rely on analog devices. Their correct functioning can be ascertained by techniques such as physical modeling and unitary experimental testing. But in general, physical models are better evaluated by mathematical methods, which encompass "formal methods".

An important objective for the PROOFS workshop is to bridge the gap between both topics, and therefore to pave the way to « security by clarity » in the design and the evaluation of embedded systems.

Scientific Context

Embedded System Security

Many efforts have been made to increase the security level of embedded systems. Nonetheless, serious threats remain.

Side-channel attacks do indeed allow to extract secrets in the real world. During the last decade, modelization attempts for the the security of systems against those attacks have been conducted. However, current evaluations are insufficient, since:
- some are countermeasure-dependent, which limit their scope;
- most of them only capture the leakage when the key is used in the crypto, and do not cover the complete life-cycle (generation, transfer, erasure) that is nonetheless described in the application source code;
- they seldom address the logical side-channels, e.g. leakage via resource sharing.
Fault injections attacks allow to recover keys:
- in one strike by bypassing access controls (PIN or authentication protocols bypassing or forcing to true),
- in one to few strikes in the crypto (Bellcore on RSA-CRT, DFA on block ciphers),
- by biasing the analog TRNG by the application of an external strong coupling.
Countermeasures have proposed but usually lack formalism. For instance, some countermeasures patch implementations (e.g. this implementation of RSA improves on top of this one, in which a flaw was discovered). Nonetheless, no proof of flaw absence has been given.
Invasive attacks allow to read internal buses, to grant access by modifying the hardware. So far, to our best knowledge, few "intelligent" detection methods or countermeasures have been proposed against this class of attacks (but for a few exceptions). Thus, the state-of-the-art protections resort to archaic solutions, such as hardware shielding, obfuscation or complex security-by-obscurity checkpoints and ratification counters. We believe that a proper formalization of the threat could help the emergence of trustworthy & low-cost solutions against invasive attacks.

Formal Methods for Security

Basically, solutions promoted by formal methods to check the security require two steps:

Formalization of the system, since it must be captured unambiguously with a formal paradigm to be processed;
Proof of security features.

A priori, all formal methods can be applied: model checks, theorem proving, etc. This work is commonplace in the fields of safety (critical software for medical, transportation, industrial, etc. applications) and of non-embedded software (certified compilers, bytecode verifiers, etc.).

Nonetheless, the issues of embedded system are special insofar as they address the boundary between software and hardware. We call firmware the piece of software that is the closest to the hardware. Formal methods indeed operate on a textual description of the system: in this case, this software is the firmware.

The security issues in embedded systems arise from interactions between software and hardware. For instance, fault attacks modify the data (software variables) by altering the hardware (physical malfunction). Yet hardware is also concerned by the PROOFS workshop: in this context, the hardware is indeed analyzed in its HDL form, which is a concurrent language, hence that can be seen as a piece of software.