1 Introduction

The Internet of Things (IoT) is a term that refers to physical things connected to the Internet and their virtual representation. It includes not just human participation but also “Things”. The IoT promises to bring new services to people in all aspects of our society. It intends to deliver pervasive connection and data collection capabilities across the home, vehicle, and industrial environments. Hundreds of billions of physical objects are equipped with various sensors and actuators and connected to the Internet through heterogeneous communication systems [1]. In a typical IoT scenario, sensors collect data using smart devices, process these data using controllers to make decisions, and then transmit this information to devices or people for execution [2].

The difficult challenge in this context is verifying and ensuring the functionality, security, and confidentiality of the IoT despite the present and hidden vulnerabilities of connected things and the expanded ineffectiveness of cyber-security.

In the technology field, IoT security has become an essential topic of conversation [3]. Security weaknesses, technical limits, and software vulnerabilities are among the significant challenges for this technology to take hold in essential applications. Whether innocent or malicious, human error is the most common cause of security vulnerabilities [4]. Moreover, detecting online cyberattacks on IoT devices is challenging due to their limited battery life and computational power. Therefore, we need an alternative method of reducing the attack surface to decrease the threat of an attack. This method would necessitate more powerful security testing on the device prior to deployment. For this reason, in this paper, we focused on the attacks and security of the IoT’s physical layer using formal methods.

In physical layer security for IoT systems, the secrecy rate is the speed at which information can be sent secretly from the source (an IoT device) to its intended destination through communication channels [5]. Using its properties, the physical layer may also provide information-theoretic security, even if the attacker has infinite processing power [6]. IoT devices and communication channels are easy targets for attackers because of their spread-out nature. Many of these devices and protocols also have limited resources, which makes them even more vulnerable. Because they do not get updated often, many of these devices can be hacked or attacked in other ways [7].

The attacker must have physical access to the device or cause a fault in it to stop it from working and get secret information from its side channels, such as how much power and energy it uses, how much radiation it puts out, and how long it takes to run. An attacker may cause a competing action to be performed on the same item or feature of the environment. This is called a cascade attack [8]. Attackers could use these problems and vulnerabilities to gain physical access to IoT devices.

In this paper, we focused on the attacks on the IoT physical layer, such as jamming and MAC spoofing [9]. Jamming is a type of denial of service (DoS) attack in which hostile nodes interfere on the networks to stop legal communication from happening. For instance, an enemy can use the same frequency as the IoT device to stop the communication between IoT devices and gateways. Spoofing is another sort of assault that sends out a false signal. A MAC spoofing attack can make a node appear legitimate. MAC spoofing is the modification of a network interface controller (NIC) card’s MAC address.

Preventing security breaches in IoT devices is an alternative to detecting them [10]. This prevention necessitates a reduction in the number of possible attack paths. Promising design approaches, secure coding, static analysis, and comprehensive testing have traditionally been used to accomplish this. However, the security of these methods cannot be guaranteed, and hence, more robust techniques are required. The formal verification application to ensure security is a promising direction, making sure that a design is correct using some mathematical and logical methods.

In the IoT, formal methods are used to do many tasks that directly relate to our everyday lives. They also validate security guarantees and real-time attributes for a given model. Through formal methods, mathematics and logic can be used to check and specify the accuracy of designs. The correct code can be created or implemented from the design once a suitable design has been established [11].

So, this paper proposes a new formal model of IoT physical layer security and attacks based on the Event-B proof-based formal model. Event-B offers rigorous mathematical reasoning that aids in developing software with greater confidence. This model goes from the abstract to the target level incrementally using the refinement method. We outline the paper’s major contributions below:

  • We propose a formal approach to representing the physical layer of an IoT system.

  • We verify the lack of IoT physical layer vulnerabilities as they are essential for formal verification due to their crucial use in conjunction with security-sensitive features of the device. As a result, complete testing of devices and attack detection becomes realistically difficult.

  • We use formal verification to detect physical-layer attacks like jamming and MAC spoofing. Formal verification is of great assistance in establishing security proofs.

To verify that the IoT physical layer model is both functional and accurate, we incorporated an electrocardiogram (ECG) IoT system into our model and we tested the model’s events to prove there is no problems at any level. The fire alarm system is used as another case study to prove that the proposed method can be applied to a wide variety of situations. We made use of the Rodin model checker and proof obligations. This paper’s remaining sections are structured as follows: Sect. 2 introduces related works; Sect. 3 describes the concept of IoT, Physical layer security and attacks and gives an outline of Event-B theories; Sect. 4 Offers apropsed model and motivating examples; Sect. 5 presents the formalization of IoT physical layer in the Event-B model; Sect. 6 proposes a verification and validation of our approach and Sect. 7 concludes this paper.

2 Related work

