Automated Reasoning of Security and Privacy of Cellular Networks

Feb 05, 2020

Download: MP4 Video Size: 308.5MB  
Watch on YouTube

Abstract

Cellular technologies enable a wide array of critical services, from personal communication, autonomous vehicles and telemedicine to critical infrastructures, such as smart grid electricity distribution. Unfortunately, security and user privacy for such complex networks are often considered as afterthoughts. These lead to inadequate security evaluation early on the development cycle that fails to identify missing security and privacy guarantees in protocol designs. To make matters worse, unsafe practices and operational oversights stemming from poor input sanitization and unvetted simplification of complex protocol interactions further contribute to the deviation of deployments from designs. In this talk, I will highlight how my research addresses these problems by developing principled techniques for analyzing design specifications and deployments of complex cellular network protocols.

 

I will first present a new adversarial reasoning technique combining the capabilities of a symbolic model checker and a cryptographic protocol verifier that enabled us to identify 20+ new vulnerabilities in 4G and 5G cellular network design specifications. I will then discuss three new side-channel attacks in 4G and 5G networks uncovered with our dedicated probabilistic reasoning technique. Next, I will talk about a fuzzing technique which is more effective than the state-of-the-art in reasoning about syntactic and semantic correctness of an implementation when binary instrumentation is not realizable and direct feedback on code coverage information is missing. Finally, I will conclude with a discussion on challenges in adapting and scaling our current approaches for a holistic analysis of 5G and next-generation cellular networks, and IoT systems.