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.

主流物联网供应商正在出现和支持。在此范式中，公司提供了支持设备访问委托云/供应商（例如Google Home，Smartthings和Apple Home）的支持，从而允许用户通过Veclegatee的单个应用程序管理来自不同供应商的多个设备。物联网代表团协议的设计和实施有缺陷，会产生严重的安全和安全后果，例如未经授权控制智能门锁和健康设备。该项目改进并扩展了Veriot（建立在Spin Model-Checker上），这是现实世界IoT代表团协议的第一个正式验证工具。该项目的新颖性是支持（1）IOT安全分析的新方法，利用可用性增强的验证报告，（2）自动，可伸缩性增强的模型构建，以及（3）将验证技术集成到现代IoT软件开发生命周期。该项目的影响将是使物联网利益相关者和开发人员早些时候找到安全缺陷 - 理想情况下，一旦引入了这些缺陷，并提高了物联网系统安全性的保证。该项目包括三个主要任务。首先，为了提高Veriot的可用性，调查人员通过自动注释自然语言文本中的物联网上下文和操作来改善错误报告，从而产生行业标准的安全性BUG报告。其次，为了提高可扩展性，研究人员通过采用新型的自然语言处理（NLP）的文档分析技术（称为稀释）来自动化模型构建，该技术可以准确地从非结构化文档中构建协议状态机器。第三，调查人员正在通过将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

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

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