For a number of years, a considerable amount of work has been spent on studying IoT technology. However, the majority of contributions focus on using formal methods in IoT physical layer security. This subsection provides a chronologically ordered literature evaluation of some of these publications. In this study [12], the authors suggested a safety protocol to address the security weaknesses in medical IoT communication. The suggested software-based communication protocol utilized inter-device cross-authentication and encryption to prevent a variety of attacks, and it was validated with Casper/FDR, a formal verification tool for processes. The results of the test showed that the proposed protocol makes sure that wireless connections between medical devices are safe. In [13], the authors came up with a new way to combine the security parts of IoT devices while taking into account their non-functional properties. A technique and a software tool were used to check the information flow security policy. Attention was paid to certain types of differences between the rules, sensors were tested for strange data, and a few types of security component conflicts were found. The SPIN tool and the PROMELA language were used to check the data flows in a network, verify the security policy, and prove that the method was sound.

It was introduced in [14, 15] new formal modeling by integrating previous formal methods to model actors, devices, and policies of human-centric infrastructures for IoT healthcare systems to investigate security and safety threats. The authors utilized Isabelle, an interactive theorem prover that provides modeling and evaluation of human-centric infrastructures by means of attack path analysis.

The primary contribution made by the authors of this research [16] was the proposed multi-factor remote user verification protocol. Passwords, smart devices, and biometrics are all used in this scheme to ensure the safety of user identities. The authors then presented a formal and informal security analysis of the protocol. Finally, other protocols’ computational and communication abilities were compared. The research in [17], presented a method that employs time-aware computations to allow the controller to assess the quality of the entered data. In industrial automation applications, the Cyber-Physical Agnosticism (CPA) property of the Internet of Things (IoT) is verified through formal verification. To simplify the structure of the SMV model, an abstract model of the facility was developed, consisting of four instances of state machines, one elevator car, and three doors. The model of an abstract plant is turned into the SMV language and the NuSMV model checker.

The Secure Swarm Toolkit (SST) was introduced in this paper [18], the authors create to facilitate the development of an IoT authorization service infrastructure. As a result of SST’s flexible security options, we anticipate that a wide variety of IoT devices, from sensor nodes to electric power grid control systems, will be able to be integrated into the authorization infrastructure. This research used the automated verification tool Alloy Analyzer to conduct a formal analysis of the system’s security.

To automate verification and probabilistically quantify attack probabilities against standard IoT system configurations, the study in [19], introduced a novel IoT Risk Analyzer framework. One can accurately assess the root cause and severity of security risks with the help of a formal model-driven verification approach, which checks all possible behaviors of the reference model in a finite state space. The proposed framework generates MDP models, which are then used by the PRISM model checker to perform automated analysis of system-level risk profiles.

In this work [20, 21], centered on utilizing the Shibboleth protocol for secure data access and outsourcing in a cloud-IoT network. This research proposes the Shibboleth-based Fog-IoT network, which includes Shibboleth to ensure security between Fog Client and Fog Node. The authors formally validated Shibboleth using High Level Petri Nets (HLPN), a mathematical and graphical modeling tool, to demonstrate the correctness of Shibboleth with respect to specific security properties. In addition, the Z3 SMT solver was used to analyze the rules of data flows, proving the system’s correctness versus the three security properties. The purpose of this paper is to present a new method that uses the Event-B modeling approach to overcome these verification limitations by modeling systems with abstraction. In comparison to earlier works, while there is a dearth of research to verify the IoT systems that deal with the physical architecture of IoT layers with security and attacks.

Our proposed model integrates modeling and verification of physical layer security and attacks in the IoT, to the advantage of working in both fields, thus contributing to their development. In this paper, we present new work in four ways: we propose a formal verification of the IoT physical layer; we check that the IoT physical layer does not have any security holes; we find physical-layer attacks, and our work is based on a formal model. Table 1 compares existing studies to our methodology based on a similar topic, methodology, and domain.

Table 1 The comparison of existing research studies with our approach
Full size table

3 Background

3.1 IoT concept

The term “Internet of Things” (IoT) is currently a hot topic. Kevin Ashton, who worked for Procter and Gamble, came up with the term in 1999 to describe how he put RFID tags and sensors on items in the supply chain [22]. Since then, RFID has gotten a lot of attention in academia and business. IoT is primarily concerned with the idea of connecting things to a network without human involvement, which facilitates the exchange and gathering of data throughout the network. This is done by connecting gadgets and “things” to the Internet and other networks in different ways. Many things are connected to each other through their built-in actuators and sensors, which can sense their surroundings and gather data, which is then sent to the next IoT layer. This section provides a basic overview of the various IoT layers [23, 24].

  1. 1.

    Physical layer: Sensors, actuators, and devices make up this layer. Sensing systems detect IoT environment parameters. It turns sensing technologies’ physical data into digital signals for communication and transmission. When some objects are not perceived, embedded sensors can help. So, embedded sensors help the perception layer by processing data at end devices.

  2. 2.

    Transport layer: Sensor data from the perception layer can be transferred to the middleware layer via wired or wireless communication routes, and the reverse is also true.

  3. 3.

    Middleware layer: Functions in a critical way. An enormous amount of data is received by this layer from the transport layer and processed by this layer. This layer can also be used to manage and control access to the devices and to find new ones.

  4. 4.

    Application layer: Application service delivery, which originates from the middleware layer and is delivered to various applications, is the responsibility of this layer. Smart cities, smart homes, smart healthcare, etc. are only a few examples.

