今天为大家推荐的论文是来自印第安纳大学邢璐祎研究组和中国科学院信息工程研究所刘奇旭研究组共同投稿的，目前已经发表在CCS 2022上的工作，P-Verifier: Understanding and Mitigating Security Risks in Cloud-based IoT Access Policies。
现代物联网（IoT）设备制造商正在借助于平台即服务（PaaS）和基础设施即服务（IaaS）物联网云平台（如AWS IoT、Azure IoT）来进行安全便利的IoT开发及部署。物联网云平台的访问控制是通过物联网访问控制策略（IoT Policy）来实现的，这些策略由设备制造商开发并由云平台端执行。IoT Policy写明哪些IoT实体(IoT 用户、IoT设备)可以在什么条件下访问哪些IoT资源。然而，针对IoT Policy的安全性，学术界还缺乏系统性研究, 厂商和用户更没有安全保障(formal guarantee)。
作者对基于现代PaaS/IaaS云的物联网访问控制策略（IoT Policy）进行了全面研究。研究表明，IoT语义和策略（policy）执行逻辑的复杂性，为IoT开发者留下了巨大的出错空间。这些出错空间的隐患，能诱导开发者编写带有漏洞的IoT Policy。作者分析了36家厂商的IoT设备或应用，以及310个IoT相关的开源项目(from Github)，从真实厂商的实现中发现了13家不同厂商的17个独立的安全漏洞实例。通过对这些安全漏洞的深入理解，作者总结了两种设计空间的安全缺陷，分别是（1）IoT Policy和MQTT协议之间语义的不匹配，和（2）IoT Policy与IAM Policy之间的安全责任的不协调。两种实现空间的缺陷分别是（3）IoT Policy模板的语义缺失，和（4）IoT Policy的互斥约束未被严格遵守。另外，作者也注意到，IoT Policy的复杂语义使得对其进行严格的自动推理(formal reasoning)来获得安全保障是困难的。本文设计和开发了第一个能够对云端IoT access control policy进行formal modeling (i.e., logical encoding)和reasoning的工具，在真实世界的几百个IoT policy上进行了大规模实验和验证。同时，为了评测IoT policy的分析工具，本文提出了第一个benchmark，称为IoT-Policy Bench。
Design Flaws of IoT Policies（IoT policy设计漏洞）
A. 设计空间的缺陷1 — IoT Policy和MQTT协议之间语义的不匹配
首先介绍设计空间的缺陷1，IoT Policy和MQTT协议之间语义的不匹配。IoT Policy对字符串解析的核心能力可以被等价为确定有限状态自动机（Deterministic Finite Automaton, DFA）。对于MQTT协议，“+”和“#”字符都是通配符，而对于云端解析的IoT Policy，“*”才是通配符。因此，IoT Policy和MQTT协议所对应的DFA字符集是不一致的。
这样一来，一个IoT资源（如一个MQTT topic）虽然可以在IoT Policy的所对应的DFA上被拒绝，但有可能在MQTT协议所对应的DFA上被允许。攻击者可以利用这样的特性绕过IoT Policy的某些限制。如图1所示，一个IoT Policy允许了对a/b/*的访问，而明确拒绝了对“a/b/x/y”资源的访问，但通过利用上述的两种DFA的不匹配的缺陷，一个攻击者可以通过访问“a/b/x/+”或“a/b/#”等字符串，访问到“a/b/x/y”资源。作者将这样的其他能访问到相同资源的字符串称为IoT同义词。
作者提到，缺陷1的一个典型的案例是日本厂商Hippokura。在其设计中，“xmd/session/[session id]”将作为不同实体之间通信的频道，并且厂商的IoT Policy明确拒绝了一个用户去订阅“xmd/session/#”主题，因此，在合法的场景下，用户只能访问其自己的“xmd/session/[session id]”主题，也就是说，一个攻击者在不知道其他人频道ID的情况下，也就无法访问别人的通信频道。然而，作者的研究发现，“xmd/#”可以作为一个IoT同义词被攻击者合法订阅，从而绕过IoT Policy的限制，导致任意一个用户可以订阅所有其他人的频道。
B. 设计空间的缺陷2，即IoT Policy与IAM Policy之间的安全责任的不协调
如图2所示，借助AWS Cognito和AWS IAM，开发者可以为AWS IoT引入动态身份认证和授权能力（一般用于用户登录和授权）。设备制造商在Cognito Identity Pool中记录的用户身份（Cognito Identity ID），当Identity Pool绑定IAM Policy，其中的每一个Cognito Identity ID代表的用户或设备可以向IAM Policy允许的任何AWS服务发送API请求，Cognito的Identity Pool的授权方式分为两种，第一种是需要完整的登录授权流程，并生成长期使用的Identity ID（以下简称为Authed ID），第二种是不经过登录授权流程而生成一个临时的Identity ID（以下简称为Unauthed ID）。作者发现，Cognito相关IAM Policy在与IoT Policy联动时的逻辑是不协调的。如图2a所示，对于经过完整登录授权的用户，除了被IAM Policy允许调用IoT相关API外，如想去真正接入IoT endpoint（以MQTT Broker为核心的IoT接入服务），还需要为Identity ID绑定一个IoT Policy来允许相关核心操作（如发布权限iot:Publish, 订阅权限iot:Subscribe），因此在IAM Policy中写一个范围较大的权限是合理的（代表所有IoT用户的总共的最大权限）。然而，如图2b所示，对于一个持有Unauthed ID的恶意用户，只需要其Identitiy Pool所绑定的IAM Policy被写入一个过大权限，而不需要再绑定IoT Policy即可直接连入IoT endpoint。当厂商未能理解两种不同逻辑的区别时，就可能引入安全风险，如攻击者可控制或监控厂商云上所有的设备。另外，无论是哪种授权逻辑，如果在IAM Policy中引入敏感的IoT API权限，也会带来安全风险，如一个恶意用户可以删除厂商在云平台上注册的设备。
被此类缺陷困扰的一个厂商是Molekule，其Unauthed ID对应的IAM policy给出了一个过大的权限，可能是iot:*，也就是iot相关的所有权限。利用这样的漏洞，一个攻击者可以在不登录的情况下，仅通过Unauthed ID，任意订阅、发布任何MQTT消息，也就是任意监控和控制任何人的设备。
http://www.xing-luyi.com/uploads/2/5/6/4/25640947/ccs_2022_iot_policy_long_version.pdf
基于对上述4种缺陷的理解，作者设计了对IoT Policy进行形式化建模的方法，并基于Z3等off–the-shelf开源求解器，开发了P-Verifier，首个针对IoT Policy进行全语义分析的的形式化验证工具，P-Verifier包含三种基本的检测能力：
-
IoT Policy是否以符合预期的方式排除了某些权限 ，例如防止用户访问目标IoT资源；
-
IoT Policy是否比一个参考策略（允许范围的上限）的权限更大；
-
是否有多个独立的IoT Policy（分配给独立用户）共享权限 。
P-Verifier解决的重大挑战包括如图1所示的IoT Policy与MQTT协议的语义不适配，换句话说，也就是IoT Policy的DFA字符集和MQTT协议字符集不适配这一问题。如忽略这一问题，P-Verifier的语义势必也会和IoT Policy一样忽略掉某些被IoT同义词绕过的可能性。这是在之前的关于云平台访问控制策略的研究中从未遇到的困境。
P-Verifier克服这一重大挑战的核心思想是，对字符集的数量进行缩减，把两个DFA字符集的问题转化成在同一个字符集上的问题，再进行形式化验证。为此，作者设计了对MQTT通配符的新的编码方式，以及解决IoT同义词问题的字符集缩减算法，在必要时对IoT Policy的通配符进行扩展以便得到所有可能存在的IoT同义词。字符集缩减算法的公式描述如图3所示。
另外，作者还通过对真实厂商和开源项目的分析整理，以及对IoT场景的理解，编制了一个包含706个IoT Policy的Benchmark。进一步，作者借助这个Benchmark，将P-Verifier与已知唯一一个能对IoT Policy进行分析的工具AWS IoT Defender进行了对比，对比结果如表1所示。结果显示，P-Verifier的效果明显好于AWS IoT Defender。另外，作者还根据字符串长度和policy语句的数量这两个维度，对P-Verifier的时间复杂度进行定性测量，如图3和图4的所示，P-Verifier的耗时增长方式近似于线性。
http://www.xing-luyi.com/uploads/2/5/6/4/25640947/ccs_2022_iot_policy_long_version.pdf
原文始发于微信公众号（安全研究GoSSIP）：G.O.S.S.I.P 阅读推荐 2022-11-03 P-Verifier
