This paper analyzes the Embedded SIM card's Machine-to-Machine Remote Provisioning Protocol's (eSIM M2M RSP) design. The eSIM M2M RSP simplifies 5G connectivity for IoT devices by securely delivering connection bootstrapping information over the air without human intervention. As IoT adoption with 5G connectivity surges, the eSIM infrastructure must handle a growing number of concurrent remote SIM provisioning requests. The statefulness and shared states of the RSP make it challenging and error-prone to implement concurrency without data races. The GSMA eSIM standard does not explicitly define any atomicity assumptions required for concurrent execution. A formal analysis of the standard-prescribed M2M RSP design reveals that explicit atomicity assumptions are necessary; without them, 31 data races can violate key invariants. During the responsible disclosure process, discussions with the standards body revealed that the M2M RSP design relies on unstated and implicit atomicity assumptions. However, we find that the standard prescribed implicit assumptions are not strong enough to maintain all the invariants. The identified race conditions can be exploited by third-party eSIM management platforms to defraud network operators. To mitigate these risks, we developed a fine-grained synchronization mechanism that we formally verified for correctness and empirically evaluated for performance. Empirical evaluations show that our synchronization mechanism ensures correctness while outperforming a baseline with a 6× speed up.

Cellular networks nowadays are not only responsible for powering up worldwide communication systems, but also enable highly sensitive applications, such as the earthquake and tsunami warning system (ETWS), telemedicine, and autonomous vehicle communication. Due to its importance, one would expect this technology to be highly robust, secure, and reliable. However, even in the newest generations (i.e., 5G), this is not the case. Due to either implementation slipups [6, 11], errors in the standard [3, 5], or misconfigurations [2]. These errors enable numerous destructive attacks, enabling malicious parties to track a victim's location, disrupt cellular services, and eavesdrop on calls, among other implications. To make matters worse, developing defenses against these types of attacks is a non-trivial task as it requires network operator cooperation. Most importantly it requires a significant amount of resources to be allocated by network operators and device manufacturers [2]. To justify allocating resources to fix these issues, network operators need to quantify the misbehaviors and attacks being carried out in the wild. Unfortunately, there is no mechanism in place to perform this type of measurement.

We present an efficient approach to learn past-time linear temporal logic formulas (PLTL) from a set of propositional variables and a sample of finite traces over those variables.The efficiency of our approach can be attributed to a careful encoding of the PLTL formula learning problem as a bit-vector function synthesis problem, and the use of an enhanced Syntax-Guided Synthesis (SyGuS) engine to solve the latter.We implemented our approach in a tool called SYSLITE and empirically evaluated its efficacy with two case studies.In these case studies, we observe that SYSLITE on average enjoys a speedup of 44x over current learning approaches for temporal formulas while learning the expected formulas in the vast majority of cases.

The paper proposes 5GReasoner, a framework for property-guided formal verification of control-plane protocols spanning across multiple layers of the 5G protocol stack. The underlying analysis carried out by 5GReasoner can be viewed as an instance of the model checking problem with respect to an adversarial environment. Due to an effective use of behavior-specific abstraction in our manually extracted 5G protocol, 5GReasoner's analysis generalizes prior analyses of cellular protocols by reasoning about properties not only regarding packet payload but also multi-layer protocol interactions. We instantiated 5GReasoner with two model checkers and a cryptographic protocol verifier, lazily combining them through the use of abstraction-refinement principle. Our analysis of the extracted 5G protocol model covering 6 key control-layer protocols spanning across two layers of the 5G protocol stack with 5GReasoner has identified 11 design weaknesses resulting in attacks having both security and privacy implications. Our analysis also discovered 5 previous design weaknesses that 5G inherits from 4G, and can be exploited to violate its security and privacy guarantees.

In the cellular ecosystem, base stations act as trusted intermediaries between cellular devices and the core network. During connection bootstrapping, devices currently, however, do not possess any mechanisms to authenticate a base station before connecting to it. This lack of authentication has been shown to be exploitable by adversaries to install fake base stations which can lure unsuspecting devices to connect to them and then launch sophisticated attacks. Despite being a well-known threat to the cellular ecosystem, this weakness is not addressed in the current protocol versions including 5G. The current paper sets out to fill this void by proposing a Public-key infrastructure (PKI) based authentication mechanism which builds on top of the asymmetric cryptography used in 5G and adheres to the relevant deployment constraints. Our proposed authentication scheme leverages precomputation-based digital signature generation algorithms and employs optimizations in three dimensions---PKI scheme-level, protocol-level, and cryptographic scheme-level---to address the trilemma of small signature size, efficient signature generation, and short verification time. Our evaluation on a real testbed indicates that the proposed scheme is not only readily deployable but also performs better than a symmetric key-based scheme (i.e., TESLA) in terms of security guarantee, overhead, and deployment constraints (e.g., backward compatibility).