报告题目：CellScope: Automatically Specifying and Verifying Cellular Network Protocols
报告时间：2019年12月16日上午9：00
报告地点：校本部计算机楼313报告厅
报告人：于银菠博士
报告摘要：Cellular networks bring us great convenience by allowing us to access networks any time anywhere. The convenience, however, suffers from design and logic flaws in network protocols, which exposes various security problems both to users and service providers. Many research efforts have been proposed to identify flaws in cellular network protocols, but most of them involve a lot of manual work. In this talk, an automated framework based on formal method for specifying and verifying cellular network protocols (CellScope) is proposed. In particular, CellScope consists of two parts: a parser frontend and a verification backend. The frontend automatically translates LTE source code to formal models and optimizes models by our property-driven slicing mechanism to reduce state space. In the backend, a counterexample guided sparse value flow analysis mechanism is proposed to enhance the accuracy of model checking. CellScope has been evaluated with an open-source LTE network software (over million lines of code) and identified several known and unknown vulnerabilities. These found vulnerabilities have been validated with real LTE simulators and phones.
报告人简介：于银菠，2014年毕业武汉大学电子信息学院，获工程学士学位；2014年至今在武汉大学电子信息学院进行硕博连读；2017年至2019年获得国家留学基金委资助于美国西北大学进行博士联合培养，导师IEEE Fellow陈焰教授。他的主要研究方向为网络安全、形式化验证、意图网络、软件定义网络和网络功能虚拟化。目前，他已发布相关学术论文9篇，单篇影响因子超过20，包括IEEE COMMUN SURV TUT, JNCA, CN等国际著名期刊，以及ACM SIGCOMM，IEEE IM等国际著名会议。同时，他还担任CCS, ICDCS, ESORIC, IEEE/ACM ToN, IEEE COMMUN SURV TUT, IEEE System Journals等国际顶级期刊和会议的审稿人。
