厦门大学系统与网络课题组的两项研究成果被网络领域研讨会Asia-Pacific Workshop on Networking (APNet 2023, CCF C类会议)录用。第7届APNet将于2023年6月29-30日在中国香港召开，本次会议共录取24篇论文，录取率为26.7%。

具体论文信息如下

Rulan Yang (厦门大学SNG二年级硕士生), Xing Fang (厦门大学SNG一年级博士生), Lizhao You (厦门大学SNG), Qiao Xiang (厦门大学SNG), Hanyang Shao (厦门大学SNG一年级硕士生), Gao Han, Ziyi Wang (厦门大学四年级本科生，已保研加入SNG), Zhihao Zhang (厦门大学SNG二年级博士生), Jiwu Shu (厦门大学，闽江学院), Linghe Kong (上海交通大学)

Diagnosing Distributed Routing Configurations Using Sequential Program Analysis

【论文简介】

本文首次将形式化方法中的静态分析技术和选择符号执行技术应用在网络故障诊断中，对网络进行数据流分析和控制流分析。文章提出了一种通过捕获路由进程间因果关系，将分布式路由计算转换成串行执行程序的方式。同时利用程序分析中的静态分析技术对网络仿真时的路由计算过程（即处理后的串行程序）进行自动化分析和诊断，从而定位网络配置错误。本文中用到的静态分析技术包括基于最小不可满足核和错误不变量的数据流分析，以及基于选择性符号执行的控制流分析技术。我们针对显式和隐式的网络错误分别采用不同的方法进行分析和诊断，结果表明两类方法都能在较短时间内有效定位到配置错误。

网络因果关系图到串行执行程序

路由的计算是由于进程间的路由传播或重分发触发的，因果关系即为引发和执行这些计算的路由进程间依赖关系。我们将路由进程抽象成程序，每次路由计算则是一次程序调用，通过捕获不同设备路由计算过程中的因果关系，每个目的前缀路由的计算过程都可以表示成一个有向无环图，如图1(b)，按拓扑序遍历该有向无环图即可得到对应的串行程序执行路径（同时包括仿真主循环计算顺序），如图1(c)。

数据流分析

显式错误是指网络中存在可观测到表项的错误，例如存在一条不满足意图的路由。对于这类错误，我们的做法是：将当前生成了错误表项的程序执行路径编码成SMT公式，然后计算该SMT公式的最小不可满足核得到最小错误语句集合（Minimal Unsatisfiable core， MUC），如图2红色语句集合，最后对集合中的每条语句计算错误不变量（即一系列导致错误表项生成的变量约束条件），如图2黄色语句集合。通过错误不变量分析和溯源错误原因，最后诊断MUC里的配置相关语句作为最小错误配置。

控制流分析

隐式错误是指网络中不可观测到表项的错误，例如某条预期的路由不存在。对于这类错误，我们的做法是：符号化网络的控制面行为，如邻居关系、路由的收发和优选行为等，如图3(a),选择性地符号执行一系列控制面行为来搜索预期的程序执行路径（即正确表项生成的执行路径），以此找到与实际行为不一致的路径条件，这些条件表示导致错误的所有控制面决策，每种条件都可以映射到相应的配置错误。此外，也可以从条件符号的生成顺序上分析错误产生的路由计算过程，如图3(b)。

对于可追溯的错误本系统能生成具有解释性的MUC和EI对。对于不可追溯的错误本系统支持诊断错误local-preference值、路由传播错误、和路由源发错误。实验结果（图4、5）显示对于可追溯和不可追溯的错误本系统均可在分钟级和秒级的时间内完成诊断。

具体论文信息如下

Huisan Xu (厦门大学SNG一年级硕士生), Qiuyue Qin (厦门大学SNG一年级硕士生), Xing Fang (厦门大学SNG一年级博士生), Qiao Xiang (厦门大学SNG), Jiwu Shu (厦门大学，闽江学院)

Toward Privacy-Preserving Interdomain Configuration Verification via Multi-Party Computation

【论文简介】

本文提出了首个适用于多管理域的网络验证系统。无论数据平面还是控制平面，现有的网络验证工具服务的主要对象都是单管理域网络。对于多管理域网络故障的检测手段还主要依赖于不同管理域的网络管理员进行人工沟通与排查。而部分实现自动化检测的多管理域网络验证工具需要将不同管理域的配置文件收集到某个可信赖的第三方，进行集中的控制平面验证。这些研究均要求每个管理域暴露自己的转发信息库或配置文件等隐私信息，存在安全隐患。

为了应对多管理域网络的网络故障检测问题，本文提出了基于安全多方计算的多管理域网络验证系统InCV (如下图所示)。该系统将对多管理域控制平面验证问题建模为域间路由的收敛性问题，并设计高效且保障隐私的路由模拟算法，在保障每个管理域不泄露自身转发信息库的前提下，验证多管理域网络控制平面的正确性。

高效的路由模拟算法

路由模拟算法DO-Simulation由若干次迭代组成，直到网络收敛。在每一次迭代中，选择一个RIB更改过的的路由器，并向其对等体发出路由通告，如下图所示。

本系统结合了FASTPLANE的路由模拟计算加速技术，通过选择合理的路由传播模拟次序，加快收敛速度，最终提升系统性能。FASTPLANE的关键思想是首先发送全局最优路由公告。然而，FASTPLANE由于不能执行撤回操作，通常应用于单调网络中。为了支持非单调网络，本系统进一步对路由撤回操作也进行了建模。

隐私保护的计算过程

数据无关（data-oblivious）是一种计算方法，它要求在执行计算时，所有操作都不会泄露关于输入数据的任何信息。本文设计了上述算法的data-oblivious版本并基于安全多方计算开源框架MP-SPDZ开发了InCV的原型系统。系统采用半诚实；诚实大多数的安全模型。初步实验结果表明InCV可在可接受时间开销内对中小型域间网络进行验证（在至多32个参与域的网络中以不超过52分钟耗时完成验证），并保护参与者配置隐私信息。

本次录用的两篇工作是厦门大学系统与网络课题组在网络与形式化方法结合方面的进一步探索。之前的研究工作包括Coral(HotNets’22),Solvability Digraph (INFOCOM’21)。