Checking Information Flow in Cloud-based IoT Access Control Policies (Extended Version)
This work formally model AWS IoT Core's components and defines an information flow graph to capture the communication among devices permitted by the access control policies, and builds a finite representation of the graph by leveraging an SMT solver, thus enabling the verification of information flow between devices.