CNCC | 翟恩南、孙猛等领域内专家与你共同探讨——云网融合中的网络形式化方法前沿技术

张鹏

西安交通大学计算机学院教授/博导

CCF高级会员。2013年博士毕业于清华大学计算机科学与技术系，2009年于香港中文大学，2011年-2012年于耶鲁大学访问研究。主要研究方向为网络验证、软件定义网络、网络安全。在ACM SIGCOMM、USENIX NSDI、ACM CoNEXT、IEEE/ACM TON、IEEE JSAC等国际会议和期刊上发表论文四十余篇。曾获中国计算机学会青年人才托举计划、西安交通大学王宽诚青年学者资助。

向乔

厦门大学信息学院教授/博导

CCF高级会员、互联网专委会、网络与数据通信专委会、分布式计算与系统专委会委员。国家人力资源和社会保障部高层次留学人才；ACM/IEEE-CS/AAAI CS2023国际计算机科学课程体系改革工作组常务委员。2014年博士毕业于美国韦恩州立大学计算机科学系。2014-2020年在加拿大麦吉尔大学，美国耶鲁大学从事博士后与研究助理教授工作，主要研究方向为网络与形式化方法、可编程网络、高性能网络和物联网。在SIGCOMM, OSDI, FAST, EuroSys, INFOCOM, JSAC, TON等计算机网络与系统顶级学术会议与期刊发表论文70余篇，合著专著一部；主持国家重点研发计划课题，国自然面上等国家级科研项目；2019年获Facebook Research Award与IEEE MASS大会最佳论文奖；担任INFOCOM, DAC, IMC, IWQoS等国际会议程序委员会委员。

翟恩南

阿里云网络研究负责人，阿里云资深技术专家

CCF互联网专委会常委。2015 年于耶鲁大学计算机系获博士学位，随后担任耶鲁大学研究型助理教授，2018年加入阿里巴巴。研究领域包括计算机网络、分布式系统、程序验证等，先后在这些方向的国际顶级会议如SIGCOMM、OSDI、SOSP、NSDI等累计发表40余篇论文。担任SIGCOMM、NSDI等国际顶级会议程序委员会委员。获通信学会技术发明一等奖一次。

面向大规模云基础设施网络的形式化验证

作为全球最大的云提供商之一，阿里云为全球超过10亿用户提供了高质量的服务。随着每年规模的飞速增长，阿里云基础设施网络面临来自可靠性多方面的诸多挑战。本次报告首先为大家介绍阿里云基础设施网络的可靠性保障技术的现状，以及面临的挑战。然后详细介绍我们如何通过形式化验证技术解决这些挑战，这些核心技术不但以论文形式发表在 SIGCOMM、NSDI 和 SOSP 等国际顶会上，还已经被规模化运用在阿里云的日常运维中，保障阿里云的基础设施网络稳定性。

孙猛

北京大学数学科学学院信息与计算科学系教授/博导

CCF形式化方法专委会委员，中国工业与应用数学学会区块链专委会常务委员。分别于1999年和2005年获得北京大学应用数学学士和博士学位。2005年至2006年，在新加坡国立大学从事博士后研究，2006年至2010年在荷兰CWI担任研究员。2010年加入北京大学数学科学学院任助理教授，2017年任正教授。在TSE、ICSE、ESEC/FSE、AAAI、FM等国际期刊和会议上发表论文100余篇。他的研究兴趣主要是软件理论和形式化方法，特别是协作模型和语言、余代数理论及其应用、软件验证和测试、网络物理系统、区块链和智能合约、以及深度学习系统的理论基础和认证技术。

当区块链遇到形式化验证

区块链已成为各种去中心化金融技术应用的基础。区块链中的漏洞等安全问题可能会导致巨大损失。形式化验证技术被用来保证复杂硬件和软件系统的质量和可信度。本次报告将展示如何利用形式化验证技术来确保基于区块链的系统的可信度。作为案例分析，报告将讨论如何对以太坊虚拟机（EVM）行为和CKB区块链中典型协议进行建模和验证。不同验证技术的组合，如模型检验、定理证明等，为分析和验证基于区块链的系统提供了强有力的支撑。

