VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
summary
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying copy_allocate instruction. Builds RefinedC-VIP (Coq-backed, automated) and implements VIP in Cerberus; proves a soundness theorem that VIP-defined programs avoid PNVI undefined behavior. Evaluates on 44 test programs: 12 behave identically, 13 are UB everywhere, 15 are PNVI-defined but need small edits to work under VIP, and artifacts are available via RefinedC-VIP.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:40Verifying programs with integer pointer casts
- 1:24Memory object models overview
- 3:33Main contributions
- 4:26Key idea: annotate integer-to-pointer casts with a provenance
- 10:25How can we interpret VIP programs under PNVI-ae-udi?
- 12:07Evaluation of the generated assembly code
- 13:53Validation of the soundness result using Cerberus
- 16:14Evaluating VIP for program verification
related talks
28mMemory simulations, security and optimization in a verified compiler
27mA CHERI C Memory Model for Verified Temporal Safety
29mOwnership Types for Verification of Programs with Pointer Arithmetic
28mProving Memory Access Violations in Isabelle/HOL
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
27mHaskell Library for Safer Virtual Machine Introspection (Experience Report)
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability
01h 25mIntroduction to Verifiable Computing