~/talk

Rex: Closing the language-verifier gap with safe and usable kernel extensions

on YouTube 19m
Talkat USENIX ATC '25 · 2025-07-07..07-09· [linux-and-operating-systems, security]

speakers

name:Jinghao Jia
links:none on file
name:Ruowen Qin
links:none on file
name:Milo Craun
links:none on file
name:Egor Lukiyanov
links:none on file
name:Ayush Bansal
links:none on file
name:Minh Phan
links:none on file
name:Michael V. Le
links:none on file
name:Hubertus Franke
links:none on file
name:Hani Jamjoom
links:none on file
name:Tianyin Xu
website:https://tianyin.github.io
name:Dan Williams
github:dcbw

resources

video:https://youtu.be/phJ-fb5lEA8
slides:none on file

summary

Rex claims to close the language‑verifier gap by running kernel extensions in safe Rust linked to a Rex kernel crate and a lightweight runtime that enforces stack safety, termination, and safe exception handling at load or runtime instead of relying on the in‑kernel verifier. Implementation targets Linux 6.15 with a rustc backend pass and kernel symbol fixups. A BMC case study shows 300 Rust lines vs 500 C, classroom assignments succeed, and performance is competitive: 5.4× over user‑space cache on 8 CPUs and slightly (<5%) faster than eBPF. no separate static verification

AI-written summary · about

chapters (7)

  1. 0:00Rex and kernel extensions
  2. 2:47Language-verifier gap problem
  3. 6:40Rex framework solution
  4. 8:05Extended tab safety in Rex
  5. 11:40Exception handling in Rex runtime
  6. 15:09Usability and performance of Rex
  7. 18:23Conclusion and future

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.