As a basis for our work, we retrieved the physical layer in this paper (see Fig. 1). So, to construct an efficient and dependable IoT physical layer formal model, we must first extract the appropriate architectural criteria for this layer. The Table 2 illustrates the functional needs that will be utilized in our formal model:

Fig. 1
figure 1

The IoT system layers architucture

Full size image
Table 2 The physical layer requirements
Full size table

3.2 Physical layer security and attacks

3.2.1 Physical layer security

The physical layer is the foundation of all security controls. Other security measures can fail without causing a disaster, but when physical security fails, people are usually left completely open to danger [4]. Physical layer security in the IoT has only recently emerged as a solution for enhancing IoT system security. For the first time, privacy is achieved using the physical layer of the network system instead of traditional cryptographic methods like interference and channel security, as well as thermal noise and other things.

Physical layer security in the IoT has only recently emerged as a solution for enhancing IoT system security. Since many sensors and actuators are resource-restricted, it is difficult to incorporate security in IoT systems. This kind of security does not rely on encryption but on the physical aspects of wireless channels, such as fading, noise, interference, and so on [4]. Security is guaranteed by Physical layer security, regardless of the eavesdropper’s computational power. So, it is becoming a good alternative or addition to hard-to-understand cryptographic algorithms for secure communications in the IoT [25].

In the physical layer, vulnerabilities are directly related to physical access to networks and devices, such as unauthorized network access, data damage, and keystroke logging. An attacker may use one or more of the following physical layer security vulnerabilities to compromise IoT devices [26]:

  1. 1.

    There may be a flaw in a device’s functionality. For example, an operation that was supposed to be there but was either left out or only partly done.

  2. 2.

    Even if the necessary security actions have been implemented in the device, implementation defects may exist. Such a defect can be an issue with cryptographic algorithms in particular.

  3. 3.

    Programming bugs like format-string vulnerabilities, buffer overflows, and arithmetic overflows and underflows can be used to make malicious payloads that stop execution and break security.

  4. 4.

    Attackers can trick other users or devices by putting fake code or data into a fake IoT device that has been added to the network.

  5. 5.

    IoT devices are subject to fault injection, differential power analysis, and timing assaults. For these attacks to work, the attacker must have physical access to the device, cause a fault, or passively watch side-channel measures like power and energy consumption [27], electromagnetic radiation, execution time, speed [28], and bandwidth [29]. So, all these vulnerabilities are related to IoT system efficiency and security.

The Fig. 2 show some proposed characteristics that cause the IoT physical layer vulnerabilities in our model, Table 3 lists the formal model requirements that must be specified in our model.

Fig. 2
figure 2

The proposed characteristics that cause the IoT physical layer vulnerabilities in our model

Full size image
Table 3 The physical layer security requirements
Full size table

3.2.2 Physical layer attacks

Physical layer security studies fall into three categories [30]. The first is eavesdropping. Illegally receiving or listening to a lawful signal, the transmitter or receiver cannot detect it since the eavesdropper is passive. The second is active attacks, like jamming. A jammer disrupts the communication providing a signal to a receiver when a transmitter sends a signal. Jamming prevents the receiver from decoding the legitimate signal. The third type of attack is spoofing, in which a person or program pretends to be someone else, getting access to sensitive information, enter the systems, steal money, or spread malware. Here, we categorize security attacks primarily in IoT physical layer as jamming and MAC spoofing attacks. They are listed below.

  • a-jamming attack

Jamming attacks are a type of denial of service (DoS) attack in which hostile nodes intentionally interfere with networks to stop lawful communication. Attackers plant jammers to interfere with wireless networks. Depending on how they plan to attack, jammers can have the same or different abilities as real network nodes. When a transmitter detects a busy wireless medium or a damaged signal received at a receiver, it will back off. A jammer can jam a network in multiple ways for maximum effectiveness. A jammer’s function determines whether it’s basic or advanced [31]. It divided the elementary jammers into proactive and reactive subgroups. The advanced kinds are function-specific and smart-hybrid. In the past, this method was used for both mobile frequency jamming and RF frequency jamming for WSN nodes (see Fig. 3).

Fig. 3
figure 3

The jamming attack

Full size image

IoT devices employ wireless connections to program, receive user instructions, or transmit data to the cloud. An adversary can jam communication between IoT devices and gateways using a frequency that is identical to that of the IoT device. IoT systems are vulnerable to jamming attacks that can cause the batteries of target devices to deplete quickly by disrupting their data transfer and forcing them to retransmit repeatedly [32]. If the attacker believes that there will be a successful transmission, they will jam the data transmission in such a way that the receiver will not be able to decipher the data that has been sent.

  • b- spoofing attack

