Extended Berkeley Packet Filter (BPF) is a language and run-time system that allows non-superusers to extend the Linux and Windows operating systems by downloading user code into the kernel. To ensure that user code is safe to run in kernel context, BPF relies on a static analyzer that proves properties about the code, such as bounded memory access and the absence of operations that crash. The BPF static analyzer checks safety using abstract interpretation with several abstract domains. Among these, the domain of tnums (tristate numbers) is a key domain used to reason about the bitwise uncertainty in program values. This paper formally specifies the tnum abstract domain and its arithmetic operators. We provide the first proofs of soundness and optimality of the abstract arithmetic operators for tnum addition and subtraction used in the BPF analyzer. Further, we describe a novel sound algorithm for multiplication of tnums that is more precise and efficient (runs 33% faster on average) than the Linux kernel's algorithm. Our tnum multiplication is now merged in the Linux kernel.


翻译:伯克利扩展包件过滤器( BPF) 是一种语言和运行时间系统, 允许非超级用户通过将用户代码下载到内核, 扩展 Linux 和 Windows 操作系统。 为确保用户代码在内核环境中运行安全, BPF 依赖于静态分析器, 以证明代码的属性, 如连接内存访问和崩溃时没有操作 。 BPF 静态分析器使用若干抽象域进行抽象解释, 检查安全性。 其中, tnums 域( 三角数) 是一个关键域, 用来解释程序值中比错误的不确定性。 本文正式指定了调子抽象域及其算术操作员 。 我们提供了抽象算术操作员在 BPF 分析器中使用的 tnuum 添加和减法 的正确性和最佳性的初步证明 。 此外, 我们描述比 Linux 内核内核算法更精确、更高效的倍性新声音算法( 平均跑33% ) 。 我们的倍增法现已合并成 Linux 。

0
下载
关闭预览

相关内容

卷积神经网络中的注意力机制综述
专知会员服务
75+阅读 · 2021年10月22日
最新《深度学习人体姿态估计》综述论文,26页pdf
专知会员服务
38+阅读 · 2020年12月29日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python图像处理,366页pdf,Image Operators Image Processing in Python
最新《医学图像深度语义分割》综述论文
专知会员服务
94+阅读 · 2020年6月7日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
【CNN】一文读懂卷积神经网络CNN
产业智能官
18+阅读 · 2018年1月2日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
【学习】(Python)SVM数据分类
机器学习研究会
6+阅读 · 2017年10月15日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Arxiv
7+阅读 · 2021年10月12日
Interpretable CNNs for Object Classification
Arxiv
20+阅读 · 2020年3月12日
Interpretable Adversarial Training for Text
Arxiv
5+阅读 · 2019年5月30日
VIP会员
相关VIP内容
卷积神经网络中的注意力机制综述
专知会员服务
75+阅读 · 2021年10月22日
最新《深度学习人体姿态估计》综述论文,26页pdf
专知会员服务
38+阅读 · 2020年12月29日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python图像处理,366页pdf,Image Operators Image Processing in Python
最新《医学图像深度语义分割》综述论文
专知会员服务
94+阅读 · 2020年6月7日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
相关资讯
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
【CNN】一文读懂卷积神经网络CNN
产业智能官
18+阅读 · 2018年1月2日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
【学习】(Python)SVM数据分类
机器学习研究会
6+阅读 · 2017年10月15日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Top
微信扫码咨询专知VIP会员