Riding the Data Storms: Specifying and Analysing IoT Security Requirements with SURFING

The Internet of Things (IoT) is a rapidly evolving domain that connects various devices and sensors to the internet, facilitating data exchange and automation. However, ensuring the trustworthiness of sensor data utilized by actuators for decision-making is a crucial concern, especially in safety-critical systems that leverage IoT. Untrustworthy data could result in data breaches, system failures, or even loss of life. Therefore, it is essential to specify and analyze the security prerequisites of IoT systems. In this paper, we present SURFING, a requirement language for IoT based on the IoT-LySa process calculus. SURFING allows IoT systems to be specified in terms of their components, communication channels, data flows, and security properties. We also describe the SURFING toolkit, which supports the simulation, and verification of IoT specifications. Furthermore, we have developed a symbolic execution engine for the SURFING toolkit, which enables tracking, navigating, and analyzing data pathways within an IoT specification. This capability helps identify and prevent potential data leaks, tampering, or spoofing. We show the utility of SURFING and its toolkit through a case study involving a street lighting control system.