编者按
2022年5月，由网络安全研究国际学术论坛（InForSec）汇编的《网络安全国际学术研究进展》一书正式出版。全书立足网络空间安全理论与实践前沿，主要介绍网络和系统安全领域华人学者在国际学术领域优秀的研究成果，内容覆盖创新研究方法及伦理问题、软件与系统安全、基于模糊测试的漏洞挖掘、网络安全和物联网安全等方向。全书汇总并邀请了近40篇近两年在网络安全国际顶级学术议上发表的论文（一作为华人），联系近百位作者对研究的内容及成果进行综述性的介绍。从即日起，我们将陆续分享《网络安全国际学术研究进展》的精彩内容。
本文成果“Shattered Chain of Trust: Understanding Security Risks in Cross-Cloud IoT Access Delegation”发表在USENIX Security 2020上。
作为主要的IoT服务平台，IoT云使得IoT用户能够远程控制设备（这种远程控制甚至可以跨越不同的IoT云平台）。支撑这种跨云平台的设备访问及其权限控制的是各个IoT云平台的授权机制。目前，由于缺少跨IoT云平台授权的行业标准，现有的授权机制往往由各厂商自己开发设计。而由于统一接口、协商等机制的缺失，现有的IoT授权机制存在严重安全隐患。为此，我们开发了半自动检测与验证工具VerioT，首次对现有的主流IoT授权机制进行了系统的分析，结果表明这些机制中普遍存在严重的安全漏洞。通过PoC攻击验证和系统性的评估研究，进一步提出了设计安全的跨云IoT授权机制所要遵循的原则。
该成果“Shattered Chain of Trust: Understanding Security Risks in Cross-Cloud IoT Access Delegation”发表在USENIX Security 2020上。
01 背景与动机
IoT应用的普及促进了对IoT设备进行高效管控的需求。为此，各个IoT厂商纷纷推出跨云平台的设备访问和控制方案。例如，用户可以把自己在Philips云平台中的设备授权给Google Home云平台，进而通过Google Home云平台来远程控制其Philips设备。支撑这样的跨平台IoT设备访问的是各个IoT厂商设计的跨平台授权机制。通过使用各个IoT平台的授权服务，用户可以构建极其复杂的授权关系，如图1所示，IoT平台间可以形成多级授权链。然而，与理论模型不同，跨IoT云平台的授权机制需要兼容所支持的各个IoT云平台已有的系统和服务，因此，其设计和实现上各不相同。这种专用且异构的跨IoT云平台授权机制被广泛应用于真实IoT平台中，如Samsung SmartThings和Google Home，了解这些机制对于IoT生态系统的安全保证至关重要，但这些机制却从未被研究过。
我们开发的半自动化工具VerioT，首次对主流IoT云平台的授权机制进行了形式化安全验证，证明了现有跨IoT云平台的授权机制普遍存在安全风险。进一步地，我们通过PoC攻击验证和系统性评估研究，总结了漏洞的根本成因，并提出如何规避所发现的安全风险的设计原则。
图1
02 设计与实现
首先，从表1可以看到，通过对Google Home、Samsung SmartThings、IFTTT、Philips、LIFX等主流IoT平台的分析，我们总结了9种不同的授权操作。每个授权操作都会导致IoT系统状态的变化，如LIFX云平台通过OAuth操作对Samsung SmartThings云平台进行授权，导致两个云平台授权令牌集合的变化，即LIFX云平台颁发一个授权令牌并传给Samsung SmartThings云平台。为了保证安全性，整个授权过程中，必须保证不存在越权访问现象，如用户不能访问未对其授权（或者权限已被取消）的设备。
表1
基于上述分析，我们使用状态机M=（A,S,O,T,s0）来描述IoT系统的授权过程。其中，A表示系统中的实体，如设备、云平台、用户；S表示系统的状态，每个状态记录了各个实体的授权令牌集合；O表示授权操作（如表1所示）的集合；T表示系统状态的转移，即在授权操作的驱使下，系统从一个状态转移到另一个状态；s0则表示没有任何授权操作发生的初始状态。为保障授权过程的安全，我们提出“在任何状态下，任何用户都不能找到对其不具备访问权限的设备的访问路径”的安全属性。其中，访问路径是通过各个实体的授权令牌集合计算得来。为了对跨IoT云平台的授权进行形式化验证，我们在发生特定操作（如取消授权操作）后，对系统的状态进行检查，通过各个实体接收到的授权指令集合和颁发的授权指令集合来计算两个实体之间是否存在访问路径。一旦发现非法访问路径，就证明存在安全漏洞。进一步地，通过查看对应的系统状态转移情况，获得授权操作顺序，并在真实系统和设备中复现授权操作，最终验证安全漏洞的真实性，并评估其后果。
为了能够实现对不同的IoT平台进行高效分析，我们设计并实现了图2所示的半自动化工具VerioT。
图2
首先，我们通过人工总结，构建了授权操作数据集，该数据集包含了表1中所有的授权操作类型和其不同的实现。我们利用IoT授权基本模型、模型生成器和配置文件来自动生成可用于形式化验证的模型，具体而言，就是通过读取配置文件的配置信息（如IoT云平台类型、设备类型、涉及的授权操作等）和基本模型，模型生成器自动生成Promela模型来描述授权过程。然后，Promela模型由形式化验证工具Spin执行，基于我们所提出的安全属性，Spin会报告出所找到的全部漏洞。最后，通过阅读漏洞报告，对漏洞进行人工确认，完成对IoT授权过程的分析。
（本文选取了文章部分章节，更多精彩内容请阅读《网络安全国际学术研究进展》一书。）
作者简介
袁斌，华中科技大学网络空间安全学院副教授。他的研究方向主要包括软件定义网络、网络安全、物联网安全、云计算安全等。他在USENIX Security、CCS、ACSAC、 IEEE TDSC、IEEE TPDS、IEEE TSC、IEEE TNSM、IEEE TNSE、ACM TOIT、FGCS等国际顶级会议和期刊上发表多篇论文。他主持了国家自然科学青年基金、博士后科学基金等项目；参与了国家重点研发计划项目、973项目等重大科研项目。
版权声明：本书由网络安全研究国际学术论坛（InForSec）汇编，人民邮电出版社出版，版权属于双方共有，并受法律保护。转载、摘编或利用其它方式使用本研究报告文字或者观点的，应注明来源。
