Formal verification for security and attacks in IoT physical layer

IoT devices are more important than ever. In a connected world, IoT devices have many uses. They are no longer merely used at work; they are part of our everyday lives. Security concerns arise if the devices generate, collect, or process sensitive data. Physical layer security controls are the cornerstone once the risk for humans increases when physical security fails. To achieve security in IoT devices, preventing is better than detecting. Formal verification is an important and valuable tool for detecting possible vulnerabilities and ensuring data security. Thus, this paper proposes an Event-B proof-based formal model of IoT physical layer security and attacks from the requirements analysis level to the goal level. Our model is built incrementally using a refining method during design and verification. We present a three-level formal approach: first, the construction of the IoT physical layer; then, we check for IoT physical layer vulnerabilities by processing the lack of some characteristics that cause these vulnerabilities, such as speed, typical bandwidth, and power consumption; lastly, we detect physical layer attacks like jamming and MAC spoofing, which helps to build security proofs. Our approach uses an electrocardiogram (ECG) IoT system as a case study, and as an additional case study to back up the proposed method’s generalizability, we used a fire alarm system. Also, we use the proof obligations and the ProB animator in the Rodin model checking tool to check and validate our approach.