Formal Verification of the LoRaWAN Protocol for the Internet of Things

14^th May 2019, 11:00
Matt Webster

Abstract

The Internet of Things (IoT) is an extension of internet connectivity into electronic devices and everyday objects, closely related to pervasive and ubiquitous computing. Many of these devices are battery-operated and have very limited energy available, making low-power wide area network (LPWAN) protocols a key enabling technology for IoT. One such LPWAN protocol is LoRaWAN, which allows for communication between end-devices and a network server via a number of network gateways in a star-of-stars topology. The protocol is optimised for battery-powered end-devices that may be mobile or stationary, and is commonly used for applications within the Internet of Things and cyber-physical systems. In this talk we examine the Adaptive Data Rate (ADR) portion of LoRaWAN. ADR allows servers to adapt and optimise the data rate used by an end-device, reducing time-on-air and power consumption. Formal verification is used here to examine the ADR sub-protocol for internal consistency. Requirements from the LoRaWAN specification are mapped to logic properties for formal verification using a requirements traceability matrix (RTM), which also provides forwards and backwards traceability between requirements and the formal model. The logical properties are then verified using a probabilistic model checker. Examination of the protocol reveals a possible vulnerability in the LoRaWAN specification that could be exploited by an attacker. Recommendations for system designers and directions for future work are given.