网络验证这件事,过去十几年一直有个尴尬的边界:能证明的事太少,真实协议里要干的活太多。
一伙横跨美欧高校与一家量化公司的研究者,刚刚把这条边界往前推了一截。他们给一类经典的网络验证语言塞进了一颗栈,并证明这颗栈不会让”判别两段程序是不是在做同一件事”变成无解问题。这种”加一种能力 + 留一份可判定性”的组合,在程序语言圈子里不算常见。
一、NetKAT 之所以够用,又之所以不够用
NetKAT 是过去十年里最被工程界用熟的网络验证语言之一。它的”够用”在于:交换机、控制器、转发规则,几乎都可以被压成几条 Kleene 代数表达式。当你只想问”这一跳去哪儿”的时候,它的判定过程跑得相当利索。
它的”不够用”在于:真实的协议常常要”剥一层再看下一层”。多协议标签交换是这样:进来一个包,先看最外层标签决定下一跳,剥掉这一层,接着看里面一层;源路由是这样:进来的包里藏着一串路径;带内遥测也是这样:每经过一跳,就要在包头里再追加一段统计信息。这些动作在 NetKAT 里要么写得很别扭,要么干脆写不出来。原因是它本质上是一个”平面正则”的世界,没有递归,也没有”我刚刚才解析过什么”的记忆。
二、把栈塞进去,等价性还判得动吗
新工作的核心思路,用一个不那么学术的比喻,是给 NetKAT 装上一颗手写的栈。
具体一点:把”已经被解析过的协议头”看作一组有限状态变量,把”还没解析的部分”看作栈。每解析一层就把对应字段抽到变量里;每需要往里追加信息就执行一次入栈。源路由是天然的栈:路径就是栈里的一个个元素;带内遥测也是:每跳一次就推一段新统计。
麻烦的地方在于,一旦允许栈的存在,理论上的等价性判定通常会爆炸——两个带栈的程序,行为上是不是等价,经常是一个不可判定的问题。新工作的关键,是把这种”无限状态”的危险挡在了门外:虽然栈本身可以长,但能取的值被有限状态变量约束住了,因此可以用有限自动机的视角去理解。
三、自动机:把”两段程序是否同义”做成机械动作
判定过程是这样的:把两段程序各自翻译成自动机,再判断这两台自动机接受的语言是否完全一致。这一步对熟悉正则语言的读者并不陌生,真正的难点是”翻译”这一步——怎么把一颗带栈的程序,正确地压成一台自动机而不丢语义。
论文给出的构造方法比较干净:把”变量当前取什么值”作为自动机的状态分量,把”栈顶此刻是谁”作为状态上的标签。于是一段程序就变成了一台状态空间有限的机器。两段程序之间是否等价,变成两台机器语言是否一致——这一类问题有非常成熟的判定工具。
反过来,当两段程序不等价时,这套流程还能自动给出反例:一个具体的输入包,在两段程序下走出不同的路径。反例的存在,让”看起来差不多”的网络配置,有了被真正排除的机会。
四、完备的公理化:语义和语法第一次对齐
在程序语言的研究里,”公理化”是检验语言是否”语义清晰”的一把硬尺。它的意思是:能不能列出一组有限的推理规则,使得”语法上能推出来的等价”和”语义上真的等价”完全重合?
对新语言来说,给出这样一组规则并不是必须的——很多语言只给出”算法判等价”,却没能在语法层面写下一个对得上的公理系统。新工作的另一个贡献,就是给出了这样的公理化系统,并在论文中证明了它是完备的。这意味着,工程师可以靠手写几条代数定律去推导两段程序的等价,而不必每次都启动判定过程。
五、这件事跟现实网络有什么关系
把这套理论直接拿去做生产网络验证,还需要相当多的工程化工作。但是它的语言能力,正好卡在几类今天越来越常见的协议行为上。
一类是可编程数据面:用户态交换机、网卡上的协议解析、可重写的包头处理流水线——这些场景天然需要”剥一层、看一层、决定下一步”。另一类是网络遥测:让包自己记录沿途路径,而不是让运维事后去捞日志;这种”在包上原地写一行”的动作,在新语言里就是一次入栈。还有一类是协议验证器的设计空间:一旦能用更接近协议的表达方式来建模,就能在更高的层面写”等价的优化”,而不是钻在每一台设备的配置里。
六、程序语言视角的小胜利
从更宽的角度看,这种工作的价值不在于立刻改变工程实践,而在于把”程序代数 + 自动机 + 网络验证”三条原本互不相干的线缝合成了一根针。它提醒工程师:一种受限的递归,如果限制得当,是可以同时获得”真实表达力”和”判定能力”的。这种”既要又要”的小胜利,是程序语言研究在工程领域里长期被低估的输出方式。
接下来,真正有意思的下一步,是把这种”带栈的可判定验证”和工业级的协议解析器对接到一起。当一台真实的交换机或网卡可以用这套语言描述它的全部协议处理逻辑,并且能在编译期被证明”和上一版本语义一致”的时候,网络配置升级这件事,就有可能从”挑灯夜战”,变成”机械可证”的小事。