一句话：提出首个为网络数据平面计算精确且可高效监控的控制接口规范（ci-spec）的算法，并在真实程序中发现 bug。
网络程序验证因控制面与数据面分工而困难：控制面计算路由并生成设备配置，数据面依赖这些配置实现转发。数据面正确性常假设控制面配置满足复杂的控制接口规范（ci-spec），因此验证器、监控器、测试生成器必须知道这些规范，否则会产生误报。本文提出首个为网络数据平面计算精确 ci-spec 的算法。该规范可高效监控：检查固定配置是否满足 ci-spec 可在多项式时间内完成。算法基于模块化程序插桩、量词消去与路径分析，表达力优于先前工作且适用于实际网络程序。实现表明，所计算 ci-spec 能在真实数据平面程序中发现真实 bug。
Verifying network programs is challenging because of how they divide labor: the control plane computes high level routes through the network and compiles them to device configurations, while the data plane uses these configurations to realize the desired forwarding behavior. In practice, the correctness of the data plane often assumes that the configurations generated by the control plane will satisfy complex specifications. Consequently, validation tools such as program verifiers, runtime monitors, fuzzers, and test-case generators must be aware of these control interface specifications (ci-specs) to avoid raising false alarms. In this paper, we propose the first algorithm for computing precise ci-specs for network data planes. Our specifications are designed to be efficiently monitorable —concretely, checking that a fixed configuration satisfies a ci-spec can be done in polynomial time. Our algorithm, based on modular program instrumentation, quantifier elimination, and a path-based analysis, is more expressive than prior work, and is applicable to practical network programs. We describe an implementation and show that ci-specs computed by our tool are useful for finding real bugs in real-world data plane programs.
@article{CampbellHF24,
title = {Computing Precise Control Interface Specifications},
author = {Eric Hayden Campbell and Hossein Hojjat and Nate Foster},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689743}
}