Safe, modular packet pipeline programming
Safe, modular packet pipeline programming
复制标题
安全、模块化的数据包管道编程
DOI：
10.1145/3498699
复制
发表时间：
2022
影响因子：
--
通讯作者：
Walker, David
中科院分区：
文献类型：
--
作者：
Loehr, Devon;Walker, David
P4语言和可编程交换机硬件(如Intel Tofino)使网络工程师能够编写新的程序来定制计算机网络的操作，从而提高性能、容错能力、能源使用和安全性。不幸的是，可能并不意味着容易--如果程序员希望他们的程序编译成专门的网络硬件，他们必须遵守许多隐含的限制。特别是，同一交换机上的所有计算必须以一致的顺序访问数据结构，否则无法沿交换机的数据包处理流水线布局数据。在本文中，我们定义了Lucid2.0，这是一种新的语言和类型系统，它保证程序以一致的顺序访问数据，从而是流水线安全的。Lucid 2.0构建在最初的Lucid语言之上，Lucid语言也是管道安全的，但缺乏数据结构库模块化构建所需的功能。因此，Lucid 2.0增加了(1)代码重用的多态和排序约束；(2)抽象的、分层的流水线位置和数据类型，以支持信息隐藏；(3)编译时构造函数、向量和循环，以允许构造灵活的数据结构；以及(4)类型推理，以减轻程序注释的负担。我们发展了Lucid2.0的元理论，证明了它的可靠性，并展示了如何将约束检查编码为SMT问题。我们通过开发一套有用的网络库和应用程序来展示Lucid 2.0的效用，这些程序利用了我们的新语言功能，包括Bloom过滤器、草图、布谷鸟哈希表、分布式防火墙、DNS反射防御、网络地址转换器(NAT)和概率流量监控服务。
The P4 language and programmable switch hardware, like the Intel Tofino, have made it possible for network engineers to write new programs that customize operation of computer networks, thereby improving performance, fault-tolerance, energy use, and security. Unfortunately,possibledoes not meaneasy—there are many implicit constraints that programmers must obey if they wish their programs to compile to specialized networking hardware. In particular, all computations on the same switch must access data structures in a consistent order, or it will not be possible to lay that data out along the switch’s packet-processing pipeline. In this paper, we define Lucid 2.0, a new language and type system that guarantees programs access data in a consistent order and hence arepipeline-safe. Lucid 2.0 builds on top of the original Lucid language, which is also pipeline-safe, but lacks the features needed for modular construction of data structure libraries. Hence, Lucid 2.0 adds (1) polymorphism and ordering constraints for code reuse; (2) abstract, hierarchical pipeline locations and data types to support information hiding; (3) compile-time constructors, vectors and loops to allow for construction of flexible data structures; and (4) type inference to lessen the burden of program annotations. We develop the meta-theory of Lucid 2.0, prove soundness, and show how to encode constraint checking as an SMT problem. We demonstrate the utility of Lucid 2.0 by developing a suite of useful networking libraries and applications that exploit our new language features, including Bloom filters, sketches, cuckoo hash tables, distributed firewalls, DNS reflection defenses, network address translators (NATs) and a probabilistic traffic monitoring service.
登录
查看更多内容
TurboEPC：利用数据平面可编程性来加速移动分组核心
DOI：
10.1145/3373360.3380839
发表时间：
2020
期刊：
Proceedings of the Symposium on SDN Research
影响因子：
--
作者：
Rinku Shah;Vikash Kumar;Mythili Vutukuru;Purushottam Kulkarni
通讯作者：
Purushottam Kulkarni
DOI：
10.1145/3387514.3405852
发表时间：
2020-07
期刊：
Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication
影响因子：
--
作者：
Xiangyu Gao;Taegyun Kim;Michael D. Wong;Divya Raghunathan;A. Varma;Pravein G. Kannan;Anirudh Sivaraman;S. Narayana;Aarti Gupta
通讯作者：
Xiangyu Gao;Taegyun Kim;Michael D. Wong;Divya Raghunathan;A. Varma;Pravein G. Kannan;Anirudh Sivaraman;S. Narayana;Aarti Gupta
DOI：
--
发表时间：
2019-02
期刊：
--
影响因子：
--
作者：
Kuo-Feng Hsu;Ryan Beckett;Ang Chen;J. Rexford;Praveen Tammana;D. Walker
通讯作者：
Kuo-Feng Hsu;Ryan Beckett;Ang Chen;J. Rexford;Praveen Tammana;D. Walker
DOI：
--
发表时间：
2021
期刊：
--
影响因子：
--
作者：
Zaoxing Liu;Hun Namkung;G. Nikolaidis;Jeongkeun Lee;Changhoon Kim;Xin Jin;V. Braverman;Minlan Yu-Minlan
通讯作者：
Zaoxing Liu;Hun Namkung;G. Nikolaidis;Jeongkeun Lee;Changhoon Kim;Xin Jin;V. Braverman;Minlan Yu-Minlan
DOI：
--
发表时间：
1999
期刊：
International Conference on Typed Lambda Calculus and Applications
影响因子：
--
作者：
Jeff Polakow;F. Pfenning
通讯作者：
F. Pfenning