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.

翻译：我们提出了安全放松分离逻辑(SecRSL),这是在释放-获取过程中证明C11程序的信息流通安全的一种分离逻辑。SecRSL是第一个安全逻辑,它(1) 支持以高层次语言对程序进行微弱的模拟推理;(2) 继承了组成和当地推理的分离逻辑的优点,即关于(3) 明确安全政策的当地推理,例如依赖价值的分类。据我们所知,SecRSL也是在不言而喻的记忆模型上形成的第一个安全逻辑。因此,我们还提出了对不言而喻的弱小记忆模型的信息流通安全的初步定义,对此我们证明SecRSL是健全的。SecRSL确保程序满足一个固定时间的安全保障,同时没有不确定的行为。我们运用SecRSL执行SL来实施和核查一系列同种货币原始的功能正确性和固定时间安全性,包括一个螺旋锁模块、一种混合敏锐和多种同步通道的实施。