Verification of P4 Programs in Feasible Time Using Assertions
Verification of P4 Programs in Feasible Time Using Assertions
复制标题
使用断言在可行时间内验证 P4 程序
DOI：
10.1145/3281411.3281421
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Barcellos, Marinho
中科院分区：
文献类型：
--
作者：
Neves, Miguel;Freire, Lucas;Schaeffer-Filho, Alberto;Barcellos, Marinho
软件定义网络的最新趋势已将网络可编程性扩展到数据平面。不幸的是，引入错误的机会显着增加。验证可以通过确保程序不违反其需求来帮助防止错误。虽然P4程序的验证研究非常活跃，但我们仍然需要工具来使程序员更容易地表达属性并快速验证复杂的不变量。在本文中，我们利用断言和符号执行，提出了一个更一般的P4验证方法。开发人员用表示一般网络正确性属性的断言来注释P4程序;结果被转换为C模型，所有可能的路径都被符号化地执行。我们实现了一个原型，并使用它来显示验证方法的可行性。由于符号执行不能很好地扩展，我们研究了一套技术，以加快P4程序的特定情况下的过程。我们使用的原型实现显示三个加速技术（使用约束，程序切片，并行化）提供的收益，并与不同的编译器优化选择实验。我们展示了我们的工具可以发现广泛的错误，并且可以在不到一分钟的时间内完成各种P4应用程序。
Recent trends in software-defined networking have extended network programmability to the data plane. Unfortunately, the chance of introducing bugs increases significantly. Verification can help prevent bugs by assuring that the program does not violate its requirements. Although research on the verification of P4 programs is very active, we still need tools to make easier for programmers to express properties and to rapidly verify complex invariants. In this paper, we leverage assertions and symbolic execution to propose a more general P4 verification approach. Developers annotate P4 programs with assertions expressing general network correctness properties; the result is transformed into C models and all possible paths symbolically executed. We implement a prototype, and use it to show the feasibility of the verification approach. Because symbolic execution does not scale well, we investigate a set of techniques to speed up the process for the specific case of P4 programs. We use the prototype implemented to show the gains provided by three speed up techniques (use of constraints, program slicing, parallelization), and experiment with different compiler optimization choices. We show our tool can uncover a broad range of bugs, and can do it in less than a minute considering various P4 applications.