检查基于云的物联网访问控制策略中的信息流（扩展版）
Checking Information Flow in Cloud-based IoT Access Control Policies (Extended Version)
浏览论文内容
中文总结 AI 辅助
该研究针对云物联网访问控制策略，通过形式化建模AWS IoT Core组件、定义信息流图并结合SMT求解器实现工具IOT:POKER，以识别设备间非预期信息流带来的安全漏洞。
中文摘要 AI 辅助
许多物联网技术的云提供商提供的访问控制机制，其正确配置对安全至关重要。然而，在设备具有不同信任级别或被划分为不同子系统的环境中，孤立验证权限是不够的。本研究分析物联网访问控制策略，以识别设备间因非预期信息流导致的潜在安全漏洞。为此，我们对AWS IoT Core的组件进行形式化建模，并定义信息流图来捕获访问控制策略允许的设备间通信。我们利用SMT求解器构建该图的有限表示，从而能够验证设备间的信息流。我们在名为IOT:POKER的工具中实现了该方法，并在一个现实场景和几个真实世界策略上对其进行评估。
英文摘要
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 compartmentalised in various subsystems. This work analyses IoT access control policies to identify potential security vulnerabilities from unwanted information flow between devices. To this end, we formally model AWS IoT Core's components and define an information flow graph to capture the communication among devices permitted by the access control policies. We build a finite representation of the graph by leveraging an SMT solver, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on a realistic scenario and several real-world policies.
