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.| 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.


