一种包解析器硬件配置描述语言及其编译结构-李璜华，李凌，赵宇，王生原，李翔宇.pdf
免费下载
软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2020,31(8):2285−2308 [doi: 10.13328/j.cnki.jos.005962] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563
一种包解析器硬件配置描述语言及其编译结构
∗
李璜华
1
,
李
凌
1
,
赵
宇
2
,
王生原
1
,
李翔宇
3
1
(清华大学 计算机科学与技术系,北京 100084)
2
(北京信息科技大学 理学院,北京 100192)
3
(清华大学 微电子学研究所,北京 100084)
通讯作者: 王生原, E-mail: wwssyy@mail.tsinghua.edu.cn
摘 要: 设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言 P3.由于要有利于高安全等级
网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信
编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了 P3 语言的核心特性及其编
译器 P3C 的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实
现 P3C 的可信编译结构将对 SDN 的安全性具有重大意义.期待 P3C 项目的开展能够促进网络与形式化领域相关工
作的进一步研究.
关键词: 领域专用语言;可重构数据包解析器;形式语义;可信编译;软件定义网络
中图法分类号: TP314
中文引用格式: 李璜华,李凌,赵宇,王生原,李翔宇.一种包解析器硬件配置描述语言及其编译结构.软件学报,2020,31(8):
2285−2308. http://www.jos.org.cn/1000-9825/5962.htm
英文引用格式: Li HH, Li L, Zhao Y, Wang SY, Li XY. Specification language for packet parsers and its compiler architecture.
Ruan Jian Xue Bao/Journal of Software, 2020,31(8):2285−2308 (in Chinese). http://www.jos.org.cn/1000-9825/5962.htm
Specification Language for Packet Parsers a nd Its Com piler Architecture
LI Huang-Hua
1
, LI Ling
1
, ZHAO Yu
2
, WANG Sheng-Yuan
1
, LI Xiang-Yu
3
1
(Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China)
2
(School of Applied Science, Beijing Information Science and Technology University, Beijing 100192, China)
3
(Institute of Microelectronics, Tsinghua University, Beijing 100084, China)
Abstra ct : 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.
Key words: domain-specific language; reconfigurable packet parser; formal semantics; trustworthy compiler; software-defined
networking
∗ 基金项目: 核高基国家科技重大专项(2017ZX01030-301-003)
Foundation item: CHB National Science and Technology Major Project of China (2017ZX01030-301-003)
本文由“面向新兴系统的形式化建模与验证方法”专题特约编辑陈振邦副教授、冯新宇教授、刘志明教授推荐.
收稿时间: 2019-08-31; 修改时间: 2019-11-02; 采用时间: 2019-12-30; jos 在线出版时间: 2020-04-18
2286
Journal of Software 软件学报 Vol.31, No.8, August 2020
互联网的实现,需要相应的网络设备对网络数据包进行处理和转发.考虑到处理速度,目前大多数的交换机
芯片都是采用固定功能的专用硬件实现,如 Broadcom 公司的 Trident
[1]
芯片.这样的交换机一经部署,就只能支
持固定的网络协议,它具有很明显的缺陷.
• 首先,近年来,互联网产业发展迅猛,各种新型网络技术层出不穷,出现了大量的新型协议如 MPLS
[2]
,
GRE
[3]
等.为了适应这些新的网络协议,运营商只能反复更新网络的中转设备.然而开发新的硬件并推
广一个新的硬件标准是十分花费时间和金钱的,如 VxLAN
[4]
协议在其被提出 3 年后才被新的硬件标准
支持.
• 其次,这种固定功能的硬件设备往往采用“自底向上”的设计模式,在这种设计模式下,设计者需要首先
考虑芯片的数据清单,确认硬件的资源能满足设计的要求后,再规划好如何利用这些资源,然后在这之
上设计功能的实现.这对于设计者来说是十分不方便的,因为设计者往往更自然地以“自顶向下”的方
式来考虑问题,即设计数据包的解析、处理和转发等过程的逻辑,而不愿意考虑硬件的实现细节.
为了提高网络中转设备的通用性和灵活性、简化开发者的开发过程,相关研究人员做出了大量的努力.
软件定义网络(software-defined networking,简称 SDN)
[5]
将控制平面和数据平面分离,给予操作者对控制平
面进行编程的能力,由控制平面通过统一、标准的接口对不同的网络设备进行配置和管理.通过这种方式,SDN
把网络设备逐渐变为可编程的软件平台,操作者可以“自顶向下”地通过编程决定各网络设备的行为.
2013 年,Bosshart 等人提出了可编程交换机的抽象转发模型
[6]
,为实现可编程数据平面提供了可能.在这个
模型中,数据包在进行转发时会通过一连串的可重配置的匹配动作表(reconfigurable match-action tables,简称
RMT),通过对这些灵活的匹配动作表的重新配置,就可以使交换机支持不同的对数据包的处理、转发方式.2014
年,Bosshart 等人在抽象转发模型的基础上进一步提出了 P4 语言
[7]
,为可编程交换机提供了一种高级编程语
言.P4 语言专注于描述数据包在匹配动作表中被处理的逻辑过程,并通过相应的编译器实现其到具体硬件的配
置,符合“自顶向下”的设计模式.P4 具有对数据平面的重配置能力、协议无关性以及目标硬件无关性,极大地提
高了对交换机编程的通用性和灵活性,也方便代码的跨平台迁移.自此,可编程数据平面逐渐兴起,SDN 的潜能
得到了更大的开发.
软件的安全性始终是软件工作者感兴趣的话题,随着 P4 的兴起,软件工作者也开始尝试用形式化方法来验
证 P4 程序的可靠性,从而提高 SDN 的安全性.2018 年,Liu 等人
[8]
设计并开发了一个用于 P4 程序正确性验证的
工具 P4v,该工具首先将 P4 程序转译为 GCL(guarded command language),然后通过添加特定注释并利用符号执
行技术来验证 P4 程序的逻辑正确性.作者在他们的工作中指出,相关的开源 P4 编译器是存在 bug 的,因此他们
构建了一个独立的编译器前端包括解析器、类型检查以及到 GCL 的翻译器.尽管这极大地提高了 P4 程序的可
信度,但 P4 程序和转换的 GCL 之间的一致性仍然是难以保证的,所以 Liu 等人也把设计一个可验证的编译器甚
至可验证的硬件作为感兴趣的未来研究工作.Lopes 等人研究实现了一个基于 Z3 求解器的原型工具
[9]
,可用于
验证 P4 编译过程(verifying P4 compilation).Kheradmand 等人为 P4 语言定义了一种基于 K-框架的形式语义
[10]
,
并借助 K-框架近期开发的原型工具 KEQ
[11]
,给出一种实现 P4 编译过程的翻译确认
[12]
解决方案.
交换机在工作时,第 1 步是实现数据包的解析.为了实现解析器的快速设计,Benacek 等人
[13]
将 P4 语言编写
的解析器程序映射到固定的硬件架构中,可以快速生成解析器对数据包进行灵活的解析,但没有实现资源的复
用.李翔宇课题组为此提出了一种通过静态配置可以实现不同解析逻辑的数据包解析器基本处理单元(process
element,简称 PE)
[14]
,经由编译器(本文工作)生成的配置文件配置后,可用于任何一层协议(可自定义)的解析,并
通过流水线式级联的方式来搭建可以支持各种协议集合的可重构数据包解析器,具有更少的资源占用率、更好
的性能和更高的灵活性.本文工作的出发点之一就是围绕这一可重构数据包解析器进行软硬件协同设计,提出
并实现一种与硬件设计匹配的硬件配置描述语言.
本文工作的大背景是服务于一种高安全交换芯片的设计与实现,需要从高安全可信的角度设计和实现这
种硬件配置描述语言,因此提出 P3 语言(specification language for reconfigurable protocol-independent packet
parsers).P3 语言比 P4 语言要简单很多,仅面向上述可重构数据包解析器的设计.P4 语言描述的是整个数据平面,
of 24
免费下载
【版权声明】本文为墨天轮用户原创内容，转载时必须标注文档的来源（墨天轮），文档链接，文档作者等基本信息，否则作者和墨天轮有权追究责任。如果您发现墨天轮中有涉嫌抄袭或者侵权的内容，欢迎发送邮件至：contact@modb.pro进行举报，并提供相关证据，一经查实，墨天轮将立刻删除相关内容。
下载排行榜
评论