CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG
CADP (Construction and Analysis of Distributed Processes)
706 lines of LNT
269 lines of EXP
269 lines of SVL
The number of connected devices that make up the IoT (Internet of
Things) already exceeded 20 billion, and is constantly increasing.
However, a study of Hewlett Packard indicates that 90% of the objects
collect and thus potentially expose data, that 80% of the objects do
not use identification and source authentication mechanisms, and that
70% do not use a mechanism of encrypting the transmitted data.
These vulnerabilities open the way to DDoS (Distributed
Denial-of-Service) attacks, which exploit over 100,000 infected
devices (e.g., cameras, video recorders, etc.) to overload various
services and websites with a deluge of data. Therefore, strengthening
the security of connected devices is a critical issue.
The SECURIOT-2 project, led by Tiempo Secure, aims at developing a SMCU (Secure Micro-Controller Unit) that will bring to the IoT a level of security similar to banking transactions and transport (smart cards) and identification (electronic passports). Besides ensuring the necessary security services (key management, authentication, confidentiality and integrity of stored/exchanged data), the SMCU needs a power management scheme adequate with the low power consumption constraints of the IoT. Given these constraints, a natural implementation of an SMCU is by means of asynchronous circuits, whose components are not governed by a clock signal, but operate independently, on an on-demand basis. Compared to classical synchronous circuits, this functioning has the potential for lower power dissipation, more harmonious electromagnetic emission, and better overall timing performance.
In this study, we consider the so-called shield, a particular asynchronous circuit designed and patented by Tiempo Secure for the protection of another (asynchronous) circuit against certain physical attacks (e.g., cutting a wire, setting a wire to a constant voltage, and introducing a short-circuit between two wires). We consider the modeling and analysis of the shield at two abstraction levels. First, at circuit level, we take into account only the components of the circuit and their interconnection, without modeling the implementation details of these components. This level is appropriate for reasoning about the desired properties of the shield, namely the detection of physical attacks. The regular structure of the shield (serial pipeline) enables to apply inductive arguments to reduce all possible attack configurations to a finite set, which we analyzed exhaustively. Next, we undertake a gate level modeling, focusing on the implementation of a component in terms of logical gates. Here we explore a range of different modeling variants for gates, electric wires, and forks (isochronic or not), and analyze their respective impact on the faithfulness of the global circuit model, the size of the underlying state spaces, the expression of correctness properties, and the overall ease of verification. The modeling was carried out using the LNT and EXP languages of CADP, and the overall analysis process was implemented using SVL scripts.
By modeling and analyzing the shield circuit using CADP, we found that
they can provide the designer with valuable information, such as the
necessity to ensure isochrony of forks. For circuit-level analysis,
we used an induction proof to extend results of our attack analysis
to a shield of arbitrary size. Also, due to their extensibility and
state space size, the LNT models of the shield provide a challenging
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin.
Modeling an Asynchronous Circuit Dedicated to the Protection Against
Physical Attacks. In Proceedings of the 4th Workshop on Models for
Formal Analysis of Real Systems MARS'2020 (Dublin, Ireland),
EPTCS 316, pp. 200-239, 2020.
Available on-line at: http://cadp.inria.fr/publications/Mateescu-Serwe-Bouzafour-Renaudin-20.html
or from our FTP site in PDF or PostScript
Inria Grenoble - Rhône-Alpes / CONVECS team
655, avenue de l'Europe
38330 Montbonnot Saint Martin
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|