Given the importance of emerging wireless networks that utilize dynamic spectrum allocation to the future national economy, it is critical to find protocol shortcomings that can result in failures as well as determine mechanisms for detection and defense against attacks that exploit protocol vulnerabilities either in the protocol specifications or their implementations. This research will develop a distributed opportunistic platform for monitoring deployed wireless networks and formal verification tools that use this data to certify safe and robust protocol operation in the field. Measurements of 4G LTE networks using a software-defined radio (SDR) platform will provide the runtime traces and channel information for new verification algorithms. New tools for rapidly verifying correct protocol operation in a variety of real-world operational scenarios will be developed. The research results will be integrated into next-generation protocol design. Consequently, this work will have a transformative societal impact by dramatically increasing the robustness and security of emergent wireless protocols. A key impact will be early identification of protocol and implementation weaknesses, which will be communicated to industry and standards organizations. All aspects of the framework, including architectures, tools, and case studies, will be made publicly available. Hands-on training modules will be developed to illustrate key concepts of wireless protocols and their security implications, which will be integrated into graduate/undergraduate classes. These courses will provide a key pathway for the dissemination of the research results. Female and minority students will be engaged through interdisciplinary research projects.
The approach being pursued is to apply formal-verification methods to wireless networks, where runtime traces are used to verify the correctness of operation against a specification. These methods are well understood and have been applied extensively in many hardware-software platforms with demonstrated success. However, they typically are used for systems with complete knowledge of runtime behaviors. In cellular systems that are distributed, there are not necessarily complete traces and complete instantaneous system states (e.g., interference data at different locations or mobile users who encounter different channel states). Therefore, this research will seek to extend formal-verification methods to the wireless-network domain, where there are incomplete and changing states and incomplete traces. The outcome of the work will be tools for collecting runtime traces and cell states and verification algorithms that can then verify correct operation or quickly detect failures caused by improper implementation or attacks.
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.
