Automatically Reasoning About How Systems Code Uses the CPU Cache
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
CFAR extracts a compact program called a memory distillate that outputs symbolic memory accesses, built by combining symbolic execution of source paths with binary replay and debug info to capture real addresses. User-written projectors answer questions like cache-footprint scaling, per-input hit/miss profiles, and secret-dependent access leaks. Evaluation covers four TCP stacks, Hyperkernel syscalls, OpenSSL algorithms and hash tables; distillates match measured traces on tested paths (zero error) and reveal an AES constant-time violation and known RSA cache leakage.
AI-written summary · about
chapters (4)
- 0:00Introduction
- 0:15The need for abstraction
- 6:28Memory distillates defined
- 8:19CFAR evaluation and results
related talks
01h 02mMemory and Compilers
27mCachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
20mCacheIR: The Benefits of a Structured Representation for Inline Caches
24mMapping Sparse Applications to Accelerated Computing Systems
14mCollapsing Towers for Side-Channel Security
32mMore CO-RE? Taming the effects of compiler optimizations on BPF tracing
40mCompact C Type Format in the GNU Toolchain
24mTowards Understanding the Costs of Avoiding Out-of-Thin-Air Results