In an IoT access network, identity spoofing attacks can be easily launched. An attacker who uses identity spoofing can pretend to be another real IoT device using the real user’s MAC (media access control) or IP (internet protocol) address as a fake ID [33, 34]. Spoofing attackers have an advantage in transmitting the deceptive signal to the receiver because they can do it at higher power. At this time, it is impossible for an attacker to be in the same physical place as a victim. Because the victims’ secret keys may have already been compromised by the attackers, cryptography-based authentication is unlikely to be effective. Attackers might be stationary or on the move.

The objective is to fool the recipients. Spoofing can be performed in two situations: (a) when the transmitter stops transmitting the signal, the spoofer can begin transferring a deceiving signal to the receiver; and (b) during the transmission phase between transceivers, the spoofer can transmit the deceiving signal with increased power to the receiver [34]. So, the receiver takes the spoofing signal as a real signal and ignores the real signal coming from the transmitter.

By forging a node’s MAC address, a MAC spoofing attack can make it look like a valid node [35]. Mac spoofing is the act of modifying the MAC address on a network interface controller (NIC) card. The MAC address is “burnt in” during manufacturing. Consequently, each network card leaves the factory with a unique MAC address. An attacker can acquire access to data by redirecting a device to another device. In reality, a spoofing attack is a Computer identity theft, is relatively simple. In reality, a spoofing attack is a simple way to steal someone’s identity on a computer. This can be done for good or bad reasons (see Fig. 4). Table 4 lists the formal model requirements that must be specified in our model.

Fig. 4
figure 4

The MAC spoofing attack

Full size image
Table 4 The physical layer attacks requirements
Full size table

3.3 An Event-B method

Event-B is a formal method for discrete system modeling based on the B-Method and developed from the idea of action systems. It’s been employed in safety–critical systems [36]. For the correct-by-construction evolution of reactive systems, it depends on first-order logic, typed set theory, and integer arithmetic. The ability to develop correct-by-construction system designs is a significant characteristic of this method. The remaining effort is to develop or implement the right code from the correct design once it has been determined. Event-B is currently centered on the concept of events in general, which is also seen in other formal approaches such as Action Systems [37], TLA [38], and UNITY [39].

In terms of CONTEXT and MACHINE, the Event-B model is made up of static and dynamic parts.

  • The CONTEXT FILE: describes the model’s static parts. It is a type of first-order theory that provides CONSTANTS declarations that are either sets (are types defined by the user) or numbers. Constants are declared within a context, and Axioms and Theorems specify their attributes and connections. An AXIOMS is a statement of a property that cannot be inferred from another axiom. THEOREMS define characteristics that should be derivable from the axioms. The Context structure is:

figure a

-The MACHINE: implements the dynamic part of the model, It uses constants and axioms that are imported from context via the SEES clause to define the dynamic structure or system evolution. The machine must describe: The system’s state via a collection of VARIABLES, The state’s consistency via a set of INVARIANTS, and, A few EVENTS to specify the machine’s probable state evolutions. Every event is expressed in the following format:

ANY parameters WHEN guards THEN actions END.

The guard specifies the required condition for an event to occur. If there is a value for its parameter that causes its guard to hold in this state, the event is said to be enabled in that state. When an event occurs, the action explains how the state variables change. The machine’s structure is

figure b

The key benefit of using Event-B is that it enables models to evolve iteratively through methods such as context EXTENDS and machine REFINEMENT. This is the primary characteristic of Event-B. With the help of these technologies, users can build systems based on their abstract specifications, and they can then add more details about how the systems will work [40]. In other words, a machine can be “refined” by another machine, and a context can be “extended” by another context. A machine can also “see” a single context or a number of contexts. In Fig. 5, relationships between the machine and the context are shown. Machines and contexts must adhere to the following visibility rules:

Fig. 5
figure 5

An Event-B project structure

Full size image

4 Proposed model and case studies

4.1 Proposed model

Building a secure, dependable, and error-free IoT system and ensuring its correct operation is a challenging endeavor. In actuality, constructing IoT systems can present a number of challenges. So, for this reason we proposed our model, which proposes a new formal model of IoT physical layer security and attacks that is based on Event-B (see Fig. 6):

Fig. 6
figure 6

Proposed model

Full size image
  1. 1.

    A formal approach to constructing IoT physical layer:

    IoT system contains “Things” which are entities or physical objects that can be uniquely identified, have an embedded system, and share data via a network. Our proposed model requires that all “things” (i.e., entities) have to identify information (such as a name, a type, a location, and properties). IoT parts include things like gadgets, sensors, and motors (each “thing” represents one component). The physical layer’s main job is to get information from the environment. We can add sensors and actuators and use information from any IoT device.

  2. 2.

    Security Model:

    We would verify the IoT physical layer vulnerabilities and monitor IoT’s system by suggesting a formal approach in several aspects: (a) assign administrator: IoT device and network monitoring by a person or more than one is helpful in lowering security vulnerabilities and risks; (b) use a strong and unique password: make sure each password you use is secure and different; (c) regular check for updates: monitoring the status of software updates for IoT devices regularly;d - monitoring baseline of devices: (i) typical bandwidth: check the functionality of any devices whose bandwidth needs are less than the threshold or are the same as reported by Orsini et al. [41]; (ii) power consumption: check the functionality of any devices whose power consumption needs are less than the threshold or are the same as reported by Prieto et al. [42]; (iii) speed: check the speed of devices that are connected to the IoT system [43].

  3. 3.

    Attacks Model:

    Two types of attacks (jamming and MAC spoofing attacks) are proposed to formally verify the IoT physical layer:

    • The jammer continuously scans the wireless channel and emits a signal that disrupts any radio activity it detects. Specification of a power threshold to distinguish channel noise from ongoing transmissions. If the estimated received power exceeds the threshold, a jamming signal is transmitted. If the estimated received power is below the threshold, there is no interference.

    • MAC addresses are assigned to every network-connected device (network card). The MAC address of the attacking device must be distinct from the sender and receiver. By rerouting a device (destination device) to another device, an attacker can gain access to its data (attacker device). Spoofing will occur if the attacker’s address corresponds to the destination address. Aside from that, nothing would occur.

