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

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.