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

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

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.