CellScope

Cellular network protocols keep emerging. The public is more aware of technology evolving in the data plane than the control plane, e.g., from TDMA, CDMA (2G) to OFDM (4G) and from micro ware to mill-meter wave (5G). On the other hand, the control plane in cellular network is also evolving fast. Many control protocols are emerging to add or enhance network functions, e.g., authentication, registration, handover, call/text services, and so on. These control protocols provide flexible network access to users, but also cause security issues to users.

To address this issue, CellScope, a vulnerability prediction tool for cellular network protocols is proposed. As shown in the above figure, CellScope adopts the counterexample guided abstraction refinement method to analyze network protocols and performs model checking on procedure dependence graphs (PDGs) of these protocols (constructed from cellular network software by CodeSurfer). Our method then starts from the abstraction model of protocols and automatically refines the model in detail according to the feasibility of found counterexamples. CellScope is precise and scalable for verifying emerging cellular network protocols and identifying vulnerabilities in cellular network protcols.