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 the CADP Web 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

Back to the CADP case studies page