CAREER: Principled Approaches to Securing Next-Generation Cellular Networks

蜂窝网络是全球范围内最普遍和最主要的通信手段，可连接全球数十亿台设备。然而，虽然是一个国家的核心基础设施，但缺乏系统和严格的安全分析框架和安全设计原则，以确保这些网络的安全和可靠运行。尽管蜂窝技术经过几代人的发展，但信任假设基本保持不变，而对手的能力却显着增强。因此，对手的能力将继续增长，并违反我们今天所依赖的下一代蜂窝网络的安全保证。因此，该项目的首要目标是通过开发算法和系统来确保下一代蜂窝网络的安全，这些算法和系统验证蜂窝网络协议的设计和实现的安全性和隐私保证，以应对可能打破当前信任假设的下一代对手。该提案的教育内容将提供和组织课程，蜂窝捕捉国旗（CCTF）比赛和K-12研讨会，重点是新兴网络和系统的安全和隐私。将招募大学生、妇女和代表性不足的学生，鼓励他们参与研究和教育活动。该项目旨在通过从设计到实施和真实的部署，从根本上纳入安全分析，提高蜂窝网络的安全性。不幸的是，由于以下三个重要的重大挑战，在实践中很难实现这一愿景：（i）缺乏安全分析的模型和属性;（ii）缺乏自动化和整体的安全分析框架;以及（iii）缺乏创建正确和安全的蜂窝协议实现的技术。该项目旨在通过以下方式在统一的框架中解决这些广泛的挑战：（a）开发一个正式的静态安全分析框架，以可扩展地分析设计的协议模型，即，下一代蜂窝网络的蜂窝标准;（B）设计和实现用于分析和验证蜂窝协议实现的安全性的动态安全分析框架;以及（c）开发蜂窝网络特定的协议建模语言和代码生成机制，以产生蜂窝协议的高保证参考实现。这项工作的结果有可能从根本上提高当前（5G）和下一代（6 G）蜂窝网络的安全性，从而对国家和全球安全产生重大影响。工具、模型、特性和发现将在公共领域共享，以促进和推动蜂窝网络科学和社区的发展，直接使蜂窝利益相关者、开发人员和标准机构受益。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Cellular networks are the most pervasive and primary means of global-scale communication that enable connectivity for billions of devices worldwide. Yet, while being such core infrastructures of a nation, there is a lack of systematic and rigorous security analysis frameworks and secure-by-design principles to ensure secure and reliable operations of these networks. Even though cellular technologies have evolved over generations, trust assumptions have largely remained the same whereas adversary capabilities have significantly grown. The adversary capabilities will thus continue to grow and violate the security guarantees of next-generation cellular networks that we rely on today. Therefore, the overarching goal of this project is to secure the next-generation cellular networks through the development of algorithms and systems that verify the security and privacy guarantees of cellular network protocols' design and implementations with respect to next-generation adversaries that can break the current trust assumptions. The proposal's educational content will offer and organize courses, cellular capture-the-flag (CCTF) competitions, and K-12 workshops focusing on the security and privacy of emerging networks and systems. Undergraduates, women, and underrepresented students will be recruited to encourage their engagement in research and educational activities.This project aims to improve the security of cellular networks from the ground up by incorporating security analysis starting from the design to implementations and real deployments. Unfortunately, it has been difficult to achieve this vision in practice due to the following three important grand challenges: (i) Lack of models and properties for security analysis; (ii) Lack of automated and holistic security analysis framework; and (iii) Lack of techniques to create correct and secure cellular protocol implementations. This project seeks to address these broad challenges in a unified framework through (a) Developing a formal static security analysis framework to scalably analyze the protocol model of the design, i.e., the cellular standard of next-generation cellular networks; (b) Designing and implementing dynamic security analysis framework for analyzing and verifying the security of cellular protocol implementations; and (c) Developing cellular network-specific protocol modeling language and code generation mechanism to produce high-assurance reference implementations of cellular protocols. Results from this work have the potential to fundamentally improve the security of current (5G) and next-generation (6G) cellular networks and thus will make a significant impact on national and global security. Tools, models, properties, and findings will be shared in the public domain to promote and advance the science and community of cellular networks, directly benefiting cellular stakeholders, developers, and standard bodies.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.