Article

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

Authors:

Francesco Rubino,

Gian-Luigi FerrariAuthors Info & Claims

Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola: 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part I

Pages 392 - 408

https://doi.org/10.1007/978-3-031-73709-1_24

Published: 27 October 2024 Publication History

Abstract

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.

References

[1]

Celik ZB, Fernandes E, Pauley E, Tan G, and McDaniel P Program analysis of commodity IoT applications for security and privacy: challenges and opportunities ACM Comput. Surv. (CSUR) 2019 52 4 1-30

Digital Library

[2]

Arslan S, Ozkaya M, and Kardas G Modeling languages for internet of things (IoT) applications: a comparative analysis study Mathematics 2023 11 1263

[3]

Fortino G, Savaglio C, Spezzano G, and Zhou M Internet of Things as system of systems: a review of methodologies, frameworks, platforms, and tools IEEE Trans. Syst. Man Cybernet. Syst. 2021 51 223-236

[4]

Ihirwe, F., Di Ruscio, D., Mazzini, S., Pierini, P., Pierantonio, A.: Low-code engineering for internet of things: a state of research. In: MODELS 2020. Association for Computing Machinery, New York (2020)

[5]

Ihirwe, F., Indamutsa, A., Ruscio, D.D., Mazzini, S., Pierantonio, A.: Cloud-based modeling in IoT domain: a survey, open challenges and opportunities. In: Proceedings of 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), pp. 73–82 (2021)

[6]

D’Angelo, G., Ferretti, S., Ghini, V.: Simulation of the internet of things. In: Proceedings of 2016 International Conference on High Performance Computing and Simulation (HPCS), pp. 1–8 (2016)

[7]

Barriga, J., Clemente, P., Sosa-Sánchez, E., Prieto, Á.: SimulateIoT: domain specific language to design, code generation and execute IoT simulation environments, pp. 92531 – 92552 (2021)

[8]

Korani ZM, Moin A, da Silva AR, and Ferreira JC Model-driven engineering techniques and tools for machine learning-enabled IoT applications: a scoping review Sensor 2023 23 1458

[9]

Zeng X, Garg SK, Strazdins P, Jayaraman PP, Georgakopoulos D, and Ranjan R IOTSim: a simulator for analysing IoT applications J. Syst. Architect. 2017 72 93-107

Digital Library

[10]

Hashem IAT, Anuar NB, Gani A, Yaqoob I, Xia F, and Khan SU Mapreduce: review and open challenges Scientometrics 2016 109 389-422

Digital Library

[11]

Lin Y-W, Lin Y-B, and Yen T-H SimTalk: simulation of IoT applications Sensors 2020 20 9 2563

[12]

Almutairi R, Bergami G, and Morgan G Advancements and challenges in IoT simulators: a comprehensive review Sensors 2024 24 1511

[13]

Bodei C, Degano P, Ferrari G-L, and Galletta L Lluch Lafuente A and Proença J Where do your IoT ingredients come from? Coordination Models and Languages 2016 Cham Springer 35-50

[14]

Bodei C, Ferrari G-L, Degano P, and Galletta L Tracing where IoT data are collected and aggregated Log. Meth. Comput. Sci. 2017 13 3:5 1-38

[15]

Bodei C, Ferrari G-L, Degano P, and Galletta L Arceri V, Cortesi A, Ferrara P, and Olliaro M Risk estimation in IoT systems Challenges of Software Verification 2021 Singapore Springer 221-242

[16]

Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: Proceedings of 2010 IEEE Symposium on Security and Privacy, pp. 317–331 (2010)

[17]

Rubino, F.: Surfing: early security validation of data flow for IoT practice, Master’s thesis, Università di Pisa (2024)

[18]

Gelernter D Generative communication in Linda ACM Trans. Program. Lang. Syst. 1985 7 1 80-112

Digital Library

[19]

Alulema D, Criado J, Iribarne L, Fernández-García AJ, and Ayala R SI4IoT: a methodology based on models and services for the integration of IoT systems Futur. Gener. Comput. Syst. 2023 143 132-151

Digital Library

[20]

Fortas A, Kerkouche E, and Chaoui A Formal verification of IoT applications using rewriting logic: an MDE-based approach Sci. Comput. Program. 2022 222

Digital Library

[21]

VV.AA: The maude system (2024). https://maude.cs.illinois.edu/wiki/The_Maude_System/. Accessed July 2024

[22]

Saidi A, Kacem MH, Tounsi I, and Kacem AH A formal approach to specify and verify internet of things architecture Internet Things 2023 24

[23]

VV.AA: The Rodin Platform (2024). https://www.event-b.org/. Accessed July 2024

[24]

Moradi F, AbbaspourAsadollah S, Pourvatan B, Moezkarimi Z, and Sirjani M Crystal framework: cybersecurity assurance for cyber-physical systems J. Log. Algebraic Methods Program. 2024 139

[25]

Ferrara P, Mandal AK, Cortesi A, and Spoto F Static analysis for discovering IoT vulnerabilities Int. J. Softw. Tools Technol. Transfer 2021 23 71-88

Digital Library

[26]

Yavuz, T., Brant, C.: Security analysis of IoT frameworks using static taint analysis. In: Proceedings of the Twelfth ACM Conference on Data and Application Security and Privacy, pp. 203–213 (2022)

[27]

Schmidt, D., Tagliaro, C., Borgolte, K., Lindorfer, M.: IoTFlow: inferring IoT device behavior at scale through static mobile companion app analysis. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, CCS 2023, Copenhagen, Denmark, 26–30 November 2023, pp. 681–695. ACM (2023)

[28]

Lanotte R and Merro M Drewes F, Martín-Vide C, and Truthe B A calculus of cyber-physical systems Language and Automata Theory and Applications 2017 Cham Springer 115-127

[29]

Lanotte R, Merro M, and Tini S A probabilistic calculus of cyber-physical systems Inf. Comput. 2021 279

Cited By

Tribastone MJähnichen SWirsing M(2024)Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola’s 70th BirthdayLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_1(1-12)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_1

Index Terms

Riding the Data Storms: Specifying and Analysing IoT Security Requirements with SURFING
1. Software and its engineering
  1. Software notations and tools
    1. System description languages
  2. Software organization and properties
2. Theory of computation
  1. Semantics and reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

IoT Security: Practical guide book
IoT device security audit tools: a comprehensive analysis and a layered architecture approach for addressing expanded security requirements
Abstract
The Internet of Things (IoT) has the potential to bring unprecedented accessibility and efficiency to a wide range of critical applications and access control services. With the advent of IoT technology, there is a surge in potential threats and ...
Data Security and risks for IoT in intercommunicating objects
BDCA'17: Proceedings of the 2nd international Conference on Big Data, Cloud and Applications

Nowadays Internet of Things" (IoT) codes are passive entities that encode information, The goal of this work is to give explicit interconnections between IoT specifications and interpreting IoT codes and information's in order to exchange information to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola: 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part I

Oct 2024

441 pages

ISBN:978-3-031-73708-4

DOI:10.1007/978-3-031-73709-1

Editors:
Tiziana Margaria
https://ror.org/00a0n9e72University of Limerick, CSIS and Lero, Limerick, Ireland
,
Bernhard Steffen
https://ror.org/01k97gp34TU Dortmund University, Dortmund, Germany

© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 October 2024

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tribastone MJähnichen SWirsing M(2024)Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola’s 70th BirthdayLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_1(1-12)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_1

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents