Uncovering Bugs in P4 Programs with Assertion-based Verification
Uncovering Bugs in P4 Programs with Assertion-based Verification
复制标题
DOI：
10.1145/3185467.3185499
复制
发表时间：
2018-03
期刊：
影响因子：
--
通讯作者：
Lucas Freire;M. Neves;Lucas Leal;Kirill Levchenko;A. E. S. Filho;M. Barcellos
中科院分区：
文献类型：
--
作者：
Lucas Freire;M. Neves;Lucas Leal;Kirill Levchenko;A. E. S. Filho;M. Barcellos
软件定义网络的最新趋势通过P4等编程语言将网络可编程性扩展到数据平面。不幸的是，在这种新情况下，在网络中引入错误的机会也大大增加。现有的数据平面验证方法无法建模P4程序，或者它们在可以建模的一系列属性中施加了严格的限制。在本文中，我们基于断言检查和符号执行介绍了数据平面程序验证方法。网络程序员注释P4程序，并具有表达一般安全性和正确性属性的断言。一旦注释，这些程序就会转换为基于C的模型，并且它们所有可能的路径象征性执行。结果表明，所提出的称为assert-p4的方法可以发现广泛的错误和软件缺陷。此外，实验评估表明，验证文献中提出的各种P4应用所需的时间不到一分钟。
Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.