Speaker
Description
XArray is a data structure used in many Linux kernel components, most notably the page cache. Its API contracts are not precisely documented, making it challenging to understand caller obligations and which invariants any changes to the implementation must maintain over the structure. Since its integration into the Linux source tree in 2019, errors in the use of the library have caused bugs such as memory leaks [1, 2], and the library code itself has suffered from bugs like race conditions and null pointer dereferences [3, 4]. Recent case studies [5, 6] suggest that applying program verification to Linux kernel source code is a promising means to make requirements structured, explicit, and machine-checkable against the implementation.
This talk presents progress verifying the core load and store APIs of the XArray library. So far, we have verified the xa_load() function and its callees, and are working on the verification of xa_store(). We will discuss how the structured specification of the original library can be used to build confidence in the Rust re-implementation that is under active development [7]. By formalizing and checking the API’s precise contracts, we can validate the parity of the Rust port’s behavior in critical kernel clients.
[1] Matthew Wilcox. “mm/huge_memory: Fix xarray node memory leak.” url: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?h=v6.19&id=69a37a8ba1b4
[2] Yang Yang. “swap_state: update shadow_nodes for anonymous page.” url: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?h=v6.19&id=5649d113ffce
[3] Matthew Wilcox. “XArray: Disallow sibling entries of nodes.” url: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?h=v6.19&id=63b1898fffcd
[4] Matthew Wilcox. XArray: Fix xas_create_range() when multi-order entry present. url: https://github.com/torvalds/linux/commit/3e3c658055c002900982513e289398a1aad4a488
[5] Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. 2024. Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler. SAS 2024.
[6] Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. 2025. Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core. OLIVIERFEST '25.
[7] Daniel Gomez, "rxarray," commit 0ae6dd57e31d, Linux kernel development tree. url:
https://git.kernel.org/pub/scm/linux/kernel/git/da.gomez/linux.git/commit/?id=0ae6dd57e31d9e436ee935288767f53e118db8c0