Many cloud providers for IoT technologies offer access control mechanisms whose proper configuration is critical for security. However, verifying permissions in isolation is insufficient in a setting where devices have different levels of trust or are compartmentalized in various subsystems. This work analyses IoT access control policies to identify and mitigate potential security vulnerabilities from unwanted information flow between devices. To this end, we present a formal model of AWS IoT Core’s components and show how to construct an information flow graph to capture communication interactions from device access control policies, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on several real-world IoT access policies.

Checking information flow in cloud-based IoT access control policies / Ceragioli, L., Galletta, L., Lunati, E.. - 7:(2026), pp. 284-295. (FMCAD 2026 - 26th Conference on Formal Methods in Computer-Aided Design Graz, Austria 14-18/09/2026) [10.34727/2026/isbn.978-3-85448-093-8_34].

Checking information flow in cloud-based IoT access control policies

Ceragioli Lorenzo;Galletta Letterio;Lunati Edoardo
2026

Abstract

Many cloud providers for IoT technologies offer access control mechanisms whose proper configuration is critical for security. However, verifying permissions in isolation is insufficient in a setting where devices have different levels of trust or are compartmentalized in various subsystems. This work analyses IoT access control policies to identify and mitigate potential security vulnerabilities from unwanted information flow between devices. To this end, we present a formal model of AWS IoT Core’s components and show how to construct an information flow graph to capture communication interactions from device access control policies, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on several real-world IoT access policies.
2026
978-3-85448-093-8
Formal methods, Computer-aided system design, Hardware and system verification
File in questo prodotto:
File Dimensione Formato  
Ceragioli-2026-Checking Information Flow in Cloud-based IoT Access Contro...-vor.pdf

Accesso aperto

Descrizione: Checking Information Flow in Cloud-based IoT Access Control Policies
Tipologia: Versione Editoriale (PDF)
Licenza: Creative commons
Dimensione 646.64 kB
Formato Adobe PDF
646.64 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11771/37698
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • OpenAlex 0
social impact