Specification Language for Packet Parsers and Its Compiler Architecture

被引：0
|
作者：
Li H.-H. [1 ]
Li L. [1 ]
Zhao Y. [2 ]
Wang S.-Y. [1 ]
Li X.-Y. [3 ]
机构：
[1] Department of Computer Science and Technology, Tsinghua University, Beijing
[2] School of Applied Science, Beijing Information Science and Technology University, Beijing
[3] Institute of Microelectronics, Tsinghua University, Beijing
来源：
Ruan Jian Xue Bao/Journal of Software | 2020年 / 31卷 / 08期
关键词：
Domain-specific language; Formal semantics; Reconfigurable packet parser; Software-defined networking; Trustworthy compiler;
D O I：
10.13328/j.cnki.jos.005962
中图分类号：
学科分类号：
摘要：
This paper designs a domain-specific language P3 for reconfigurable protocol-independent packet parsers. Due to the requirement to facilitate the implementation of a high-security network, the language is designed from the perspective of high trustworthiness, including the formal definition of type system and operational semantics of the language and its trusted compiler architecture. Based on the full understanding of the basic requirements of the reconfigurable hardware, from the view of hardware-software codesign, the core characteristics of P3 language and its trusted compiler architecture named P3C are finally defined. As the reconfigurable packet parser is an important part of SDN and programmable data plane, implementing the trusted compiler architecture of P3C will be of great significance to the security of SDN. It is expected that the development of P3C project will promote the further research in the field of network and formal method. © Copyright 2020, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：2285 / 2308
页数：23
相关论文
共 22 条
  • [1] Broadcom BCM56850 StrataXGS®Trident II Switching Technology, (2013)
  • [2] Davie BS, Rekhter Y., MPLS: Technology and Applications, (2000)
  • [3] Hanks S, Meyer D, Farinacci D, Et al., Generic Routing Encapsulation (GRE), (2000)
  • [4] Mahalingam M, Dutt DG, Duda K, Et al., Virtual eXtensible local area network (VXLAN): A framework for overlaying virtualized layer 2 networks over layer 3 networks, RFC, 7348, (2014)
  • [5] McKeown N., Software-defined networking, INFOCOM Keynote Talk, 17, 2, pp. 30-32, (2009)
  • [6] Bosshart P, Gibb G, Kim HS, Et al., Forwarding metamorphosis: Fast programmable match-action processing in hardware for SDN, ACM SIGCOMM Computer Communication Review, 43, 4, pp. 99-110, (2013)
  • [7] Bosshart P, Daly D, Gibb G, Et al., P4: Programming protocol-independent packet processors, ACM SIGCOMM Computer Communication Review, 44, 3, pp. 87-95, (2014)
  • [8] Liu J, Hallahan W, Schlesinger C, Et al., P4v: Practical verification for programmable data planes, Proc. of the 2018 Conf. of the ACM Special Interest Group on Data Communication, pp. 490-503, (2018)
  • [9] Lopes N, Bjorner N, McKeown N, Et al., Automatically verifying reachability and well-formedness in P4 networks, Technical Report, (2016)
  • [10] Kheradmand A, Rosu G., P4K: A formal semantics of P4 and applications, (2018)
123