Software — Stack — for Massively Geo-Distributed Infrastructures

logo IMT Atlantique logo inria logo LS2N

Paper accepted to Journal of Reliable Intelligent Environments -

Formal verification for security and attacks in IoT physical layer

ZinahHussein Toman, LazharHamel, Sarah HusseinToman, Mohamed Graiet, DaltonCézaneGomes Valadares

IoT devices are more important than ever. In aconnected world, IoT devices have many uses. They are no longer merely used atwork; they are part of our everyday lives. Security concerns arise if thedevices generate, collect, or process sensitive data. Physical layer securitycontrols are the cornerstone once the risk for humans increases when physicalsecurity fails. To achieve security in IoT devices, preventing is better thandetecting. Formal verification is an important and valuable tool for detectingpossible vulnerabilities and ensuring data security. Thus, this paper proposesan Event-B proof-based formal model of IoT physical layer security and attacksfrom the requirements analysis level to the goal level. Our model is builtincrementally using a refining method during design and verification. Wepresent a three-level formal approach: first, the construction of the IoTphysical layer; then, we check for IoT physical layer vulnerabilities byprocessing the lack of some characteristics that cause these vulnerabilities,such as speed, typical bandwidth, and power consumption; lastly, we detectphysical layer attacks like jamming and MAC spoofing, which helps to buildsecurity proofs. Our approach uses an electrocardiogram (ECG) IoT system as acase study, and as an additional case study to back up the proposed method’sgeneralizability, we used a fire alarm system. Also, we use the proofobligations and the ProB animator in the Rodin model checking tool to check andvalidate our approach.