王竟亦

浙江大学研究员/博导

分别于2013年和2018年从西安交通大学和新加坡科技设计大学获得学士和博士学位，新加坡国立大学Research Fellow。致力于使用形式化方法、软件工程助力构建更加安全可信的智能化、网络化系统和装备（如工业控制系统/装备、人工智能系统、区块链系统等）。相关研究成果在形式化方法、安全与隐私、软件工程等领域国际顶级会议和期刊如S&P、CCS、ICSE、TSE、FM、TACAS等发表论文30余篇（含CCF A类近20篇）。两次获得ACM SIGSOFT杰出论文奖（ICSE 2018和ICSE 2020)，并入选ACM SIGSOFT Research Highlights。主持或承担国家重点研发计划项目、浙江省 “尖兵”研发攻关计划项目、国家自然科学基金青年项目、CCF-华为胡杨林基金等。

大模型驱动安全协议自动化建模技术初探

面向安全协议的形式化验证工具如Tamarin、Proverif等在保障网络协议安全性方面具有重要价值。然而，使用该类工具进行形式化建模需要较多的交叉领域专家知识，易出错而代价高。近来，诸如ChatGPT等大语言模型在包括代码生成等自然语言处理任务上有了突破性进展。本报告将介绍我们最近在基于大语言模型自动化生成面向安全验证的安全协议形式化符号模型方面的初步探索。该工作受到CCF-华为胡杨林基金形式化方法专项资助。

卜磊

南京大学软件学院教授/博导

主要研究领域是软件工程与形式化方法，包括模型检验技术，实时混成系统，信息物理融合系统等方向。2010年在南京大学获取计算机博士学位。曾在CMU、MSRA等科研机构进行访学与合作研究。相关工作发表于领域重要期刊与会议如TCAD、TC、TDSC、RTSS、HSCC等。入选国家级青年人才计划，NASAC青年软件创新奖，高校计算机专业优秀教师奖励计划，CCF-IEEE CS青年科学家奖等。

门神：事件驱动型物联网形式化建模、验证及修复

随着现代信息技术的不断发展，物联网已经进入各个领域，并得到了广泛应用。特别是以 IFTTT框架为代表的事件驱动型物联网系统构建机制极大便利了普通用户通过编写简单事件驱动规则来快捷、高效地按需构建自己的智能物联网系统。但是，这一普通使用的机制背后存在严峻的安全问题。普通用户对其设计的规则所带来的系统行为缺乏完整理解，随着规则数目增长，系统复杂度急剧上升，难以整体把握。在此之外，相关物联网设备可能受到外界攻击，其组网后，整体系统的安全性进一步面临巨大挑战。因此，帮助用户对其自构建的事件驱动型物联网系统进行自动化安全检验是一项十分重要的工作。本报告将对我们在面向事件驱动型物联网系统的自动化建模和安全检验技术研究，及所开发的工具“门神”进行介绍。门神综合考虑智能家居系统安全相关因素，对智能家居系统进行自动化建模，使用模型检验方法对系统安全性进行验证，并进一步对所发现的风险进行修复，实现对相关系统的可信增强。

李福亮

东北大学计算机学院副教授/博导

CCF互联网专委会执行委员、体系结构专委会委员。主要研究方向为未来网络技术、网络智能运维等；主持国家级项目6项，主持华为、字节跳动、阿里巴巴合作项目6项；第一及通讯作者发表学术论文30余篇，申请发明专利10余项，出版学术专著6部；入选辽宁省百千万人才工程、沈阳市高层次人才计划；获沈阳市中青年科技创新人才、辽宁省通信学会优秀科技工作者等荣誉称号。

网络配置合成技术探索与实践

互联网的规规模不断扩大，网络设备支持的服务和功能越来越多，人工手动配置难以应对复杂的网络配置需求，导致配置错误频发。针对上述问题，研究网络配置自动合成方法，用以提高配置效率，降低配置出错的概率。报告具体介绍内容包括：配置合成技术概述、可解释配置合成技术、配置翻译技术、意图驱动配置技术等。