PROOFS: Security Proofs for Embedded Systems


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:

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

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.

Formal Methods for Security

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

  1. Formalization of the system, since it must be captured unambiguously with a formal paradigm to be processed;
  2. 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.



Secure-IC S.A.S.