An official website of the United States government
5G is a high-bandwidth low-latency communication technology that requires deploying new cellular base stations. The environmental cost of deploying a 5G cellular network remains unknown. In this work we answer several questions about the environmental impact of 5G deployment, including: Can we reuse minerals from discarded 4G base stations to build 5G or does 5G require new minerals that were not required in 4G base stations? And, how sustainable is this transition? We answered these questions buy surveying the minerals needed to build 5G base stations. We found that the key technologies behind 5G require additional rare-earth metals to build essential semiconductor components needed for 5G, such as yttrium, barium, gallium, and germanium. Additionally, since 5G needs many more base stations than 4G network to achieve the same coverage, we describe how 5G will likely increase the use of materials like copper, gold, and aluminum, all of which are difficult or impractical to recycle from the 4G base stations they will replace. We estimate that to provide coverage comparable to 4G in the United States, we will need about 600 million 5G base stations, which will consume thousands of tons of these metals and significant amount of fossil fuels, as well as will result in releasing toxic gases during material mining and refining. Despite these environment costs, we also describe the environmental benefits that a 5G network can offer.
more »
« less
Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications
In this paper, we present Hermes, an end-to-end framework to automatically generate formal representations from natural language cellular specifications. We first develop a neural constituency parser, NEUTREX, to process transition-relevant texts and extract transition components (i.e., states, conditions, and actions). We also design a domain-specific language to translate these transition components to logical formulas by leveraging dependency parse trees. Finally, we compile these logical formulas to generate transitions and create the formal model as finite state machines. To demonstrate the effectiveness of Hermes, we evaluate it on 4G NAS, 5G NAS, and 5G RRC specifications and obtain an overall accuracy of 81-87%, which is a substantial improvement over the state-of-the-art. Our security analysis of the extracted models uncovers 3 new vulnerabilities and identifies 19 previous attacks in 4G and 5G specifications, and 7 deviations in commercial 4G basebands.
more »
« less
- Award ID(s):
- 2326898
- PAR ID:
- 10535452
- Publisher / Repository:
- USENIX Association
- Date Published:
- ISBN:
- 978-1-939133-44-1
- Format(s):
- Medium: X
- Location:
- Philadelphia, PA, USA
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Highly-configurable software underpins much of our computing infrastructure. It enables extensive reuse, but opens the door to broken configuration specifications. The configuration specification language, Kconfig, is designed to prevent invalid configurations of the Linux kernel from being built. However, the astronomical size of the configuration space for Linux makes finding specification bugs difficult by hand or with random testing. In this paper, we introduce a software model checking framework for building Kconfig static analysis tools. We develop a formal semantics of the Kconfig language and implement the semantics in a symbolic evaluator called kclause that models Kconfig behavior as logical formulas. We then design and implement a bug finder, called kismet, that takes kclause models and leverages automated theorem proving to find unmet dependency bugs. kismet is evaluated for its precision, performance, and impact on kernel development for a recent version of Linux, which has over 140,000 lines of Kconfig across 28 architecture-specific specifications. Our evaluation finds 781 bugs (151 when considering sharing among Kconfig specifications) with 100% precision, spending between 37 and 90 minutes for each Kconfig specification, although it misses some bugs due to underapproximation. Compared to random testing, kismet finds substantially more true positive bugs in a fraction of the time.more » « less
-
This paper presents a conversational pipeline for crafting domain knowledge for complex neuro-symbolic models through natural language prompts. It leverages large language models to generate declarative programs in the DomiKnowS framework. The programs in this framework express concepts and their relationships as a graph in addition to logical constraints between them. The graph, later, can be connected to trainable neural models according to those specifications. Our proposed pipeline utilizes techniques like dynamic in-context demonstration retrieval, model refinement based on feedback from a symbolic parser, visualization, and user interaction to generate the tasks’ structure and formal knowledge representation. This approach empowers domain experts, even those not well-versed in ML/AI, to formally declare their knowledge to be incorporated in customized neural models in the DomiKnowS framework.more » « less
-
The value of verification of cyberphysical systems depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature and different timelines of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. We describe a logical-time-based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear.more » « less
-
End-to-End O-RAN Security Architecture, Threat Surface, Coverage, and the Case of the Open FronthaulO-RAN establishes an advanced radio access network (RAN) architecture that supports inter-operable, multi-vendor, and artificial intelligence (AI) controlled wireless access networks. The unique components, interfaces, and technologies of O-RAN differentiate it from the 3GPP RAN. Because O-RAN supports 3GPP protocols, currently 4G and 5G, while offering additional network interfaces and controllers, it has a larger attack surface. The O-RAN security requirements, vulnerabilities, threats, and countermeasures must be carefully assessed for it to become a platform for 5G Advanced and future 6G wireless. This article presents the ongoing standardization activities of the O-RAN Alliance for modeling the potential threats to the network and to the open fronthaul interface, in particular. We identify end-to-end security threats and discuss those on the open fronthaul in more detail. We then provide recommendations for countermeasures to tackle the identified security risks and encourage industry to establish standards and best practices for safe and secure implementations of the open fronthaul interface.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