4.2 Case studies

To better understand our model, we’ll use an IoT system for electrocardiogram (ECG) monitoring in this section. real-time Monitoring of Electrocardiograms (EMoNet) [44]. It’s a smart city network made up of patients with heart conditions and a slew of ambulances, smartwatches, and other wearable ECG sensors. EMoNet’s flow diagram is shown in Fig. 7, which shows an individual patient’s three-minute timed job. It mostly involves getting an electrocardiogram (ECG) and figuring out what it means, as well as calling an ambulance if the patient shows signs of a heart attack.

Fig. 7
figure 7

An overview of the electrocardiogram (ECG) system

Full size image

There are four components to electrocardiogram (ECG) monitoring, and each things in an IoT system reflects one of the following components:

  1. 1.

    Smartwatches (smartwatch): provides the ECG Analysis.

  2. 2.

    Wearable ECG Sensor (Wearable): provides the Heart Rate History.

  3. 3.

    Healthcare Cloud (Cloud): offers emergency service.

  4. 4.

    Ambulance (Ambulance): provide Assistance.

The control flow is triggered at regular intervals by ECG Analysis (smartwatch), which then passes control to Heart Rate History (Wearable) to obtain the most recent sensor reading. Then, ECG Analysis regains control once Heart Rate History hands it back to it. In the event that there are indications of a heart attack, control is transferred from ECG Analysis to the emergency service by Healthcare Cloud (Cloud), which then transfers control to the assistance service of the closest ambulance (Ambulance). After going via the emergency services, control is handed back to the ECG analysis. The physical layer consists of all four components used to represent things [45].

To meet the aforementioned requirements, we present in this study a formal approach to modeling electrocardiogram (ECG) monitoring based on the Event-B method. The Event-B specification, with its formal syntax and semantics, is capable of validating the behavior of created models through the execution of multiple verification features.

To support the generalizability of the proposed method, we test another scenario by checking the IoT system-based fire alarm.

Second Scenario. In the second scenario, there are six components to Fire Alarm System that represent the things in an IoT system:

  1. 1.

    Smoke detecting (SmokeDet).

  2. 2.

    Temperature Sensing (TempSens).

  3. 3.

    Gas Detection (GasDet).

  4. 4.

    Fire Analysis (FireAnaly).

  5. 5.

    Alarm Control (AlarmCont).

  6. 6.

    Water Sprinkling (WaterSpr).

It is begins by collecting data from two types of sensors: smoke detectors (SmokeDet) and temperature sensors (TempSens). Fire Analysis (FireAnaly) will begin its work once it has received real-time data from the preceding sensors. The fire analysis is responsible for analyzing the data received from smoke detection and temperature sensors and comparing it to a predetermined threshold to determine whether or not there is a fire. When a decision has been reached, alarm control (AlarmCont) and water sprinklers (WaterSpr) are activated. Thus, alarm bells and water sprinklers have been developed simultaneously [46]. In Sect. 6, we show how our model can be used with the two case studies.

5 Proposed model for formalization IoT physical layer in Event-B

In this section, our strategy for formalizing the physical layer of IoT systems in terms of security and attacks is described. The IoT physical layer formal model, as shown in Fig. 8, consists of an abstract model and two refinements. We begin by modeling the physical layer in the abstract model, then refine it to model the physical layer security, and refine it again to represent the physical layer attack.Model three contexts and machines is what we’re proposing to do.

Fig. 8
figure 8

Mapping between proposed model and Event-B model

Full size image

5.1 Physical layer structure model

This section describes in detail how the abstract model was constructed. The structure of the physical layer is represented by the abstract model. The primary contribution of this model is a formal way to build the physical layer of an IoT system (see Fig. 9). It is made up of the context and the machine, as detailed bellow:

Fig. 9
figure 9

Physical model

Full size image

A. Specifications

Here are the IoT physical layer requirements rewritten for the abstract model. The contents of the IoT physical layer are specified by the first three. The following four represent the model events that describe the behavior of this layer as illustrated in Table 5.

Table 5 Specifications of requirements in a model
Full size table

B. Context

