SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
summary
SecRSL is a separation logic that proves information-flow security for C11’s Release-Acquire fragment under an axiomatic memory model and is mechanized in Coq. It defines indistinguishability between sets of execution graphs, proves soundness by inductively constructing a partially consistent matching graph, and ensures constant-time security without undefined behaviour. Verified implementations include a spinlock, a mixed-sensitivity mutex, and synchronous channels; empirical results show secure RA implementations significantly outperform sequentially consistent baselines.
AI-written summary · about
chapters (4)
- 0:00Start
- 0:39Information Flow and C11 Concurrency Model
- 6:35What Does Information Flow Security Mean in an Axiomatic Model
- 8:33Non-Atomic Writer
related talks
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
27mConcurrent Incorrectness Separation Logic
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic