CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
summary
Claims a verification method that proves non‑interference for concurrent programs without any timing assumptions by requiring commutativity of updates only on an abstract view of shared state. Formalized as CommCSL, proven sound in Isabelle/HOL, and implemented in the SMT‑based verifier HyperViper (built on Viper). The implementation automatically checks user‑supplied abstractions and commutativity obligations and successfully verifies a suite of challenging examples; artifacts and proofs are available.
AI-written summary · about
chapters (11)
- 0:00CommCSL introduction
- 1:25Non-interference side-channel risks
- 4:58Timing channels challenges
- 7:47Abstract commutativity solution
- 10:35CommCSL proof obligations
- 13:48Implementation in Hyper-Viper
- 14:53Evaluation summary
- 15:37Q&A: Forking assumptions
- 16:39Q&A: Composing analyses
- 18:04Q&A: Abstraction inference
- 20:11Q&A: Programmer-friendly rules
related talks
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
19mScenario-based Proofs for Concurrent Objects
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
27mC4: verified transactional objects
54mReasoning about Progress of Concurrent Objects