An Integrated Toolkit for IoT Protocol Dialecting with Formal Verification
Abstract
Motivation. Internet of Things (IoT) technologies are enabling increasingly pervasive communications of mobile and embedded devices,, including those in Naval ship and shore environments.Current IoT protocols suffer from exploitable vulnerabilities, at both specifi,cation (design) andcode (implementation) levels. We are particularly concerned about attacks that infiltrate, eavesdrop,disrupt, or,hijack communications between IoT devices. A main culprit behind attacks against IoTdevices is the uniformity of IoT protocols, whic,h poses two security threats: (1) the standard protocolspecifications are universally adopted, making it easy for attackers to learn,, understand and forgeprotocol messages; (2) the protocols? generality leads to design and implementation bloat, enlargingthe attack, surface and increasing the number of vulnerabilities in them.Vision. Our vision is a new paradigm called IoT-FD ? Internets of Form,al Dialect-Speaking Things.IoT-FD aims to break IoT protocols? uniformity and bloat, by creating IoT protocol dialects, eachbeing a,customized and debloated variant of a standard IoT protocol stack. Furthermore, eachprotocol dialect will be created based on formal, specifications of the dialect?s behaviors, usagecontexts, and desired properties, which will then be formally verified to ensure th,at the dialect willfunction correctly without design- and implementation-level vulnerabilities. The IoT-FD paradigmwill also help fo,rmally define the dialect?s robustness against adversarial inference and imitation.Proposed Work. In this research, we propose to de,velop an integrated IoT-FD toolkit for creatingIoT protocol dialects from its original protocol code base, aiming at a high level of, practicality,assurance, and robustness. The toolkit will support the end-to-end workflow of protocol dialecting,which involves prot,ocol stack customization, debloating, and formal verification. To demonstrate thepracticality of the IoT-FD toolkit, we will instant,iate the toolkit for real-world IoT protocols, startingfrom Bluetooth and Zigbee on a range of system platforms and devices.Innovati,on Claim and Impacts To the best of our knowledge, this project is among the first tocreate protocol dialects for specialized IoT en,vironments, with formal specification and verificationsupport. Technically, it challenges and changes the ?uniformity and bloat? sta,tus quo of currentIoT protocol development and deployment, and will contribute new models, techniques, and toolsto the research comm,unity. Practically, this project is expected to elevate the level of security andresiliency of specialized IoT and embedded networks, that are widely deployed in Naval and otherdefense environments.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 05, 2022
- Source ID
- N000142212671
Entities
People
- Dongyan Xu
Organizations
- Office of Naval Research
- Purdue University
- United States Navy