• Abstract Summary: Extended Berkeley Packet Filter (BPF) is a language and run-time system enabling non-superusers to extend Linux and Windows by downloading user code to the kernel. It relies on a static analyzer to ensure code safety in kernel context. The BPF static analyzer uses abstract interpretation with several domains, and the tnum domain is key for reasoning about bitwise uncertainty. This paper formally specifies the tnum abstract domain and its arithmetic operators, provides proofs of soundness and optimality for tnum addition and subtraction operators in the BPF analyzer, describes a novel sound tnum multiplication algorithm that is more precise and efficient than the Linux kernel's algorithm (runs 33% faster on average), and this tnum multiplication is now merged in the Linux kernel.
• Comments: There are 20 pages.
• Subjects: Programming Languages (cs.PL).
• Report Number: Rutgers Department of Computer Science Technical Report DCS-TR-755 (Extended version of the CGO-2022 paper).
• Cite As: arXiv:2105.05398 [cs.PL] (or arXiv:2105.05398v3 [cs.PL] for this version), https://doi.org/10.48550/ArXiv.2105.05398 (arXiv-issued DOI via DataCite).
• Submission History: Submitted by Santosh Nagarakatte. Version 1 was submitted on Wed, 12 May 2021 01:58:27 UTC with a size of 2,459 KB. Version 2 was submitted on Mon, 13 Dec 2021 16:05:18 UTC with a size of 3,366 KB. Version 3 was submitted on Wed, 15 Dec 2021 23:18:39 UTC with a size of 591 KB.