IOT-physical is the initial context for the IoT physical layer in the Event-B model. Sets (clause SETS) that describe different notions of an abstract model, such as defining IoT things as (thing, thing name, thing type, thing properties, and thing location), are included in the collection. The names of the fields of variables that are relevant to this kind of data are things like nameset, typeset, proset, and locatset. Also, the description of the containing physical layer includes things like sensors, actuators, devices, and data with the set names SENSOR, ACTUATOR, DEVICE, and DATA. The AXIOMS illustrate the characteristics of the qualities whose values were derived from the SETS. In this scenario, the axm1, axm2, and axm3 variables are introduced so as to stipulate that all of the defined sets of things, SENSOR, and ACTUATOR, are, in fact, finite (see Fig. 10).

Fig. 10
figure 10

An Event-B model for IoT architecture: the context (1)

Full size image

C. Machine

The”physical layer” machine is in charge of most of the ideas in the physical layer. It is made up of a group of things, each of which has a physical part that is represented by sensors, actuators, and devices (that meet the Phy1 and Phy2 requirements). The gathering of information from the environment of IoT devices is this layer’s primary responsibility. In other words, the machine is represented by the clause SEES in the preceding context of IOT-physical, which is the first machine in the Event-B model for the IoT physical layer, as shown in Fig. 11. As a next step, we created a set of variables to represent the abstract model’s components. Phy-Req1 is a representation of each thing that has a name, a type, properties, and a location, and the invariants inv1, inv2, inv3, and inv4 describe this. Phy-Req2 is modeled using the following: inv5, inv6, and inv7. The data variable is defined as a subset of the data set by this machine (invariants inv8). This is followed by the model of the sensor Phy-Req3 by the invariant inv9.

Fig. 11
figure 11

An Event-B model for IoT architecture: the machine (1)

Full size image

The first event in the abstract model, the addData event, is used to add data from any IoT device that meets Phy-Req4 and is included in the data set (grd1) but not in the data set (grd2), and then added to the data set (act1). In a manner analogous to this event, the addSensor and addActuator events include the addition of one or more sensors and actuators, respectively, that satisfy Phy-Req5, and Phy-Req6 as shown in Fig. 12.

Fig. 12
figure 12

The events of adding data, sensor, and actuator for IoT architecture

Full size image

In the physical layer of an IoT structure, sensors or other devices are used to gather data from the IoT environment. The collectDataSensor event tells us what this function is, and Phy-Req7 is modeled to match (see Fig. 13).

Fig. 13
figure 13

The collectDataSensor event for IoT architecture

Full size image

5.2 Physical layer security model

In this model, we’d check for any IoT physical layer vulnerabilities, such as weak passwords and outdated systems, and we’d examine the baseline (speed, normal bandwidth, and power consumption) to make sure there aren’t any. Because they are used in conjunction with security-sensitive functions on the device, IoT physical layer vulnerabilities hold a special place in the formal verification process. Complete device testing and attacks detection are therefore made more challenging. During Event-B, the Physical layer is brought in by a refining of the process (see Fig. 14). Therefore, we will develop a second level of abstraction that will further refine the first level.As illustrated below:

  1. A.

    Specifications:

Fig. 14
figure 14

Security model

Full size image

The following are rewritten requirements for the first refinement to describe some of the IoT’s physical layer vulnerabilities that cause insecurity to the system. As illustrated in Table 6.

Table 6 Specifications of requirements in a model
Full size table
  1. B.

    First Refinement:

In this section, we extend the structure of the physical layer to the formalization we made in the previous section. So, that physical layer security can be shown in a formal way using the refinement concept of Event-B by adding a variable and five new events: updateChecking, passwordChecking, bandwidthMonitoring, powerMonitoring, and speedMonitoring, (see Fig. 15).

Fig. 15
figure 15

An Event-B model for IoT physical layer security: the machine (1)

Full size image

According to our proposed for this model, we illustrated the more effective vulnerabilities in IoT physical layer.

  1. 1.

    1-Put someone in charge of managing everything. Having a person who acts as the administrator of all of the devices connected to the internet of things as well as the network can help reduce the number of security oversights and vulnerabilities. In our model, the administrator is represented by the variable admin, which is shown as the invariants inv1 and inv3. It is set up to assign a system administrator that satisfies Sec-Req1.

  2. 2.

    2-Make sure all of your passwords are strong and unique. Many cyberattacks can be thwarted with the use of strong passwords. A password manager is a piece of software that makes it easier for users to set secure passwords and keep them safe within the application they use, this is modeled Sec-Req2 and Sec–Req3.

  3. 3.

    The invariants (inv4 and inv5) serve to specify the system password. And, we suggest adding a Checking password to check if it is strong or weak password. This is modeled by the event passwordChecking as shown in Fig. 16 where a component hasStrongPassword is checked by another variable check_password (Guards grd1, grd2, and grd3).

  4. 4.

    3-Check updates on a regular basis. The Internet of Things (IoT) is plagued by numerous security flaws. This is due to the fact that IoT devices can be vulnerable at any level. Cybercriminals are still using old flaws to infect devices, which shows how long devices can stay online without being fixed. This part is modeled by Sec-Req4. Variable check_update and IsUpdate are defined in invariants inv8 and inv9, respectively. which represents an enablement of the specification of the system’s update.So, An event with the name updateChecking is created to model the system’s checking for updates (set grd1 and grd3) and ensuring that they are present (set act1) (see Fig. 17)

  5. 5.

    4-Monitor the device’s baseline operation which satisfied Sec-Req5. It might be difficult to identify cyberattacks. The baseline behavior (speed, typical bandwidth, power consumption, etc.) of devices might assist users in spotting changes that may indicate malware infections. In this model, we suggest to adding a variable and three new events to monitoring the device behavior: bandwidthMonitoring, powerMonitoring, and speedMonitoring.

