计算机软件新技术国家重点实验室   青年学者学术报告

摘 要：

近年来，世界范围内网络事故频繁发生，造成了严重经济损失。为了从根本上解决这一问题，学术界和工业界对网络验证逐渐关注。不同于传统“被动”+“事后”的网络故障诊断方法，网络验证利用形式化方法对网络进行分析，“主动”的在“事前”发现潜在网络故障。数据平面验证是网络验证的一类方法，可在毫秒时间内增量验证数据平面状态（包括拓扑、IP转发规则等）更新后网络转发行为的正确性。这些方法将网络中数据包进行等价类划分，并验证受影响的等价类的转发行为。我们发现已有数据平面验证方法只能实现对纯IP转发设备的实时验证，而无法表达真实网络设备中存在ACL、NAT、策略路由等功能。此外，这些功能通常匹配除IP外的多个包头域（如五元组），导致等价类爆炸问题而无法在有效时间内完成验证。为此，我们提出APKeep实时网络正确性验证方法。APKeep用模块化的网络模型来表示真实网络设备的多种功能，并可快速的更新计算网络中的最小等价类，从而解决等价类爆炸问题，实现真正意义上的实时验证。基于包括IP转发规则和ACL规则的真实网络更新数据发现，已有方法或验证时间过长或内存溢出，而APKeep仍然可以在毫秒时间内完成增量验证。

张鹏，西安交通大学计算机学院副教授，博士生导师。2013年博士毕业于清华大学计算机科学与技术系，获清华大学优秀博士毕业生。主要研究方向为网络验证、软件定义网络、网络与信息安全。在USENIX NSDI、ACM CoNEXT、ACM HotNets、IEEE INFOCOM、IEEE ICNP、IEEE/ACM TON等国际会议和期刊上发表论文四十余篇。曾获中国计算机学会青年人才托举计划、西安交通大学王宽诚青年学者资助。现为中国计算机学会互联网专委会委员、网络与数据通信专委会委员。

地点：计算机科学技术楼230室