Database of Case Studies Achieved Using CADP

Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks

Organisation: Tiempo SAS
CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG

Method: LNT
EXP
SVL

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: 2019-2020

Size: 706 lines of LNT
269 lines of EXP
269 lines of SVL

Description: 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.

Conclusions: 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 benchmark.

Publications: [Mateescu-Serwe-Bouzafour-Renaudin-20] 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

Contact:
Wendelin Serwe
Inria Grenoble - Rhône-Alpes / CONVECS team
655, avenue de l'Europe
38330 Montbonnot Saint Martin
France
Email: Wendelin.Serwe@inria.fr



Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Mon May 25 09:49:00 2020.


Back to the CADP case studies page