Checking Information Flow in Cloud-based IoT Access Control Policies

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.