Imagine what would happen if all wireless communication stopped suddenly. There would be mass panic since many people have never known any other way of communicating. There would also be catastrophic failure of many systems and processes that have been built on top of a wireless communication system, e.g., autonomous vehicles, navigation systems, and increasingly, smart devices in the home, office, and hospitals. In other words, the consequences of a breakdown of the wireless communications plane are severe.

One can argue that this scenario is unlikely because of the standards process by which wireless communication devices and networks are designed. On the other hand, while the standards process produces efficient protocols, rigorous mathematical assurance of their safe and predictable behavior on diverse complex distributed deployment scenarios has been lacking. Consequently, we face the very real possibility of rare) unexpected protocol behaviors which may result in failure or there may exist unknown vulnerabilities that can be exploited by unfriendly third parties. Given the ease of using powerful software-defined radios, the potential for unintentional or intentional malicious behaviors also increases. As we move towards 5G and future networks with dynamic spectrum allocation, the set of potential failure modes multiplies. For instance, unintentional spectrum squatting or intentional attacks that force legitimate users to vacate spectrum or trigger their devices into conservative protocol behaviors that use less bandwidth are possible.

This project focuses on addressing this crucial problem. The project will develop a flexible, powerful distributed platform for monitoring deployed networks, and analysis tools that use this data to certify safe and robust protocol operations in field. The project is funded by National Science Foundation under the “Formal Methods in the Field” program and is titled “DOPaMINe: Distributed Opportunistic Platform for Monitoring In-Situ Networks. The research will be performed in close collaboration between the University of Florida and Portland State University. Dr. Sandip Ray, member of Warren B. Nelms Institute for the Connected World, Endowed IoT Term Professor and Professor of the Department of Electrical and Computer Engineering, will lead the research from UF side. The anticipated approach will involve a tight mix of analytic and experimental components. The analytic work will extend existing formal verification methods to certify assurance of trustworthy execution of deployed protocols. The experimental work will utilize traces from deployed networks to demonstrate viability of the analysis. The anticipated result will be powerful assurance infrastructure to certify robustness of wireless communication systems against failures and malicious exploitation, and detect vulnerabilities and non-compliance of system executions in real-time.