ACM通信

软件Dataplane验证

业界正热衷于可编程网络，运营商可以在网络设备上动态部署网络功能，类似于在云环境中的物理机器上部署虚拟机。这种灵活性带来了不可预测的行为和性能的威胁。我们需要对网络功能施加的最小限制是什么，以使我们能够验证网络设备的行为和执行如预期的那样，例如，不会崩溃或进入无限循环?我们介绍了在两个任务上迭代工作的结果:为包处理软件设计一个特定于领域的验证工具，同时试图确定包处理软件必须满足的最小限制集，以实现验证友好。我们的主要见解是，包处理软件是领域特定验证的一个很好的候选者，例如，因为它通常由不同的代码片段组成，共享有限的可变状态;我们可以利用这个属性和其他属性来避开基本的验证挑战。我们将我们的想法应用于Click包处理软件;我们可以在几十分钟内完成一个IP路由器和两个简单的中间箱的完整和可靠的验证，而最先进的通用工具却不能在几个小时内完成相同的任务。

回到顶部

1.简介

网络设备应该向操作员公开什么样的编程接口?回答这个问题涉及到灵活性和可验证性之间的基本权衡:我们选择的接口越灵活，我们可以在网络设备上部署的功能范围就越广，但是验证网络设备将按照预期行为和执行就越困难，例如，无论我们如何配置它或它接收到什么流量，它都不会崩溃。

没有发现记录

登录阅读全文