基于Armstrong的有状态数据平面上下文相关策略的可扩展测试
Scalable Testing of Context-Dependent Policies over Stateful Data Planes with Armstrong
摘要：
如今，网络运营商花费大量的人工努力来确保和检查网络满足他们的预期策略。虽然最近在网络验证方面的工作已经取得了巨大的进步，以减少这种努力，他们专注于简单的可达性属性，不能处理上下文相关的政策（例如，主机产生了多少连接），这是运营商使用有状态网络功能（NF）实现的。总之，这些引入了新的表现力和可扩展性挑战，这些挑战超出了现有网络验证机制的范围。为了解决这些挑战，我们提出了阿姆斯特朗，一个系统，使运营商能够测试，如果网络与有状态的数据平面元素正确地实现了一个给定的上下文相关的政策。我们的设计对解决表达性和可扩展性做出了三个关键贡献：（1）用于对网络I/O进行建模的抽象I/O单元，其编码策略相关的上下文信息;（2）通过有限状态机抽象的集合对复杂NF进行实际表示;以及（3）符号执行的可扩展应用程序，以解决状态空间爆炸。我们证明，阿姆斯特朗是几个数量级的速度比现有的机制。
英文摘要：
Network operators today spend significant manual effort in ensuring and checking that the network meets their intended policies. While recent work in network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context-dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful network functions (NFs). Together, these introduce new expressiveness and scalability challenges that fall outside the scope of existing network verification mechanisms. To address these challenges, we present Armstrong, a system that enables operators to test if network with stateful data plane elements correctly implements a given context-dependent policy. Our design makes three key contributions to address expressiveness and scalability: (1) An abstract I/O unit for modeling network I/O that encodes policy-relevant context information; (2) A practical representation of complex NFs via an ensemble of finite state machines abstraction; and (3) A scalable application of symbolic execution to tackle state space explosion. We demonstrate that Armstrong is several orders of magnitude faster than existing mechanisms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
