Modeling and proving dynamic behaviors of a routing protocol: A tutorial

With the increasing adoption of Internet of Things technologies for controlling physical processes, their dependability becomes important. One of the fundamental functionalities on which such technologies rely for transferring information between devices is packet routing. However, while the performance of Internet of Things–oriented routing protocols has been widely studied experimentally, little work has been done on provable guarantees on their correctness in various scenarios. To stimulate this type of work, in this article, we give a tutorial on how such guarantees can be derived formally. Our focus is the dynamic behavior of distance-vector route maintenance in an evolving network. As a running example of a routing protocol, we employ routing protocol for low-power and lossy networks, and as the underlying formalism, a variant of linear temporal logic. By building a dedicated model of the protocol, we illustrate common problems, such as keeping complexity in control, modeling processing and communication, abstracting algorithms comprising the protocol, and dealing with open issues and external dependencies. Using the model to derive various safety and liveness guarantees for the protocol and conditions under which they hold, we demonstrate in turn a few proof techniques and the iterative nature of protocol verification, which facilitates obtaining results that are realistic and relevant in practice.

A Multi-Agent Reinforcement Learning-Based Optimized Routing for QoS in IoT

The Routing Protocol for Low power and lossy networks (RPL) is used as a routing protocol in IoT applications. In an endeavor to bring out an optimized approach for providing Quality of Service (QoS) routing for heavy volume IoT data transmissions this paper proposes a machine learning-based routing algorithm with a multi-agent environment. The overall routing process is divided into two phases: route discovery phase and route maintenance phase. The route discovery or path finding phase is performed using rank calculation and Q-routing. Q-routing is performed with Q-Learning reinforcement machine learning approach, for selecting the next hop node. The proposed routing protocol first creates a Destination Oriented Directed Acyclic Graph (DODAG) using Q-Learning. The second phase is route maintenance. In this paper, we also propose an approach for route maintenance that considerably reduces control overheads as shown by the simulation and has shown less delay in routing convergence.

LDES: Detector Design for Version Number Attack Detection using Linear Temporal Logic based on Discrete Event System

The Internet Engineering Task Force (IETF) has defined routing protocols for Low Power and Lossy Networks (RPL) for constrained devices. RPL constructs DODAGs (Destination Oriented Directed Acyclic Graphs), to optimize routing. RPL ensures acyclic topology with the DODAG version number. However, the control message's DODAG version number is not authenticated. So, RPL is vulnerable to topological inconsistency attack known as DODAG Version Number (DVN) attack. DVN attack creates a packet delay, packet loss, cyclic topology, etc., in the network. This paper proposes a method for detecting DODAG version number attacks. Several existing schemes to defend against the DVN, such as cryptographic techniques, trust-based, threshold-based and mitigation are computationally intensive or require protocol modification. DVN does not change the packet format or sequence of packets, but can still perform attacks and hence fall under the category of stealthy attacks, which are difficult to detect using traditional Intrusion Detection System$'$s (IDS). Discrete-Event System (DES) based IDS have been applied in the literature for stealthy attacks that achieve low overhead, low false alarm rate, etc. However, the construction of DES-based IDS for network protocol may lead to errors, as modelling is manual. The resulting IDS, therefore, is unable to guarantee its correctness. This paper proposes Linear Temporal Logic (LTL) based DES paradigm to detect DVN. LTL-based paradigm facilitates formal verification of the DES-based IDS, and hence the correctness of the scheme is ascertained. The proposed technique is simulated using the Contiki cooja simulator. When the percentage of spiteful nodes in the network increases, the true positive rate, and packet delivery rate drops, while the false positive rate and control message overhead increase. The memory requirement for sending the packets and verifying the nodes is minimal. The LTL-based IDS has been formally verified using NuSMV to ensure the correctness of the framework.

LC-DEX: Lightweight and Efficient Compressed Authentication Based Elliptic Curve Cryptography in Multi-Hop 6LoWPAN Wireless Sensor Networks in HIP-Based Internet of Things

The high level of security requirements and low capabilities of constrained devices that are connected to the Internet of Things (IoT) constitute a new challenge in terms of proposing an authentication solution that deals with the problem of energy constraints. The Host Identity Protocol Diet EXchange (HIP DEX) is primarily designed to be suitable for constrained devices and designed to be resistant to Denial of Service (DoS) and man-in-the-middle (MITM) attacks. In this paper, we propose an efficient saving energy solution to secure end-to-end (E2E) communications based on the compression of the IPv6 over Low Power Wireless Personal Area Networks (6LoWPAN) header for HIP DEX packets. We implement our solution in an IoT based-WSN over Constrained Application Protocol (CoAP) in the application layer and Routing Protocol for Low power and lossy networks (RPL) in the routing layer. We also propose a novel distribution model that minimizes the number of signaling messages. Both proposed compression and distribution models for HIP DEX combined with an original implementation of an opportunistic association establishment of the handshake, constitute an efficient security solution for IoT. We called our solution Lightweight Compressed HIP DEX in the IoT (LC-DEX).

A Trust-Integrated RPL Protocol to Detect Blackhole Attack in Internet of Things

Internet of things (IoT) offers communication between user-to-machine and machine-to-machine. Due to their inherent characteristics of open medium, very dynamic topology, lack of infrastructure and lack of centralized management authority, IoT present serious vulnerabilities to security attacks. The routing protocol for low-power and lossy networks (RPL) does not have an inherent mechanism to detect routing attacks. Popular among these IoT attacks is blackhole attack. An attacker can exploit the routing system of RPL to launch blackhole attack against an IoT network. To secure IoT networks from blackhole attack, trust-integrated RPL protocol (TRPL) is proposed and implemented. The trust system is embedded in the RPL protocol to detect and isolate a blackhole attack while optimizing network performance. The trust is calculated from successful interaction between two nodes. The calculated trust value is considered in parent selection. TRPL demonstrates its superior performance over the standard RPL protocol and existing techniques in the detection and isolation of blackhole attacks.