Guan-Hua (Scott) Tu

Assistant Professor

Department of Computer Science and Engineering,
Michigan State University
428 S SHAW LN, ROOM 3115
East Lansing, MI 48824-1266
Email: ghtu AT
Office: 1124 Engineering Building

Formal Analysis

  • CNetVerifer: An Automated, Extensible Control-Plane Protocols Verication Technique[SIGCOMM'14, IEEE/ACM ToN'15]
  • We develop CNetVerifier, an automated control-plane protocol interaction verification method with domain-specific heuristics and model checking techniques to systematically explore possible problematic interactions in cellular networks. The main advantage of this methodology is the exploration of problems/issues in mobile networks is not restricted by unlimited use scenarios (time consuming) or the lack of full access to mobile device or network infrastructure. Its impact on the wireless/mobile networking technology and cybersecurity can be considered as far-reaching. It does not only capture the fundamental design issues of mobile networks span over multiple dimensions, but also discover the security loopholes> caused by improper designs of control-plane protocols of mobile networks. The lessons we learnt can be even applied to the next big things (e.g., 5G, Internet of Thing, Device-to-Device communication) in the networking area.

    • CNetVerifier Overview
    • Cellular network control-plane protocol interaction
    • Finding summary