Fig. 16
figure 16

The passwordChecking event for physical layer security

Full size image
Fig. 17
figure 17

The updateChecking event for physical layer security

Full size image

- Each IoT device has a standard bandwidth barrier the(bandwidth threshold). The invariants inv11, inv12 and inv13 define how to model the bandwidth (BANDWIDTH). It must be a number, and each device has to have it (device_bandwidth) and have a threshold (bandwidth_threshold), respectively which models the requirement Sec–Req6. The event (bandwidthMonitoring) is designed to model the monitoring of the state bandwidth of any devices that require less or the same amount of bandwidth as the threshold set (grd1, grd2, and grd3), and to decide the state (act1) that satisfies Sec-Req7 (see Fig. 18).

Fig. 18
figure 18

The bandwidthMonitoring event for physical layer security

Full size image

- Power consumption limits the battery life of portable devices like cell phones and laptop computers. For each IoT device has a standard power consumption, set (inv17), which models the requirement Sec–Req6, and the (inv15 and inv18) define the power consumption of device. (grd1, grd2, and grd3) are meant to model the monitoring of state power consumption in any devices that need less or the same amount of power as the threshold set by the event (powerMonitoring) and to decide the state (act1) that meets Sec-Req9 (see Fig. 19).

Fig. 19
figure 19

The powerMonitoring event for physical layer security

Full size image

- Devices connected to the IoT network can be monitored for their current speed. The (inv19 and inv20) models the requirement Sec–Req10 regarding the device speed (device_speed), and device state (speed_state). The (speedMonitoring) event is utilized to monitor the speed status of the device. Every IoT device has a speed within a particular range set (grd1 and grd2), then the speed state is checked (act1), as shown below (Fig. 20).

Fig. 20
figure 20

The speedMonitoring event for physical layer security

Full size image

5.3 Physical layer attacks model

In this model, we used jammer and MAC spoofing attacks as our models for the more significant IoT physical layer attacks, as shown below (Fig. 21).

  1. A.

    Specifications:

Fig. 21
figure 21

Attacks model

Full size image

The following requirements for the second refinement have been rearranged to describe some of the attacks on the system that use the IoT’s physical layer according to our model. Table 7 shows a structure that can be used to get physical layer attack parameters from the proposed method.

Table 7 The physical layer Attacks requirements
Full size table
  1. B.

    Second Refinement

This part shows the second refinement to the IoT physical layer model, which is attacks on the physical layer. This refinement adds the physical layer representations for the jamming and MAC spoofing attacks to the formalization that was made for the abstract model in the last refinement. That is illustrated in Fig. 22.

Fig. 22
figure 22

An Event-B model for IoT physical layer attacks: the machine (3)

Full size image

- Jamming attack: An IoT device and a gateway can not talk to each other if an attacker with a jammer uses the same frequency as the IoT device. For this purpose, we model how a jammer operates in the formalization method.

The jammer is always looking for radioactivity on the wireless channel and sending out a signal to stop it, this modeled Jam–Req1. The inv1, inv2 define jamming attack (DOSjammer_attack) and send a jamming signal (send_DOSjammer_signal), respectively. And the event (DOSJammingAttack) check this signal in grd2. After that, The specification of a power threshold (power_ threshold) set (inv5), received power (POWER_RECEIVED) set (inv3), and the channel communication power (communication_power) set (inv4) is required to distinguish channel noise from continuous transmission activity (grd3 and grd4) which models the requirement Jam–Req2. So, if the estimated received power exceeds the predetermined threshold (grd5), the jamming signal is transmitted (act1). Jamming does not occur if the estimated received power is less than the threshold; this satisfies (Jam–Req3) (see Fig. 23).

Fig. 23
figure 23

The DOSJammingAttack event for physical layer Attacks

Full size image

-MAC spoofing attack: MAC address spoofing occurs when an attacker changes a network device’s MAC address to something else. In our model, we are formally modeling this attack’s method and workflow.

To model MAC-Req1, we used the invariants (inv14 and inv15) to define the sender’s and receiver’s MAC addresses. And, the (inv16) defines the MAC address for attack (attackMACAddress) which has to be different from the preferences of both the sender and the receiver MAC-Req2. However, an attacker can acquire access to a data set (inv17). The event (MACSpoofingAttackChecking) covers MAC Req3 by redirecting a device’s destination (distination_address) to a different device (current_address) set (grd2, grd3). Spoofing will occur if the attacker’s address matches the destination address (grd4). If not, nothing would happen. Set the act1 and MAC-Req4 requirements (see Fig. 24).

