SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices)

TL;DR

SecRSL is a novel separation logic designed for verifying information-flow security in C11 concurrent programs with relaxed memory models, enabling compositional reasoning and security guarantees.

Contribution

It introduces the first security logic supporting weak-memory reasoning over an axiomatic model, with proofs of security and correctness for concurrent primitives.

Findings

SecRSL is sound for an axiomatic weak memory model.

It verifies security and correctness of concurrency primitives.

Empirical evaluations show SecRSL's effectiveness in secure concurrent programming.

Abstract

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.