SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices)
This work addresses security verification for concurrent C programs under weak-memory models, which is foundational for secure systems but incremental as it builds on existing separation logic techniques.
The authors tackled the problem of proving information-flow security for C11 programs with weak-memory concurrency by developing SecRSL, a separation logic that supports compositional reasoning and expressive policies, and applied it to verify constant-time security in concurrency primitives with empirical performance evaluations.
We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic's virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification. SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour. We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL's power to support the development of secure and performant concurrent C programs.