Collaborative Research:FMitF:Track 1: DOPaMINe: Distributed Opportunistic Platform for Monitoring In-Situ Networks

鉴于利用动态频谱分配的新兴无线网络对未来国民经济的重要性，发现可能导致故障的协议缺陷以及确定利用协议规范或其实现中的协议漏洞的攻击的检测和防御机制是至关重要的。这项研究将开发一个分布式机会平台，用于监测已部署的无线网络和正式的验证工具，使用这些数据来证明现场安全和健壮的协议操作。使用软件定义无线电(SDR)平台测量4G LTE网络将为新的验证算法提供运行时跟踪和信道信息。将开发新的工具，用于在各种实际操作场景中快速验证正确的协议操作。研究成果将被整合到下一代协议设计中。因此，这项工作将极大地提高新兴无线协议的健壮性和安全性，从而产生革命性的社会影响。一个关键影响将是及早识别协议和实施缺陷，并将其传达给行业和标准组织。框架的所有方面，包括架构、工具和案例研究，都将公开提供。将开发实践培训模块，以说明无线协议的关键概念及其安全含义，并将其整合到研究生/本科生课程中。这些课程将为研究成果的传播提供一条关键途径。女性和少数族裔学生将参与跨学科的研究项目。正在追求的方法是将正式的验证方法应用于无线网络，其中使用运行轨迹来验证操作的正确性，以符合规范。这些方法是众所周知的，并已在许多硬件-软件平台中广泛应用，并取得了成功。但是，它们通常用于完全了解运行时行为的系统。在分布式蜂窝系统中，不一定存在完整的踪迹和完整的瞬时系统状态(例如，在不同位置的干扰数据或遇到不同信道状态的移动用户)。因此，本研究将寻求将形式化验证方法扩展到存在不完整和变化状态以及不完整踪迹的无线网络领域。这项工作的结果将是收集运行时跟踪和单元状态的工具，以及验证算法，然后可以验证正确的操作或快速检测由不正确的实现或攻击导致的故障。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.