FMitF: Track II: Usability, Scalability, and Deployment Improvement of VerioT

FMITF：轨道 II：VerioT 的可用性、可扩展性和部署改进

• 批准号: 2124225
• 负责人: Luyi Xing
• 金额: $ 10万
• 依托单位: Indiana University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2124225&HistoricalAwards=false
• 关键词: FMitF; Track; II; Usability; Scalability

The Internet-of-Things (IoT) access-delegation paradigm is emerging and supported by mainstream IoT vendors. In this paradigm, companies provide support to delegate device access to a delegatee cloud/vendor (such as Google Home, SmartThings, and Apple Home), thus permitting a user to manage multiple devices from different vendors through a single app of the delegatee. Flawed design and implementation of IoT delegation protocols incur serious security and safety consequences, such as unauthorized control of smart door locks and health devices. This project improves and extends VerioT (built on the Spin model-checker), the first formal-verification tool for real-world IoT delegation protocols. The project’s novelties are in new methods to facilitate (1) IoT security analysis leveraging usability-enhanced verification reporting, (2) automatic, scalability-enhanced model construction, and (3) integrating verification techniques to modern IoT software development lifecycle. The project’s impacts will be to enable IoT stakeholders and developers to find security flaws earlier --- ideally as soon as the flaws are introduced --- and to increase assurance in the security of IoT systems.The project includes three main tasks. First, to increase the usability of VerioT, the investigators are improving bug reporting by automatically annotating the reported counter-examples with IoT contexts and operations in natural language texts, producing industry-standard security-bug reports. Second, to increase scalability, the investigators are automating model construction by adopting novel Natural Language Processing (NLP) based document analysis techniques, called Dilution, which can precisely construct protocol state machines from unstructured documentation. Third, the investigators are developing support for enterprise-level deployment by integrating VerioT into modern Continuous Integration/Continuous Deployment (CI/CD) pipelines in the software-engineering and IoT industries. The project is intended to yield an industry-strength IoT protocol verifier that keeps up with the development of verification technology and IoT software practices, and helps developers proactively identify new bugs in IoT protocols and software before they are deployed in production.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

物联网（IoT）访问委托模式正在兴起，并得到主流IoT供应商的支持。在此范例中，公司提供支持以将设备访问委托给被委托者云/供应商（诸如Google Home、SmartThings和Apple Home），从而允许用户通过被委托者的单个应用管理来自不同供应商的多个设备。物联网委托协议的设计和实施存在缺陷，会导致严重的安全和安全后果，例如未经授权控制智能门锁和健康设备。该项目改进和扩展了VerioT（构建在Spin模型检查器上），这是第一个用于真实世界物联网委托协议的正式验证工具。该项目的创新之处在于新方法，以促进（1）物联网安全分析，利用可用性增强的验证报告，（2）自动化，可扩展性增强的模型构建，以及（3）将验证技术集成到现代物联网软件开发生命周期中。 该项目的影响将是使物联网利益相关者和开发人员能够更早地发现安全漏洞--理想情况下，一旦引入漏洞--并提高物联网系统安全性的保证。该项目包括三个主要任务。首先，为了提高VerioT的可用性，研究人员正在改进错误报告，通过自然语言文本中的物联网上下文和操作自动注释报告的反例，生成行业标准的安全错误报告。其次，为了提高可扩展性，研究人员正在通过采用新的基于自然语言处理（NLP）的文档分析技术（称为Dilution）来自动化模型构建，该技术可以从非结构化文档中精确构建协议状态机。第三，研究人员正在通过将VerioT集成到软件工程和物联网行业的现代持续集成/持续部署（CI/CD）管道中，为企业级部署提供支持。该项目旨在产生一个行业实力的物联网协议验证器，跟上验证技术和物联网软件实践的发展，并帮助开发人员在物联网协议和软件部署到生产中之前主动识别新的错误。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

MQTTactic: Security Analysis and Verification for Logic Flaws in MQTT Implementations

MQTTactic：MQTT 实现中逻辑缺陷的安全分析和验证

• 发表时间: 2024
• 期刊: Proceedings of the IEEE Symposium on Security and Privacy
• 作者: B. Yuan, Z. Song

Who's In Control? On Security Risks of Disjointed IoT Device Management Channels

• DOI: 10.1145/3460120.3484592
• 发表时间: 2021-11
• 期刊: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
• 作者: Yan Jia;Bin Yuan;Luyi Xing;Dongfang Zhao;Yifan Zhang;Xiaofeng Wang;Yijing Liu;Kaimin Zheng;Peyton Crnjak;Yuqing Zhang;Deqing Zou;Hai Jin

P-Verifier: Understanding and Mitigating Security Risks in Cloud-based IoT Access Policies

• DOI: 10.1145/3548606.3560680
• 发表时间: 2022-11
• 期刊: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security
• 作者: Ze Jin;Luyi Xing;Yiwei Fang;Yan Jia;Bin Yuan;Qixu Liu