计算机网络已经是全球最重要的基础设施之一。然而，随着网络规模的不断增长，协议配置日趋复杂，单纯依靠管理员对网络进行配置极易出现错误，从而引发严重网络故障。近年来，世界范围内已发生多起大规模网络故障，造成大量用户无法上网、飞机无法起飞、银行账户冻结等严重后果。已有的网络正确性验证技术仅能针对规模较小、配置简单的网络进行验证，在网络规模较大、配置较复杂时无法在有效时间内得到验证结果。

针对上述问题，西安交大研究人员通过建立模块化网络行为模型，利用形式化方法有效压缩网络状态，提出了一种快速网络配置自动化验证方法，验证时间在1毫秒以内，真正做到计算机网络的实时验证，有望应用在大规模数据中心网络中。

近日，相关研究成果被计算机网络领域顶级学术会议NSDI 2020 （The 17th USENIX Symposium on Networked Systems Design and Implementation）录用，题目为《APKeep：面向真实网络的实时验证技术》（APKeep: Realtime Verification for Real Networks）。西安交通大学为第一作者单位，计算机学院张鹏副教授为论文第一作者。

NSDI由美国USENIX（高等计算系统协会）主办，是计算机网络领域顶级学术会议，由于每年有大量来自麻省理工学院、斯坦福大学、普林斯顿大学等世界顶尖高校和微软、谷歌等大型互联网公司的投稿，录用论文的含金量极高。这是自2004年NSDI创办以来内地高校以独立第一单位在该会议上发表的并列第6篇论文，也是西安交通大学首次在该会议上发表论文。

西安交通大学计算机学院张鹏课题组依托于智能网络与网络安全教育部重点实验室，研究方向包括计算机网络体系结构、网络安全、网络大数据等，近5年在ACM CoNEXT、IEEE TON、IEEE INCP、IEEE INFOCOM等计算机网络领域顶级会议和期刊上发表了多篇论文。

论文链接：

https://www.usenix.org/conference/nsdi20/presentation/zhang-peng

研究团队链接：

http://gr.xjtu.edu.cn/web/p-zhang