Synthesizing safe and efficient kernel extensions for packet processing
Synthesizing safe and efficient kernel extensions for packet processing
复制标题
综合安全高效的内核扩展进行数据包处理
DOI：
10.1145/3452296.3472929
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Sivaraman, Anirudh
中科院分区：
文献类型：
--
作者：
Xu, Qiongwen;Wong, Michael D.;Wagle, Tanvi;Narayana, Srinivas;Sivaraman, Anirudh
扩展的Berkeley包过滤器（BPF）已经成为一种在Linux操作系统中扩展包处理功能的强大方法。BPF允许用户用高级语言（如C或Rust）编写代码，并在内核中的特定钩子（如网络设备驱动程序）上执行它们。为了确保在内核环境中安全执行用户开发的BPF程序，Linux使用内核内静态检查器。检查器只允许程序执行，如果它能证明程序是无崩溃的，总是在安全范围内访问内存，并避免泄漏内核数据。第一，即使是中等大小的BPF程序也会被认为太大而无法分析，并被内核检查器拒绝。第二，内核检查器可能会错误地确定BPF程序表现出不安全的行为。三，即使是对BPF代码的小性能优化（例如，5%的收益）必须由专家开发人员精心手工制作。传统的BPF优化编译器往往是不够的，因为内核检查器的安全约束是不兼容的基于规则的优化。我们提出了K2，一个基于程序合成的编译器，自动优化BPF字节码的形式正确性和安全性的保证。相对于最好的clang编译程序，K2产生的代码大小减少了6- 26%，平均数据包处理延迟降低了1.36%-55.03%，吞吐量（每个核心每秒的数据包）提高了0- 4.75%，这些都是从Cilium，Facebook和Linux内核中提取的基准测试。K2结合了几种特定领域的技术，通过将BPF程序的等价性检查加速6个数量级来实现合成。
Extended Berkeley Packet Filter (BPF) has emerged as a powerful method to extend packet-processing functionality in the Linux operating system. BPF allows users to write code in high-level languages (like C or Rust) and execute them at specific hooks in the kernel, such as the network device driver. To ensure safe execution of a user-developed BPF program in kernel context, Linux uses an in-kernel static checker. The checker allows a program to execute only if it can prove that the program is crash-free, always accesses memory within safe bounds, and avoids leaking kernel data.BPF programming is not easy. One, even modest-sized BPF programs are deemed too large to analyze and rejected by the kernel checker. Two, the kernel checker may incorrectly determine that a BPF program exhibits unsafe behaviors. Three, even small performance optimizations to BPF code (e.g., 5% gains) must be meticulously hand-crafted by expert developers. Traditional optimizing compilers for BPF are often inadequate since the kernel checker's safety constraints are incompatible with rule-based optimizations.We present K2, a program-synthesis-based compiler that automatically optimizes BPF bytecode with formal correctness and safety guarantees. K2 produces code with 6--26% reduced size, 1.36%--55.03% lower average packet-processing latency, and 0--4.75% higher throughput (packets per second per core) relative to the best clang-compiled program, across benchmarks drawn from Cilium, Facebook, and the Linux kernel. K2 incorporates several domain-specific techniques to make synthesis practical by accelerating equivalence-checking of BPF programs by 6 orders of magnitude.
登录
查看更多内容
DOI：
10.1145/3458336.3465281
发表时间：
2021-06
期刊：
Proceedings of the Workshop on Hot Topics in Operating Systems
影响因子：
--
作者：
Hugo Sadok;Zhipeng Zhao;Valerie Choung;Nirav Atre;Daniel S. Berger;J. Hoe;Aurojit Panda;Justine Sherry
通讯作者：
Hugo Sadok;Zhipeng Zhao;Valerie Choung;Nirav Atre;Daniel S. Berger;J. Hoe;Aurojit Panda;Justine Sherry
DOI：
--
发表时间：
2019-07
期刊：
--
影响因子：
--
作者：
Dmitry Duplyakin;R. Ricci;Aleksander Maricq;Gary Wong;Jonathon Duerig;E. Eide;L. Stoller;Mike Hibler;David Johnson;Kirk Webb;Aditya Akella;Kuang-Ching Wang;Glenn Ricart;L. Landweber;C. Elliott;M. Zink;E. Cecchet;Snigdhaswin Kar;Prabodh Mishra
通讯作者：
Dmitry Duplyakin;R. Ricci;Aleksander Maricq;Gary Wong;Jonathon Duerig;E. Eide;L. Stoller;Mike Hibler;David Johnson;Kirk Webb;Aditya Akella;Kuang-Ching Wang;Glenn Ricart;L. Landweber;C. Elliott;M. Zink;E. Cecchet;Snigdhaswin Kar;Prabodh Mishra
RockSalt：针对 x86 的更好、更快、更强的 SFI
DOI：
10.1145/2254064.2254111
发表时间：
2012
期刊：
Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Greg Morrisett;Gang Tan;Joseph Tassarotti;Jean;Edward Gan
通讯作者：
Edward Gan
DOI：
10.1145/3385412.3386027
发表时间：
2020
期刊：
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Huang, Kangjing;Qiu, Xiaokang;Shen, Peiyuan;Wang, Yanjun
通讯作者：
Wang, Yanjun
DOI：
10.1145/3179425
发表时间：
2018
期刊：
Proceedings of the ACM on Measurement and Analysis of Computing Systems
影响因子：
--
作者：
Subramanian, Kausik;D'Antoni, Loris;Akella, Aditya
通讯作者：
Akella, Aditya