Fig. 24
figure 24

The MACSpoofingAttackChecking event for physical layer attacks

Full size image

6 Verification and validation

In this section, the steps taken to verify and validate our model are described. The Rodin platform is used to model and validate Event-B for model validation. Although some difficult proof obligations (POs) [47] necessitate manual interactive verification, most of the proof obligations can be proved automatically using the Rodin platform, which automatically creates the proof obligations for each theorem and invariant. The accuracy generation invariants must meet their proof obligations at each level of the model. Validation is accomplished through close observation of the specification’s operation. A plugin called ProB is available on the Rodin platform for animating and validating Event-B requirements.

6.1 Proof-based verification

The Proof Obligation Generator is a feature of the Rodin Platform that generates proof obligations (POs) mechanically. In general, proof tasks were either well-definedness (WD) or invariant preservation (INV) types (for the model’s invariants). The invariant preservation operators (INV POs) guarantee that all events comply with the specification.

The purpose of the well-definedness proof obligation rule (WD) is to guarantee that a potentially ill-defined theorem, axiom, invariant, guard, action, witness, or variant is, in fact, well defined. The following element names are used when referring to a particular modeling component: inv/WD, thm/WD, axm/WD, grd/WD, act/WD, VWD, and evt/x/WWD. The way this proof obligation rule is put into action depends on the expression, which may or may not be clear. A PO may be discharged either automatically or interactively (indicated by the green symbol), or it may remain undischarged (orange symbol). When you see the letter “A” on the PO, it indicates that the discharge is processed automatically.

For example, in our model, the invariant (INV1) in the abstract model (physical layer)inv1: thingname ∈ thing ↔ namesetwhen verifying this invariant by proof obligation, if assigned a name to things, then it is discharged and indicated by (green symbol), if not, it remains undischarged (orange symbol).

In our model, (see Fig. 25); 100% of proof obligations were automatically satisfied by the Rodin prover. The complexity of the proof obligation is correlated with the speed at which automatic proofs can be completed. The robust Rodin plugins greatly facilitate our work by automating the majority of the routine mechanical tasks. But careful modeling and smarter automatic proof tools can cut down on the amount of time people have to spend on verification tasks. Figure 26 shows the proof statistics that illustrates the distribution of automatically and manually discharged POs.

Fig. 25
figure 25

The proof obligations of IoT physical layer formal model

Full size image
Fig. 26
figure 26

The proof statistics of IoT physical layer formal model

Full size image

It’s important to note that the Event-B approach does not have the state explosion problem [48], which is a problem with other verification techniques used in the literature.

6.2 Validation by ProB model checker

There are numerous potent plugins for Rodin. We use the ProB animation tool [47] in our work. For the Event-B approach, ProB is a constraint solver and model verifier that enables both the validation of the requirements and the detection of errors to fix them. It is not necessary for the user to intervene to demonstrate most of the proof obligations. Using ProB’s constraint-solving capabilities, you may create models, check for deadlocks-free, and generate test cases. It needs a concrete model to be done, and cannot be done on an abstract Event-B specification. We were able to perform an automated animation to verify the accuracy of the model specification step-by-step using an animator checker tool. We were able to bring the case studies to life in our model by altering the values of its many variables, carriers, and constants. The initialization parameters of an electrocardiogram (ECG) IoT system shown in Fig. 27 must be used to put this animation into action. To support the generalizability of the proposed method using another case study fire alarm system, see Fig. 28, which shows the initialization parameters of this case study. By monitoring the various states, we may determine whether the model behaves accurately. ProB tested the model’s events and found no problems at any level. This shows that the model’s behavior has been fixed.

Fig. 27
figure 27

Initialization values of the electrocardiogram (ECG) system

Full size image
Fig. 28
figure 28

Initialization values of the fire alarm system

Full size image

7 Conclusion

In this research, we present a method for verifying and validating the security and attacks of the IoT’s physical layer. We formalized and validated the physical-layer vulnerabilities and attacks. First, we defined the needs for modeling the IoT physical layer structure, vulnerabilities (by analyzing the absence of changes in a number of characteristics that contribute to these vulnerabilities, such as speed, usual bandwidth, and power consumption), and attacks (jamming and MAC spoofing). Second, an Event-B model was shown to model and test the security and attacks on the physical layer of the IoT using the mechanism for refinements. The refinements made it possible for us to make corrections by constructing all the models and facilitating the proofs. To show how well our method works, we turned our ideas into a real-world example in the form of an electrocardiogram (ECG) IoT system. As a second case study to show how flexible the proposed method is, we looked at the fire alert system. An animator checker called ProB and proof obligations are used to ensure that our formal model is correct. In future work, we intend to address issues that must be resolved for the IoT physical layer’s continued security. We would like to address the security of physical layer communication protocols as a software component, as our model only addressed the physical component. Additionally, we intend to address security at the IoT system’s other layers.