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

合作研究：FMitF：轨道 1：DOPaMINe：用于监控原位网络的分布式机会平台

• 批准号: 2019240
• 负责人: Sandip Ray
• 金额: $ 25万
• 依托单位: University of Florida
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019240&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; DOPaMINe

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.

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