  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.
