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 。