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

Pengbo Yan  0000-0003-0396-8343 University of MelbourneAustralia
<EMAIL_ADDRESS>and  Toby Murray  0000-0002-8271-0289 University of
MelbourneAustralia<EMAIL_ADDRESS>
(2021)

###### 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.

Information-flow Security, Separation Logic, Weak Memory Consistency,
Axiomatic Semantics

††copyright: rightsretained††journal: PACMPL††journalyear:
2021††journalvolume: 5††journalnumber: OOPSLA††article: 99††publicationmonth:
10††doi: 10.1145/3485476††submissionid: oopsla21main-p14-p††ccs: Theory of
computation Separation logic††ccs: Security and privacy Logic and verification

##  1\. Introduction

Logics for proving that concurrent programs do not leak sensitive information
have received much recent study (Murray et al., 2016; Murray et al., 2018;
Karbyshev et al., 2018; Ernst and Murray, 2019; Schoepe et al., 2020; Frumin
et al., 2021). A common thread of much recent work has been adapting ideas
from concurrent separation logic (O’Hearn, 2004) to reason about secure
information flow. Indeed, recent security logics purposefully closely resemble
traditional concurrent separation logics (Ernst and Murray, 2019; Frumin et
al., 2021). Besides providing a familiar, compositional and elegant setting in
which to carry out security proofs, such logics have also proved amenable to
automated verification via symbolic execution (Ernst and Murray, 2019).

Security separation logics have so far been confined to reasoning over
sequentially-consistent memory models. There exist a handful of information-
flow logics and type systems for weak memory consistency models (Vaughan and
Millstein, 2012; Mantel et al., 2014; Smith et al., 2019). However they lack
the local reasoning abilities, and consequent scalability, afforded by
separation logics. They also lack separation logic’s support for reasoning
about resource ownership transfer with invariants, which is crucial for
expressive reasoning. Additionally, these logics have targeted machine-level
weak memory models, and so are not readily applicable for reasoning about
programs in higher level languages.

In some sense, these limitations are not surprising. Logics for information-
flow security are almost exclusively proved sound against _operational_
semantic models. Yet formal weak memory models are often specified
_axiomatically_ , in which program behaviours are represented as mathematical
objects constrained by the axioms of the weak memory model.

To our knowledge there do not even exist prior definitions of information-flow
security for such models, without which one cannot even state the soundness
theorems for any proposed logic. Even if one had such properties, another
necessary but lacking ingredient for proving the soundness of such logics is
suitable compositional, inductive properties that state the semantic meaning
of the logic’s judgements. The shape of such properties is well understood for
traditional (non-security) separation logics (Vafeiadis and Narayan, 2013;
Doko and Vafeiadis, 2016, 2017), many of which share very similar definitions.
Yet little is known about what they should look like for security separation
logics.

In this paper, we introduce _Security Relaxed Separation Logic_ (SecRSL).
SecRSL is the first concurrent separation logic for reasoning about secure
information flow in a relaxed memory model. It targets the Release-Acquire
fragment of C11 with relaxed accesses (Section 3), and thus supports reasoning
about high-level programs for the first time. It also inherits the local
reasoning, expressiveness, and compositionality of traditional concurrent
separation logics.

SecRSL’s design (Section 4) combines ideas from two prior logics: (1) Ernst
and Murray’s Security Concurrent Separation Logic (SecCSL) (Ernst and Murray,
2019), an information-flow security analogue of traditional concurrent
separation logic for sequential consistent concurrency; and (2) Vafeiadis and
Narayan’s Relaxed Separation Logic (RSL) (Vafeiadis and Narayan, 2013). Thus
SecRSL inherits SecCSL’s support for proving expressive security policies like
those involving _value-dependent classification_ (Murray et al., 2016), in
which the sensitivity of one variable can change in response to changes in the
value held by another. It also inherits RSL’s ability to reason about
ownership transfer with invariants via C11’s Release-Acquire atomics.

To state the soundness of SecRSL (Section 5), we present what is to our
knowledge the first definitions of information-flow security for an axiomatic
weak memory model (Section 5.1). We believe it should be readily applicable to
similar memory models (Doko and Vafeiadis, 2016, 2017) with little
modification, while providing guidance on how to structure such definitions
for less similar axiomatic models. Our security definition protects against
passive attackers who can observe the contents of low (public) memory
locations, as well as attackers who can observe the program’s memory access
pattern (i.e. can see _which_ locations are being accessed by the program but
not the _values_ being written to them). Thus SecRSL also protects against
attackers who can mount cache side-channel attacks and provides a form of
_constant-time security_ (Barthe et al., 2019).

To prove SecRSL sound, we developed a novel, compositional definition of
relational validity (Section 5.3) that encodes the meaning of SecRSL
judgements. As with the top-level security properties, we believe this
definition is of independent interest beyond the confines of our specific
memory model, which we inherit from RSL (Vafeiadis and Narayan, 2013).

We demonstrate SecRSL’s power by using it to implement and verify the
functional correctness and constant-time security of a range of concurrency
primitives (Section 6). Specifically, we demonstrate SecRSL’s support for
traditional relaxed memory reasoning by showing how Vafeiadis and Narayan’s
RSL proof for a spinlock module can be replayed in SecRSL. Thus we prove it
not only functionally correct but also to satisfy SecRSL’s constant-time
security guarantee. We then extend that example to implement a _mixed-
sensitivity mutex_ for protecting access to data of varying sensitivity.
Finally, we implement and verify multiple implementations of a _synchronous
channel_ abstraction for transmitting data of varying sensitivity. We
benchmark their performance against an (unverified) sequentially-consistent
implementation. In doing so, we find that SecRSL enables significant
performance gains of up to $\sim$90% depending on platform. Thus demonstrating
SecRSL’s power to support the development of secure and performant concurrent
C programming abstractions.

All formal results in this paper have been mechanised in the Coq theorem
prover. The theories are available as supplementary material (Yan, 2021).

##  2\. Overview

##### C11 Release-Acquire atomics

$\mathit{MP}_{1}(x)\stackrel{{\scriptstyle\text{def}}}{{=}}\ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ $

$\mathbf{let}\ b=\mathbf{alloc}_{\textbf{high}}()\ \mathbf{in}\ $

$\mathbf{let}\ a=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $

$\mathbf{let}\ c=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $

$[a]_{\textbf{rlx}}:=0;$

$[b]_{\textbf{na}}:=x;$ | $\mathbf{repeat}\ [a]_{\textbf{acq}}\ \mathbf{end}{}$
---|---
$[a]_{\textbf{rel}}:=1;$ | $\mathbf{let}\ y=[b]_{\textbf{na}}\ \mathbf{in}\ $
| $[c]_{\textbf{na}}:=y$

Figure 1. A message-passing program

The program $\mathit{MP}_{1}$ in Fig. 1 is a slight adaptation of the classic
_message-passing_ program, and makes use of C11’s Release-Acquire atomics.
This program has access to some local variable $x$. It creates two threads and
uses the location $b$ to send a message containing $x$ from the left thread to
the right one, where the location $a$ is used to synchronise the two threads.
The message-passing protocol initialises $a$ to hold 0. Once $b$ holds the
message to be transferred, $a$ is updated to hold 1 to signal to the right
thread that the message (stored in $b$) is now ready to be read. The right
thread busywaits until $a$ is non-zero (the repeat command executes its body
until it returns a non-zero value). The right thread then loads the message
from $b$ before writing it to the location $c$.

In the C11 Release-Acquire fragment we consider, loads and stores to memory
locations are annotated with various modes. These affect the potential
observable reorderings that are possible under the memory model. The left
thread’s store of 1 to location $a$ carries the _release_ mode (rel), while
the right thread’s load of $a$ (inside the busyloop) carries the _acquire_
mode (acq). Together these modes guarantee that if the acquire load reads the
value $1$, then the prior store of $x$ to location $b$ must have also
completed. Hence, the subsequent load from $b$ must read the value $x$ and so
$x$ will be written to location $c$.

In SecRSL (as in RSL before it) two kinds of locations are distinguished:
_atomic_ locations and _non-atomic_ locations. Modes like acquire and release
can be used only with atomic locations; non-atomic locations must be accessed
using the non-atomic mode (na). When reasoning about the program in Fig. 1
therefore, location $a$ is treated as an atomic location while $b$ and $c$ are
considered non-atomic locations.

Figure 2. Two executions of the $\mathit{MP}_{1}(x)$ program. Edges depict
some key relations of the memory model (Section 3.2): $\mathit{sb}$ (black,
solid); $\mathit{rf}$ (dashed, green); $\mathit{mo}$ (dotted, orange). As with
much prior work, we draw the arrows for the $\mathit{rf}$ relation to depict
data flow: for read and write actions $r$ and $w$ respectively, when
$\mathit{rf}(r)=w$ we draw a (dashed, green) line from $w$ to $r$.

The axiomatic C11 memory model defines a program execution as a set of actions
related by several binary relations that impose ordering constraints on those
events. Two possible executions of this program are depicted graphically in
Fig. 2, where the nodes depict the actions and the edges depict various
relations between them. The execution on the left in this figure arises when
the loop executes only once; the one on the right executes the busyloop twice.

We formally define the Release-Acquire fragment of C11 and its memory model
that SecRSL treats in Section 3, which we inherit from RSL (Vafeiadis and
Narayan, 2013).

##### Information-flow Security

What should information-flow security mean in this fragment of C11? As with
SecCSL (Ernst and Murray, 2019), we assume the existence of a passive attacker
who can observe certain parts of memory. Specifically, when they are allocated
certain memory locations are deemed to be potentially attacker-observable.
Such locations might hold data that will be publicly output or copied onto the
network. We call these locations low and all other locations high.

Notice from the allocation statements in Fig. 1 that the atomic location $a$
and the non-atomic location $c$ are both low. Being conservative, atomic
locations should be considered attacker-observable, because interactions with
them (e.g. those with $a$ in Fig. 1) affect thread scheduling and so are
potentially observable to attackers who can measure time.

In this example, the location $c$ is also considered attacker observable. As
is standard in information-flow security, we assume the attacker knows the
program’s source code. Hence, constants that appear in the program text are
considered public. The program only writes public constants to $a$; however it
eventually writes $x$ to location $c$. Hence, the program is information-flow
secure only if $x$ is public data.

We say that a program does not leak information (and so is information flow
secure) if all executions of that program beginning from states that agree on
the values of public (i.e. non-secret) data are indistinguishable to the
attacker. Supposing the variable $x$ holds public data initially, then the
program $\mathit{MP}_{1}$ is secure if for all $x$, $x^{\prime}$, if $x$ and
$x^{\prime}$ are equal, then $\mathit{MP}_{1}(x)$ is indistinguishable from
$\mathit{MP}_{1}(x^{\prime})$.

Due to the nondeterminism inherent in axiomatic semantic models, a single
program can give rise to multiple executions: an implementation is free to
choose any one of them while remaining compliant with the semantics. Indeed
two possible behaviours of $\mathit{MP}_{1}(x)$ are depicted in Fig. 2. This
nondeterminism creates potential challenges for secure information flow.

To understand why, suppose the initial state of the example was extended with
an additional secret bit $b$ and consider an implementation of the weak memory
semantics that chooses to produce the left execution when $b=1$ and to produce
the right one otherwise. An attacker who can measure execution time would be
able to distinguish these two executions since one performs an extra action.

Thus, as with prior work (Smith et al., 2019), we make the necessary
assumption that the resolution of nondeterminism in the weak memory semantics
does not itself reveal sensitive information. Since in our semantics
nondeterminism arises from the selection of memory locations returned by the
alloc expression, as well as from the concurrency semantics, we assume that
neither the memory allocator nor the concurrency implementation (the compiler,
operating system scheduler, hardware, etc.) reveal secrets to the attacker.
Both assumptions are intuitively necessary in order to proceed with source
level reasoning about information-flow security.

Our threat model also includes attackers who can observe not only the values
written to low locations, but also the program’s memory access pattern: such
attackers can observe which locations the program is accessing even if they
cannot see the values being written to them.

Thus as well as guaranteeing that indistinguishable values are written to low
locations, SecRSL’s top-level security property also requires that for two
executions to be indistinguishable they must access the same locations in the
same way at the same time. Additionally its rules prevent programs from
branching on secrets. Thus it guarantees a form _constant-time security_
(Barthe et al., 2019).

We formally define these guarantees via SecRSL’s top-level security property
in Section 5.1.

##### The Logic

Recall we said the example $\mathit{MP}_{1}$ is secure under the assumption
that its argument is public if for all arguments $x$ and $x^{\prime}$ that are
equal, $\mathit{MP}_{1}(x)$ is indistinguishable from
$\mathit{MP}_{1}(x^{\prime})$. Thus SecRSL is a _relational_ logic (Benton,
2004) that in general relates the executions of two programs, and proves them
indistinguishable.

SecRSL judgements have the general form

$\left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).\ Q\\},\
\left[(y,y^{\prime}).\ HQ\right],$

where $P$ is the precondition, $E$ and $E^{\prime}$ are the two programs we
are proving indistinguishable, $y$ and $y^{\prime}$ are the return values of
$E$ and $E^{\prime}$, and $Q$ is the postcondition. $HP$ and $HQ$ track the
set of high locations before and after the execution.

Since SecRSL is relational, its separation logic assertions relate pairs of
states (Ernst and Murray, 2019). The judgement above means that if $E$ and
$E^{\prime}$ are run from starting states related by $P$ in which all
locations in $HP$ are unobservable to the attacker, then their executions will
be indistinguishable to the attacker and, moreover, $Q$ will relate the final
states and $HQ$ will track the final set of locations known to be unobservable
to the attacker.

The security of $\mathit{MP}_{1}$ we can thus express in SecRSL as the
judgement: $\left[\emptyset\right],\ \\{\mathsf{Low}(x,x^{\prime})\\}\
\mathit{MP}_{1}(x),\ \linebreak\mathit{MP}_{1}(x^{\prime})\
\\{\mathsf{true}\\},\ \left[\emptyset\right]$. SecRSL introduces the
relational assertion $\mathsf{Low}(e,e^{\prime})$ to assert that expressions
$e$ and $e^{\prime}$ denote identical values. We note that $HP$ and $HQ$
_under-approximate_ the set of high locations. This explains why the post-set
in this judgement is empty.

We defer an explanation of the assertion forms of SecRSL and its rules to
Section 4. However we note that it supports analogues of all of the reasoning
principles of RSL. In particular, atomic locations like $a$ in Fig. 1 carry
(relational) invariants $Q(v)$ that can be used to reason about ownership
transfer via Release-Acquire patterns. Being relational, these invariants can
express security properties as well as functional ones.

$Q(v)\stackrel{{\scriptstyle\text{def}}}{{=}}(v=0\land\mathsf{emp})\lor(v=1\land((b,b)\mapsto(x,x^{\prime})\mathrel{\star}\mathsf{Low}(x,x^{\prime})));\qquad
Q^{\prime}\stackrel{{\scriptstyle\text{def}}}{{=}}Q[1:=\mathsf{emp}]$

$[\emptyset],\\{\mathsf{Low}(x,x^{\prime})\\}$

$\mathbf{let}\ b=\mathbf{alloc}_{\textbf{high}}()\ \mathbf{in}\ $

$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(b,b)\\}$

$\mathbf{let}\ a=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $

$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(b,b)\mathrel{\star}\mathsf{Rel}(a,Q)\mathrel{\star}\mathsf{Acq}(a,Q)\\}$

$\mathbf{let}\ c=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $

$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(c,c)\mathrel{\star}\mathsf{Uninit}(b,b)\mathrel{\star}\mathsf{Rel}(a,Q)\mathrel{\star}\mathsf{Acq}(a,Q)\\}$

$[a]_{\textbf{rlx}}:=0;$

$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(c,c)\mathrel{\star}\mathsf{Uninit}(b,b)\mathrel{\star}\mathsf{Rel}(a,Q)\mathrel{\star}\mathsf{Acq}(a,Q)\mathrel{\star}\mathsf{Init}(a)\\}$

$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(b,b)\mathrel{\star}\mathsf{Rel}(a,Q)\\}$ |  $[b],\\{\mathsf{Uninit}(c,c)\mathrel{\star}\mathsf{Acq}(a,Q)\mathrel{\star}\mathsf{Init}(a)\\}$
---|---
$\qquad\qquad\qquad[b]_{\textbf{na}}:=x;$ | $\qquad\qquad\qquad\mathbf{repeat}\ [a]_{\textbf{acq}}\ \mathbf{end}{};$
$[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}(b,b)\mapsto(x,x^{\prime})\mathrel{\star}\mathsf{Rel}(a,Q)\\}$ | $[b],\\{\mathsf{Low}(x,x^{\prime})\mathrel{\star}(b,b)\mapsto(x,x^{\prime})\mathrel{\star}\mathsf{Uninit}(c,c)$
|  $\mathrel{\star}\mathsf{Acq}(a,Q^{\prime})\\}$
$\qquad\qquad\qquad[a]_{\textbf{rel}}:=1;$ | $\qquad\qquad\qquad\mathbf{let}\ y=[b]_{\textbf{na}}\ \mathbf{in}\ $
$[b],\\{\mathsf{Rel}(a,Q)\mathrel{\star}\mathsf{Init}(a)\\}$ | $[b],\\{(b,b)\mapsto(y,y)\mathrel{\star}\mathsf{Uninit}(c,c)\mathrel{\star}\mathsf{Acq}(a,Q^{\prime})\\}$
| $\qquad\qquad\qquad\qquad[c]_{\textbf{na}}:=y$
| $[b],\\{(b,b)\mapsto(y,y)\mathrel{\star}(c,c)\mapsto(y,y)$
|
$\qquad\qquad\qquad\qquad\qquad\qquad\qquad\mathrel{\star}\mathsf{Acq}(a,Q^{\prime})\\}$

$[\emptyset],\\{\mathsf{true}\\}$

Figure 3. Secure message passing in SecRSL, proving $\left[\emptyset\right],\
\\{\mathsf{Low}(x,x^{\prime})\\}\ \mathit{MP}_{1}(x),\
\mathit{MP}_{1}(x^{\prime})\ \\{\mathsf{true}\\},\ \left[\emptyset\right]$. To
reduce clutter, we write proof sketches as if they operate over a single
program. However, they should really be understood as operating over a pair of
programs, where the second program is obtained by substituting each variable
in the first program with its primed counterpart. This proof sketch uses
notational shorthands defined on page 4.

Fig. 3 depicts a proof sketch for the security of $\mathit{MP}_{1}$ in SecRSL.
We note that the invariant $Q$ used for this proof encodes that when location
$a$ holds the value 1, then location $b$ holds a public value. Hence this
example demonstrates SecRSL’s ability to support reasoning about value-
dependent classification policies, as well as the local, compositional
reasoning with ownership transfer that makes concurrent separation logics so
powerful.

##  3\. Language and Memory Model

###  3.1. Programming Language

SecRSL is defined over the Release-Acquire fragment of C11 with relaxed
accesses of RSL (Vafeiadis and Narayan, 2013). The only difference is that in
SecRSL, each memory allocation expression $\mathbf{alloc}_{F}()$ is annotated
with a security level $F\in\\{\textbf{high},\textbf{low}\\}$, which is used to
define the top-level information-flow security property established by SecRSL.
These annotations are _ghost information_ and are ignored by the language
semantics (see Section 3.2).

As with RSL (Vafeiadis and Narayan, 2013), SecRSL programs are assumed to be
in A-Normal form (Flanagan et al., 1993). Thus an atomic expression,
$e\in\mathsf{AExp}$, is either a variable $x$ or a value $v$ (a memory
location $\ell\in\mathsf{Loc}$ or a number $n\in\mathbb{N}$). Program
expressions, $E\in\mathsf{Exp}$, include atomic expressions $e$, let-bindings,
conditionals, loops, parallel composition, labelled memory allocations
$\mathbf{alloc}_{F}()$, loads $[e]_{X}$, stores $[e]_{Y}:=e^{\prime}$, and
atomic compare-and-swap (CAS) instructions.

$\displaystyle v\in\mathsf{Val}::=\ $ $\displaystyle\ell\mid n\ \ \ \ \ \ \ \
\ \text{where}\leavevmode\nobreak\ \ell\in\mathsf{Loc},n\in\mathbb{N}$
$\displaystyle e\in\mathsf{AExp}::=\ $ $\displaystyle x\mid v\ \ \ \ \ \ \ \ \
\text{where}\leavevmode\nobreak\ x\in\mathsf{Var}$ $\displaystyle
E\in\mathsf{Exp}::=\ $ $\displaystyle e\mid\mathbf{let}\ x=E\ \mathbf{in}\
E^{\prime}\mid\mathbf{if}\ e\ \mathbf{then}\ E\ \mathbf{else}\ E^{\prime}$
$\displaystyle\mid\mathbf{repeat}\ E\ \mathbf{end}\mid
E_{1}\|E_{2}\mid\mathbf{alloc}_{F}()$
$\displaystyle\mid[e]_{X}\mid[e]_{Y}:=e^{\prime}\mid\mathbf{CAS}_{Z,W}(e,e^{\prime},e^{\prime\prime})$
where $\displaystyle
X\in\\{\textbf{sc},\textbf{acq},\textbf{rlx},\textbf{na}\\},\leavevmode\nobreak\
Y\in\\{\textbf{sc},\textbf{rel},\textbf{rlx},\textbf{na}\\},$ $\displaystyle
Z\in\\{\textbf{sc},\textbf{rel\\_acq},\textbf{acq},\textbf{rel},\textbf{rlx}\\},$
$\displaystyle
W\in\\{\textbf{sc},\textbf{acq},\textbf{rlx}\\},\leavevmode\nobreak\
F\in\\{\textbf{high},\textbf{low}\\}$

As in C, in conditional expressions we treat zero as false and non-zero values
as true. The construct $\mathbf{repeat}\ E\ \mathbf{end}$ executes $E$
repeatedly until it returns a non-zero value.

In the C11 Release-Acquire memory model, memory accesses are annotated by
their mode, which affects the ordering guarantees they provide. Modes
comprise: sequentially consistent (sc), acquire (acq), release (rel), combined
release-acquire (rel_acq), relaxed (rlx), or non-atomic (na). Different kinds
of memory accesses support different modes. For instance, reads cannot be
releases, writes cannot be acquires, CASs cannot be non-atomic.

CAS is an atomic operation used heavily in lock-free concurrent algorithms. In
high-level terms, it takes a location, $\ell$, and two values, $v^{\prime}$
and $v^{\prime\prime}$, as arguments. It atomically checks if the value in the
memory location $\ell$ is $v^{\prime}$. If it is then the CAS operation is
said to succeed and it atomically stores $v^{\prime\prime}$ into memory
location $\ell$ and returns $v^{\prime}$ (the old value). Otherwise the CAS is
said to fail and it does not modify the memory and simply returns whatever
non-$v^{\prime}$ value was stored in location $\ell$. CAS expressions
$\mathbf{CAS}_{Z,W}(e,e^{\prime},e^{\prime\prime})$ are annotated with two
access modes: one $Z$ to be used for the successful case, and the other $W$
for the unsuccessful case. The expressions $e$, $e^{\prime}$ and
$e^{\prime\prime}$ respectively denote the values $\ell$, $v^{\prime}$ and
$v^{\prime\prime}$ mentioned above.

We write $[E]_{\textbf{na}}$ to abbreviate $\mathbf{let}\ x=E\ \mathbf{in}\
[x]_{\textbf{na}}$; and $E_{1};E_{2}$ for $\mathbf{let}\ x=E_{1}\ \mathbf{in}\
E_{2}$ when $x$ is not free in $E_{2}$.

###  3.2. Memory Model

Like other relaxed memory models (Manson et al., 2005; Sarkar et al., 2009;
Alglave et al., 2009; Batty et al., 2011; Mador-Haim et al., 2012; Batty et
al., 2016) the semantics that our programming language inherits from RSL
(Vafeiadis and Narayan, 2013) is defined axiomatically, in which a program’s
semantics is defined as a set of its _executions_. Each execution is
represented by a set of actions plus various binary relations on those
actions. Actions in our semantics are identical to those in RSL, except that
each allocate action $\mathrm{A}_{F}(\ell)$ carries the security label $F$ of
the allocation expression $\mathbf{alloc}_{F}()$ that generated it.

$\mathsf{Act}::=\mathrm{skip}\mid\mathrm{W}_{(\textbf{sc}\mid\textbf{rel}\mid\textbf{rlx}\mid\textbf{na})}(\ell,v)\mid\mathrm{R}_{(\textbf{sc}\mid\textbf{acq}\mid\textbf{rlx}\mid\textbf{na})}(\ell,v)$

$\mid\mathrm{RMW}_{(\textbf{sc}\mid\textbf{rel}\mid\textbf{rel\\_acq}\mid\textbf{acq}\mid\textbf{rlx})}(\ell,v,v^{\prime})\mid\mathrm{A}_{(\textbf{low}\mid\textbf{high})}(\ell)$

Actions describe a program’s interactions with memory. The $\mathrm{skip}$
action is a no-op, and represents local computation, as well as thread forks
and joins. The other actions represent respectively: writes (generated by
store expressions); reads (generated by load expressions); atomic read-modify-
write actions (generated by CAS expressions); and allocations. Actions carry
information about the memory location $\ell$ that was accessed and the values
$v,v^{\prime}$ etc. read or written.

The binary relations over actions include (Vafeiadis and Narayan, 2013) the
_sequenced-before relation_ $\mathit{sb}$, which relates actions according to
the order that they appear in the program’s textual control flow. We have
$\mathit{sb}(a,b)$ if $a$ immediately precedes $b$. The _reads-from_ relation
$\mathit{rf}$ is a map from read actions $r$ to write actions $w$: when
$\mathit{rf}(r)=w$, it means that the value read by the action $r$ was written
to the location that is being read by the action $w$. The _memory-order_
(Vafeiadis and Narayan, 2013) relation $\mathit{mo}$ (aka the _modification-
order_ (Batty, 2014) relation) and the _sequential-consistency_ order relation
$\mathit{sc}$ are total orders: the former relates write actions to the same
atomic location; the latter imposes a total order on all sc actions.

The arrows in Fig. 2 depict three of these relations: $\mathit{sb}$ (solid,
black); $\mathit{rf}$ (dashed, green); and $\mathit{mo}$ (dotted, orange).

In a program execution, each action is identified by a unique _name_ , drawn
from some countably infinite set $\mathsf{AName}$. To give meaning to these
opaque action names, the execution includes a _labelling_ function
$\mathit{lab}$ that associates each with an action $a\in\mathsf{Act}$. Then,
formally, an execution is a tuple
$\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
where $\mathcal{A}$ is a finite subset of action names from $\mathsf{AName}$,
$\mathit{lab}$ is a function from $\mathsf{AName}$ to $\mathsf{Act}$,
$\mathit{sb}$ and $\mathit{mo}$ are binary relations on elements of
$\mathcal{A}$, and $\mathit{rf}$ is a partial map between elements of
$\mathcal{A}$.

Two additional relations are defined in terms of the others. The
_synchronises-with_ relation $\mathit{sw}$: intuitively $\mathit{sw}(w,r)$
holds when $w$ is a release write and $r$ is an acquire read that synchronises
with $w$. We omit its full definition (see Vafeiadis and Narayan (2013, Figure
3)) for the sake of brevity. The _happens-before_ relation $\mathit{hb}$
formalises when one action must complete before another, and is the transitive
closure of $\mathit{sb}\cup\mathit{sw}$.

The semantics of a program $E\in\mathsf{Exp}$ is defined as usual for
axiomatic weak memory models: the possible executions of $E$ are calculated
and then constrained by the axioms of the memory model to leave only those
executions that are _consistent_ with the model. We refer to Vafeiadis and
Narayan (2013) for the axioms and write
$\mathsf{Consistent}(\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle)$
when an execution
$\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
is consistent.

Executions are calculated by applying a semantic function
$\llbracket\cdot\rrbracket$ that maps expressions $E\in\mathsf{Exp}$ to a set
$\llbracket E\rrbracket$ of their executions, each of which is a tuple
$\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{fst},\mathit{lst}\rangle$
where $\mathcal{A}$, $\mathit{lab}$ and $\mathit{sb}$ are as above,
$\mathit{res}$ is the expression’s result, and $\mathit{fst}$ and
$\mathit{lst}$ respectively denote the (action names of) the first and last
actions of the expression in the $\mathit{sb}$ order. We also refer readers to
Vafeiadis and Narayan (2013, Section 3) for the details of the semantics,
which are unchanged except that allocation expressions $\mathbf{alloc}_{F}()$
produce allocation actions $\mathrm{A}_{F}(\ell)$ that carry their security
label $F$. Note that this allocation label is otherwise ignored by the
semantics, and so does not influence program execution; it is merely
propagated to the label of allocation actions to make it visible to SecRSL’s
top-level security property (Section 5.1).

Like RSL, some rules of SecRSL are valid only in a stronger memory model that
strengthens the C11 axioms to exclude so-called “out of thin air” reads in
programs with relaxed writes. The definition of this stronger memory model is
identical to that of Vafeiadis and Narayan (2013, Section 6). We refer to it
as the _strengthened_ memory model, while noting that this strengthening is
quite standard and was used as the base for various separation logics that
succeeded RSL (Doko and Vafeiadis, 2016, 2017).

##  4\. Logic

Like many other logics for proving secure information flow (Benton, 2004;
Barthe et al., 2017; Ernst and Murray, 2019; Maillard et al., 2019), which
necessarily relate pairs of program executions, SecRSL is a _relational_ logic
(Benton, 2004). In general, SecRSL reasons about a pair of A-Normal form
programs $E$ and $E^{\prime}$ to prove that they are indistinguishable to the
attacker and thus do not leak sensitive information. (We define
indistinguishability in Section 5.1.)

For example, consider some program
$\mathit{Prog}_{1}(\mathit{hi},\mathit{lo})$ whose initial state comprises
some secret $\mathit{hi}$, as well as some public data $\mathit{lo}$. Security
requires that when run from two initial states that agree on $\mathit{lo}$ but
might differ on $\mathit{hi}$, the executions of $\mathit{Prog}_{1}$ are
indistinguishable. Therefore, to prove this hypothetical program secure, we
must prove that for all values $\mathit{lo}$, $\mathit{hi}$,
$\mathit{lo}^{\prime}$, $\mathit{hi}^{\prime}$, if $\mathit{lo}$ and
$\mathit{lo}^{\prime}$ are equal then the behaviours of
$\mathit{Prog}_{1}(\mathit{lo},\mathit{hi})$ are indistinguishable to the
attacker from the behaviours of
$\mathit{Prog}_{1}(\mathit{lo}^{\prime},\mathit{hi}^{\prime})$.

##### SecRSL Judgement

Thus the SecRSL judgement:

$\left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).\ Q\\},\
\left[(y,y^{\prime}).\ HQ\right]$

where $E$ and $E^{\prime}$ are expressions (programs). Intuitively, this
judgement means that from the attacker’s point of view, the executions of $E$
are indistinguishable from those of $E^{\prime}$. $P$ (respectively $Q$) is a
_relational_ separation logic precondition (Ernst and Murray, 2019)
(respectively postcondition, which may refer to the values $y$ and
$y^{\prime}$ returned by the expressions $E$ and $E^{\prime}$ respectively).
We introduce SecRSL’s assertion language shortly. $HP$ (respectively $HQ$)
under-approximates the set of memory locations known to be high (i.e.
unobservable to the attacker) before (respectively after) $E$ and $E^{\prime}$
execute. Like $Q$, $HQ$ can also refer to the return values $y$ and
$y^{\prime}$ of $E$ and $E^{\prime}$ respectively.111That SecRSL tracks which
locations are known to be unobservable to the attacker, rather than tracking
those that are known to be observable, might be surprising. We explain this
design choice later in Section 5.4. As with prior security logics (e.g. SecCSL
(Ernst and Murray, 2019)), the sets $HP$ and $HQ$ can depend on values read
during the program and so support value-dependent location sensitivity (Murray
et al., 2016) (i.e. locations whose classification depends on runtime values).

##### Notational Shorthands

For boolean condition $B$ and SecRSL assertion $P$, we write $P\land B$ to
abbreviate $\mathit{if}\ B\ \mathit{then}\ P\ \mathit{else}\ \mathsf{false}$.
When writing postconditions we will write $\\{(y,y).\ Q\\}$ instead of
$\\{(y,y^{\prime}).\ Q\land y=y^{\prime}\\}$, or omit the “$(y,y^{\prime}).$”
when the postcondition does not refer to the return values. To save space, we
also avoid duplicating the “$(y,y^{\prime}).$” prefix in both the
postcondition and the post-set of high locations, omitting it from the latter.
We write $\\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).\ Q\\}$, when $E$ and
$E^{\prime}$ neither modify nor depend on the high locations set, which
abbreviates $\forall HP.\ \left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\linebreak\
\\{(y,y^{\prime}).\ Q\\},\ \left[HP\right]$. We write $\left[HP\right],\
\\{P\\}\ E\ \\{(y,y^{\prime}).\ Q\\},\ \left[HQ\right]$, when talking about
two identical programs $E$, to abbreviate $\left[HP\right],\ \\{P\\}\ E,\ E\
\\{(y,y^{\prime}).\ Q\\},\ \left[HQ\right]$. We also combine these
abbreviations: $\\{P\\}\ E\ \\{(y,y^{\prime}).\ Q\\}$ means $\forall HP.\
\left[HP\right],\ \\{P\\}\ E,\ E\ \\{(y,y^{\prime}).\ Q\\},\ \left[HP\right]$.
These conventions are used both for presenting the rules of the logic and to
simplify proof sketches like that of Fig. 3.

##### SecRSL Assertions

SecRSL’s relational assertions $P,Q$ etc. are evaluated over pairs of
memories, like SecCSL’s assertions (Ernst and Murray, 2019). They include
relational (i.e. 2-state) analogues of all the RSL assertions (Vafeiadis and
Narayan, 2013) and are defined below.

$P,P_{1},P_{2}::=\mathsf{false}\mid P_{1}\Rightarrow
P_{2}\mid\forall(x,x^{\prime}),P\mid(\ell,\ell^{\prime})\mapsto(e,e^{\prime})$

$\mid\mathsf{emp}\mid P_{1}\star
P_{2}\mid\mathsf{Init}(\ell)\mid\mathsf{Uninit}(\ell,\ell^{\prime})\mid\mathsf{Low}(e,e^{\prime})$

$\
\mid\mathsf{Rel}(\ell,Q)\mid\mathsf{Acq}(\ell,Q)\mid\mathsf{RMWAcq}(\ell,Q)$

In a judgement $\left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).\
Q\\},\ \left[(y,y^{\prime}).\ HQ\right]$ we call $E$ the _left_ program and
$E^{\prime}$ the _right_ program. SecRSL assertions are therefore evaluated in
pairs of heaps (memories): the left (respectively right) memories are those
encountered during the execution of $E$ (respectively $E^{\prime}$). Thus
universal quantification quantifies over both a left and a right variable;
points-to assertions $(\ell,\ell^{\prime})\mapsto(e,e^{\prime})$ state that in
the left memory, the non-atomic location $\ell$ holds the value denoted by $e$
(and likewise for the right memory with $\ell^{\prime}$ and $e^{\prime}$).
Likewise $\mathsf{Uninit}(\ell,\ell^{\prime})$ means that the non-atomic
location $\ell$ ($\ell^{\prime}$) is uninitialised in the left (right) memory.
$\mathsf{Low}(e,e^{\prime})$ means that $e$ and $e^{\prime}$ denote equal
values, and so are indistinguishable to the attacker and, hence, can be
treated as public data that is safe to reveal to the attacker without
violating security. It is analogous to SecCSL’s _value-sensitivity_ assertion
(Ernst and Murray, 2019).

As in RSL, the assertions $\mathsf{Init}(\ell)$, $\mathsf{Rel}(\ell,Q)$,
$\mathsf{Acq}(\ell,Q)$ and $\mathsf{RMWAcq}(\ell,Q)$ refer to atomic locations
$\ell$. $\mathsf{Init}(\ell)$ means that atomic location $\ell$ has been
initialised; the others represent the permission to perform the corresponding
action on that location. $Q$ is an invariant, attached to atomic location
$\ell$, and is parameterised by the value $v$ in memory at location $\ell$.
For instance, $\mathsf{Acq}(\ell,Q)$ is the permission to perform an acquire
load on location $\ell$, obtaining the invariant $Q(v)$ where $v$ is the value
read from the location; $\mathsf{Rel}(\ell,Q)$ is the permission to perform a
release write to location $\ell$, provided that the invariant $Q(v)$ holds
where $v$ is the value being written; the $\mathsf{RMWAcq}(\ell,Q)$ permission
allows performing the CAS operation on location $\ell$.

Unlike the aforementioned assertions for non-atomic locations, those for
atomic locations do not need to mention pairs of locations
$(\ell,\ell^{\prime})$ or pairs of values $(v,v^{\prime})$. This is because
SecRSL requires that each atomic location is low and that the access patterns
of which locations are accessed are identical between the left and right
executions (Section 2). Thus atomic locations will be proved to be identical
in the left and right executions (both the location $\ell$ itself and the
value $v$ that it holds).

From these assertions the standard logical connectives $\mathsf{true}$,
$\land$, $\lor$, $\lnot$, and $\exists$ can be derived in the usual way.
Moreover, SecRSL assertions enjoy the usual semantic equivalences of
separation logic. In particular, we have that $\forall P,Q,R\in\mathsf{Assn}:$

$\displaystyle P\mathrel{\star}Q\sim$ $\displaystyle\ Q\mathrel{\star}P$
$\displaystyle P\mathrel{\star}(Q\mathrel{\star}R)\sim$ $\displaystyle\
(P\mathrel{\star}Q)\mathrel{\star}R$ $\displaystyle
P\mathrel{\star}\mathsf{emp}\sim$ $\displaystyle\ P$
$\displaystyle\mathsf{false}\mathrel{\star}\mathsf{false}\sim$ $\displaystyle\
\mathsf{false}$ $\displaystyle P\lor Q\sim$ $\displaystyle\ Q\lor P$
$\displaystyle P\lor(Q\lor R)\sim$ $\displaystyle\ (P\lor Q)\lor R$
$\displaystyle(P\lor\mathsf{false})\sim$ $\displaystyle\ (P\lor P)$
$\displaystyle(P\lor P)\sim$ $\displaystyle\ P$

These equivalences are derived from the assertion semantics, which will be
introduced in Section 5.2 (see also Section A.1).

$\begin{array}[]{c}\\{\mathsf{emp}\\}\ \mathbf{alloc}_{\textbf{low}}()\
\\{(\ell,\ell).\mathsf{Uninit}(\ell,\ell)\\}\end{array}$

$\begin{array}[]{c}\left[HF\right],\ \\{\mathsf{emp}\\}\
\mathbf{alloc}_{\textbf{high}}()\
\\{(\ell,\ell).\mathsf{Uninit}(\ell,\ell)\\},\ \left[\\{\ell\\}\cup
HF\right]\end{array}$

$\begin{array}[]{c}\left[HF\right],\ \\{P\mathrel{\star}G\\}\
[\ell]_{\textbf{na}}:=v,\ [\ell]_{\textbf{na}}:=v^{\prime}\
\\{(\ell,\ell)\mapsto(v,v^{\prime})\\},\
\left[HF\right]\end{array}\begin{array}[]{c}\mathit{if}\ \ell\not\in HF\
\mathit{then}\ G=\mathsf{Low}(v,v^{\prime})\ \mathit{else}\ G=\mathsf{emp}\\\
(P=\mathsf{Uninit}(\ell,\ell))\ \lor\
(P=(\ell,\ell)\mapsto(\\_,\\_))\end{array}$

$\begin{array}[]{c}\\{(\ell,\ell)\mapsto(v,v^{\prime})\\}\
[\ell]_{\textbf{na}},\ [\ell]_{\textbf{na}}\
\\{(y,y^{\prime}).(\ell,\ell)\mapsto(v,v^{\prime})\land y=v\land
y^{\prime}=v^{\prime}\\}\end{array}$

$\\{P\\}\ e,\ e^{\prime}\ \\{(y,y^{\prime}).P\land y=e\land
y^{\prime}=e^{\prime})\\}$

Figure 4. Non-Atomic Rules

$\\{\mathsf{emp}\\}\ \mathbf{alloc}_{\textbf{low}}()\
\\{(\ell,\ell).\mathsf{Rel}(\ell,Q)\mathrel{\star}\mathsf{Acq}(\ell,Q)\\}$

$\\{\mathsf{emp}\\}\ \mathbf{alloc}_{\textbf{low}}()\
\\{(\ell,\ell).\mathsf{Rel}(\ell,Q)\mathrel{\star}\mathsf{RMWAcq}(\ell,Q)\\}$

$\\{\mathsf{Acq}(\ell,Q)\mathrel{\star}\mathsf{Init}(\ell)\\}\
[\ell]_{\textbf{rlx}}\ \\{(v,v).\mathsf{Acq}(\ell,Q)\\}$

$\\{\mathsf{Rel}(\ell,Q)\mathrel{\star}Q(v)\\}\ [\ell]_{\textbf{rel}}:=v\
\\{\mathsf{Rel}(\ell,Q)\mathrel{\star}\mathsf{Init}(\ell)\\}$

$\\{\mathsf{Acq}(\ell,Q)\mathrel{\star}\mathsf{Init}(\ell)\\}\
[\ell]_{\textbf{acq}}\ \\{(v,v).\
Q(v)\mathrel{\star}\mathsf{Acq}(\ell,Q\left[v:=\mathsf{emp}\right])\\}\forall
v.\leavevmode\nobreak\ \mathsf{precise}(Q(v))$

$\\{\mathsf{Rel}(\ell,Q)\\}\leavevmode\nobreak\
[\ell]_{\textbf{rlx}}:=v\leavevmode\nobreak\ \\{\text{Init}(\ell)\\}Q=\lambda
x.\leavevmode\nobreak\ (\mathit{if}\ x=v\ \mathit{then}\ \mathsf{emp}\
\mathit{else}\ \texttt{false})$

$\\{\mathsf{Acq}(\ell,Q)\mathrel{\star}\mathsf{Init}(\ell)\\}\
[\ell]_{\textbf{rlx}}\ \\{(v,v).\leavevmode\nobreak\ \mathsf{Acq}(\ell,Q)\land
Q(v)\neq\mathsf{false}\\}$

$\\{P\\}\ \mathbf{CAS}_{X,Y}(\ell,v,v^{\prime})\ \\{(y,y).\leavevmode\nobreak\
R\\}\begin{array}[]{c}P\implies\mathsf{Init}(\ell)\mathrel{\star}\mathsf{RMWAcq}(\ell,Q)\mathrel{\star}\mathsf{true}\\\
P\mathrel{\star}Q(v)\implies\mathsf{Rel}(\ell,Q^{\prime})\mathrel{\star}Q^{\prime}(v^{\prime})\mathrel{\star}R[v/y]\\\
X\in\\{\textbf{rel},\textbf{rlx}\\}\implies Q(v)=\mathsf{emp}\\\
X\in\\{\textbf{acq},\textbf{rlx}\\}\implies
Q^{\prime}(v^{\prime})=\mathsf{emp}\\\ \\{P\\}\ [\ell]_{Y}\
\\{(y,y).\leavevmode\nobreak\ y\neq v\Rightarrow R\\}\end{array}$

$\left[HP\right],\ \\{P\\}\ E_{T},\ E_{T}\ \\{(y,y).Q\\},\
\left[HQ\right]\left[HP\right],\ \\{P\\}\ E_{t},\ E_{t}\ \\{(y,y).Q\\},\
\left[HQ\right]\ \ \ \ \ \ \ t\sqsubseteq T$ , where rlx⊑rel⊑sc and
rlx⊑acq⊑sc

Figure 5. Atomic Rules

##### Non-Atomic Rules

The rules for operations on non-atomic locations are shown in Fig. 4. Recall
that our threat model assumes a memory allocator that does not leak sensitive
information, i.e. the resolution of the nondeterministic choice about which
memory location the $\mathbf{alloc}()$ expression returns does not reveal
secrets. Additionally, recall from Section 2 that SecRSL does not allow
programs to branch on secrets. This ensures that all decisions about whether
to allocate or not depend only on public data. Hence, when reasoning about
memory allocation (rules A-L and A-H), the postcondition can assert that the
two locations $\ell$ and $\ell^{\prime}$ returned in the left and right
executions respectively are equal. Naturally, high allocations increase the
set of known high locations (see rule A-H).

When writing to a non-atomic location $\ell$, the rule NA-W ensures security
by requiring that if the write might be visible to the attacker ($\ell\not\in
HF$) then the values $v$ and $v^{\prime}$ being written must be
indistinguishable: $\mathsf{Low}(v,v^{\prime})$.

In addition notice that the rules for reading and writing non-atomic locations
require that the location $\ell$ being accessed is identical in both programs.
This is required to provide SecRSL’s constant-time guarantee of
indistinguishability against attackers who can observe the memory access
pattern of the program (Section 2).

The Value rule in Fig. 4 is analogous to its RSL counterpart.

$\begin{array}[]{c}\mathsf{emp}\iff\mathsf{Low}(x,x)\\\\[4.30554pt]
\mathsf{Init}(\ell)\iff\mathsf{Init}(\ell)\mathrel{\star}\mathsf{Init}(\ell)\\\\[4.30554pt]
\mathsf{Rel}(\ell,\lambda v.\leavevmode\nobreak\ Q_{1}(v)\lor
Q_{2}(v))\iff\mathsf{Rel}(\ell,Q_{1})\mathrel{\star}\mathsf{Rel}(\ell,Q_{2})\\\\[4.30554pt]
\mathsf{Acq}(\ell,\lambda v.\leavevmode\nobreak\
Q_{1}(v)\mathrel{\star}Q_{2}(v))\iff\mathsf{Acq}(\ell,Q_{1})\mathrel{\star}\mathsf{Acq}(\ell,Q_{2})\\\\[4.30554pt]
\mathsf{RMWAcq}(\ell,Q)\iff\mathsf{RMWAcq}(\ell,Q)\mathrel{\star}\mathsf{RMWAcq}(\ell,Q)\\\
\\\
\mathsf{RMWAcq}(\ell,Q)\iff\mathsf{RMWAcq}(\ell,Q)\mathrel{\star}\mathsf{Acq}(\ell,Q^{\prime})\forall
v.\leavevmode\nobreak\ (Q^{\prime}(v)=\mathsf{emp}\lor
Q(v)=Q^{\prime}(v)=\mathsf{false})\end{array}$ Figure 6. Split Rules

${\left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).Q\\},\
\left[HQ\right]}\begin{array}[]{c}(P\implies P^{\prime})\leavevmode\nobreak\
\land\leavevmode\nobreak\ HP^{\prime}\subseteq HP\\\ \leavevmode\nobreak\
\forall(y,y^{\prime}).\leavevmode\nobreak\ \leavevmode\nobreak\
(Q^{\prime}\implies Q)\leavevmode\nobreak\ \land\leavevmode\nobreak\
HQ\subseteq HQ^{\prime}\\\ \left[HP^{\prime}\right],\ \\{P^{\prime}\\}\ E,\
E^{\prime}\ \\{(y,y^{\prime}).Q^{\prime}\\},\
\left[HQ^{\prime}\right]\end{array}$

$\left[HP\right],\ \\{P\lor P^{\prime}\\}\ E,\ E^{\prime}\
\\{(y,y^{\prime}).Q\lor Q^{\prime}\\},\
\left[HQ\right]\begin{array}[]{c}\left[HP\right],\ \\{P\\}\ E,\ E^{\prime}\
\\{(y,y^{\prime}).Q\\},\ \left[HQ\right]\\\ \left[HP\right],\
\\{P^{\prime}\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).Q^{\prime}\\},\
\left[HQ\right]\\\ \end{array}$

$\left[\texttt{if}\ b\ \texttt{then}\ H1\ \texttt{else}\ H2\right],\
\\{\mathsf{Low}(b,b^{\prime})\mathrel{\star}P\\}\ E,\ E^{\prime}\
\\{(y,y^{\prime}).\leavevmode\nobreak\ Q\\},\
\left[HQ\right]\begin{array}[]{c}\left[H1\right],\ \\{b\land b^{\prime}\land
P\\}\ E_{1},\ E_{1}^{\prime}\ \\{(y,y^{\prime}).Q\\},\ \left[HQ\right]\\\
\left[H2\right],\ \\{\lnot b\land\lnot b^{\prime}\land P\\}\ E_{2},\
E_{2}^{\prime}\ \\{(y,y^{\prime}).Q\\},\ \left[HQ\right]\\\ E=\texttt{if}\ b\
\texttt{then}\ E_{1}\ \texttt{else}\ E_{2}\qquad\qquad E^{\prime}=\texttt{if}\
b^{\prime}\ \texttt{then}\ E_{1}^{\prime}\ \texttt{else}\
E_{2}^{\prime}\end{array}$

$\left[HP\right],\ \\{\exists x.P\\}\ E,\ E^{\prime}\
\\{(y,y^{\prime}).\exists x.Q\\},\ \left[HQ\right]\left[HP\right],\ \\{P\\}\
E,\ E^{\prime}\ \\{(y,y^{\prime}).Q\\},\ \left[HQ\right]$

$\left[HP\right],\ \\{P\mathrel{\star}F\\}\ E,\ E^{\prime}\
\\{(y,y^{\prime}).Q\mathrel{\star}F\\},\ \left[HQ\right]\left[HP\right],\
\\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).Q\\},\ \left[HQ\right]$

$\left[HP\right],\ \\{P_{1}\mathrel{\star}P_{2}\\}\ E_{1}\|E_{2},\
E_{1}^{\prime}\|E_{2}^{\prime}\
\\{(y,y^{\prime}).Q_{1}\mathrel{\star}Q_{2}\\},\ \left[HQ_{1}\cup
HQ_{2}\right]\begin{array}[]{c}\left[HP\right],\ \\{P_{1}\\}\ E_{1},\
E_{1}^{\prime}\ \\{(y,y^{\prime}).Q_{1}\\},\ \left[HQ_{1}\right]\\\
\left[HP\right],\ \\{P_{2}\\}\ E_{2},\ E_{2}^{\prime}\ \\{Q_{2}\\},\
\left[HQ_{2}\right]\end{array}$

$\\{P\\}\ \mathbf{repeat}\ E\ \mathbf{end},\ \mathbf{repeat}\ E^{\prime}\
\mathbf{end}\ \\{(y,y).Q\land y\neq 0\\}\begin{array}[]{c}\\{P\\}\ E,\
E^{\prime}\ \\{(y,y^{\prime}).\leavevmode\nobreak\
Q\mathrel{\star}\mathsf{Low}(y,y^{\prime})\\}\\\
Q[(0,0)/(y,y^{\prime})]\implies P\end{array}$

$\left[HP_{1}\right],\ \\{P_{1}\\}\ \mathbf{let}\ x=E_{1}\ \mathbf{in}\
E_{2},\ \mathbf{let}\ x^{\prime}=E_{1}^{\prime}\ \mathbf{in}\ E_{2}^{\prime}\
\\{(y,y^{\prime}).Q_{2}\\},\
\left[HQ_{2}\right]\begin{array}[]{c}\left[HP_{1}\right],\ \\{P_{1}\\}\
E_{1},\ E_{1}^{\prime}\ \\{(x,x^{\prime}).Q_{1}\\},\ \left[HQ_{1}\right]\\\
\forall\leavevmode\nobreak\ (x,x^{\prime}).\left[HQ_{1}\right],\ \\{Q_{1}\\}\
E_{2},\ E_{2}^{\prime}\ \\{(y,y^{\prime}).Q_{2}\\},\
\left[HQ_{2}\right]\end{array}$

Figure 7. Structural Proof Rules

##### Atomic Rules

The rules for operations on atomic memory locations are depicted in Fig. 5,
and are each analogous to their RSL counterparts. Rules for allocating atomic
locations (A-R and A-M), like their non-atomic counterparts, assert that the
chosen location is identical (and thus public) in both executions, returning
the appropriate permissions as in RSL. Notice that these rules are valid only
for low allocations, since SecRSL requires that all atomic locations are low
(Section 2). That is also the reason why each of these rules talks about two
identical programs, since SecRSL requires that all actions on low locations
are identical between the two executions. As in RSL, performing a release
write (rule Rel-W) requires the permission $\mathsf{Rel}(\ell,Q)$ as well as
evidence that the invariant $Q(v)$ holds for the value $v$ being written,
which must be public (equal in both executions), as must the location $\ell$
being written to. Similarly, performing an acquire read (rule Acq-R) requires
the appropriate permission plus evidence that the location was initialised.
Doing so obtains the invariant $Q(v)$ for the value $v$ that was read, which
is identical in both executions (because atomic locations must be low). As in
RSL this rule requires that $Q$ is precise, whose definition for SecRSL’s
relational assertions we postpone to Definition 5.6 in Section 5.2. The rules
for relaxed reads and writes also follow their RSL counterparts. As there, the
rules RLX-R*, RLX-W*, and CAS* (when
$X\notin\\{\textbf{rel\\_acq},\textbf{sc}\\}$) are only sound in the
_strengthened_ memory model (Section 3.2) of RSL and its successors (Doko and
Vafeiadis, 2016, 2017).

##### Split Rules

SecRSL assertions behave identically to their RSL counterparts. The assertions
on atomic locations behave identically as in RSL (see Fig. 6):
$\mathsf{Init}(\ell)$ and $\mathsf{RMWAcq}(\ell,Q)$ are duplicable, as is
$\mathsf{Rel}(\ell,Q)$ which can also be split along disjunctions in $Q$;
$\mathsf{Acq}(\ell,Q)$ on the other hand can be split along separating
conjunction in $Q$. $\mathsf{RMWAcq}(\ell,Q)$ can also be split to produce a
separate, but weak, $\mathsf{Acq}(\ell,Q)$ permission.

##### Structural Rules

The structural rules for SecRSL are shown in Fig. 7. It supports all the
standard rules from concurrent separation logic, like RSL before it. Notice
that the consequence rule Conseq allows one to expand the pre-set $HP$ of high
locations, or reduce the post-set $HQ$. As in SecCSL (Ernst and Murray, 2019),
the rules for conditionals and loops do not allow programs to branch on
secrets. This is a necessary condition to enforce SecRSL’s constant-time
security (Section 2).

As with RSL, the rule for parallel composition Par is not symmetric. This is
because we inherit RSL’s semantics for parallel composition in which, for
$E_{1}\|E_{2}$, the return value of $E_{2}$ is discarded. This is why the
postcondition $Q_{2}$ in the second premise of the Par rule does not refer to
the return values of $E_{2}$ and $E_{2}^{\prime}$.

##  5\. Soundness

Like all program logics, SecRSL’s soundness is proved against the programming
language semantics. Specifically, as with prior security separation logics
like SecCSL (Ernst and Murray, 2019), we define a set of top-level security
and safety properties over the programming language semantics that apply to
entire program executions. We prove that if a program is verified in SecRSL
then it enjoys these properties. We call this result SecRSL’s _adequacy
theorem_ (Theorem 5.5), in Section 5.1.

In order to prove these properties, we developed a compositional and inductive
definition of relational validity over the C11 weak memory model that encodes
the semantic meaning of SecRSL judgements $\left[HP\right],\ \\{P\\}\ E,\
E^{\prime}\ \\{(y,y^{\prime}).\ Q\\},\ \left[HQ\right]$. We call this property
_relational validity_. It holds when for every consistent execution (i.e. one
that is consistent with the axioms of the memory model) of $E$, one can
_inductively_ construct a related consistent execution of $E^{\prime}$ that
witnesses the security of both executions (by guaranteeing that they are
indistinguishable) and their safety. The rules of the logic are then proved
sound against this definition of relational validity.

Naturally, this relational validity rests on the semantics of SecRSL’s
assertions, which we present in Section 5.2. We present the definition of
semantic validity for SecRSL’s judgements in Section 5.3.

As mentioned, SecRSL’s soundness proof was mechanised in Coq, and is available
as supplementary material.

###  5.1. Adequacy

SecRSL’s adequacy theorem includes SecRSL’s top-level security guarantees of
_low safety_ and _location safety_ : the former guarantees that an attacker
who can observe the contents of low memory locations throughout a program’s
execution cannot learn sensitive information. The latter strengthens this
guarantee to also include attackers who can observe the memory-access pattern
of the program, i.e. can observe which locations are being accessed but not
the values being written to them. This latter property provides protection
against attackers who e.g. can mount cache timing channel attacks, and so
provides a form of _constant-time_ security (Barthe et al., 2019).

To our knowledge, these are the first top-level confidentiality properties
defined over an axiomatic weak memory semantics. We believe that our
properties are of independent interest and could be adapted to other axiomatic
weak memory models.

The top-level properties that SecRSL guarantees via its adequacy theorem also
include that programs are memory safe, never read from uninitialised
locations, and are free of data races. These properties SecRSL inherits from
RSL (Vafeiadis and Narayan, 2013).

##### Whole-program executions

SecRSL’s top-level properties are defined over whole-program executions. For a
program $E$, we denote this set of executions $\mathit{CC}[\\![E]\\!]$ (the
set of _complete consistent_ executions (Vafeiadis and Narayan, 2013)). As in
RSL, whole-program executions of $E$ are obtained from the consistent
executions of $E$ by adding two extra $\mathrm{skip}$ actions: one that
precedes the execution of $E$ and another that follows it.

###### Definition 5.1 (Whole-program executions).

We denote by $\mathit{CC}[\\![E]\\!]$ the set of whole-program executions of
$E$:
$\mathit{CC}[\\![E]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}\\{\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle\mid$
$\exists
a,b,\mathcal{A}_{prg},\mathit{lab}_{prg},\mathit{sb}_{prg},\mathit{fst},\mathit{lst}.$
$a\neq b\land\mathcal{A}=\\{a,b\\}\uplus\mathcal{A}_{prg}\ \land$
$\mathit{sb}=\mathit{sb}_{prg}\cup(a,\mathit{fst})\cup(\mathit{lst},b)\ \land$
$\mathit{lab}=\\{a\rightarrow\mathrm{skip},b\rightarrow\mathrm{skip}\\}\cup\mathit{lab}_{prg}\
\land$
$\langle\mathit{res},\mathcal{A}_{prg},\mathit{lab}_{prg},\mathit{sb}_{prg},\mathit{fst},\mathit{lst}\rangle\in[\\![E]\\!]\
\land$
$\mathsf{Consistent}(\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle)\\}$

##### Top-level Security Statement

A key challenge in phrasing the top-level adequacy statement over the C11
memory model, which would persist also for other axiomatic memory models, is
dealing with the nondeterminism inherent in such models. Put simply, for two
programs $E$ and $E^{\prime}$ that (due to nondeterminism) each have a set of
behaviours as their semantics, what does it mean for the behaviours of $E$ to
be indistinguishable from those of $E^{\prime}$?

Following prior work on security definitions for concurrent, nondeterministic
programs (Murray and Lowe, 2009) one way to define this is to assume that
sources of nondeterminism will be resolved in the same way in the two
programs, and so to compare only those pairs of executions that arise from
resolving the nondeterminism identically in both programs. $E$ and
$E^{\prime}$ are indistinguishable when each such pair of executions is
indistinguishable. If we take this approach for SecRSL, what assumptions would
it hard-wire into the resulting adequacy theorem?

The sources of nondeterminism in the C11 memory model of Section 3.2 that we
inherit from Vafeiadis and Narayan (2013) are the nondeterministic model of
memory allocation and the weak memory concurrency semantics. The former
abstracts away from how memory locations are allocated in the
$\mathbf{alloc}()$ expression. The latter abstracts away from the concurrency
inherent in the C11 language and, hence, the implementation choices of the
compiler that generates code for the underlying instruction set architecture
and its weak memory model, as well as the internal details of how threads are
scheduled by the operating system and hardware.

Considering only pairs of executions in which nondeterminism is resolved
identically therefore encodes into the security property the basic assumption
of Section 2 that the memory allocator never leaks sensitive information, and
nor does the implementation choices of the weak memory model.

What does it mean for nondeterminism to have been resolved identically in two
executions? To answer this question, let us rephrase what it means to prove
indistinguishability of each pair of executions of $E$ and $E^{\prime}$ in
which nondeterminism has been resolved identically. This assumption can be
stated equivalently by saying that if $E^{\prime}$ has the opportunity to make
an identical choice to $E$, then it will do so (and vice-versa). Thus it
suffices to show for each execution of $E$, there exists a corresponding
execution of $E^{\prime}$ in which it is evident that the nondeterministic
choices have been resolved identically, and then prove that these two
executions are indistinguishable.

This is precisely what SecRSL’s adequacy theorem does (as well as proving that
both executions are safe).

To do so, we must define a sufficient condition that allows us to judge when
the nondeterminism in two executions has been resolved identically. Recall
that in our semantics (Section 3.2), each execution is a set of actions
related by various binary relations. We can view each execution therefore as a
directed graph (see e.g. Fig. 2), whose nodes are the actions and whose edges
carry labels like $\mathit{sb}$, $\mathit{rf}$, etc.

We claim that nondeterminism has been resolved identically in two executions
when (1) those executions are _isomorphic_ (i.e. there is one-to-one mapping
between the nodes of the two graphs and the two graphs have the same structure
and edge relationships) and (2) if for every allocation action
$\mathrm{A}_{F}(\ell)$ in one graph, the isomorphic action of the other graph
is identical (i.e. is also $\mathrm{A}_{F}(\ell)$). Condition (1) implies
identical resolution of nondeterminism resulting from the weak memory
concurrency model, while (2) implies identical allocation decisions.

Thus SecRSL’s adequacy theorem says that for every execution of $E$, there
exists an execution of $E^{\prime}$ for which conditions (1) and (2) hold, and
that the two executions are indistinguishable.

Since our definition of indistinguishability implies condition (2), SecRSL’s
adequacy theorem is stated more succinctly by saying that for each whole-
program execution
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}\in\mathit{CC}[\\![E]\\!]$,
there exists an isomorphic whole-program execution
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}\in\mathit{CC}[\\![E^{\prime}]\\!]$
that is indistinguishable to $\textstyle\chi$.

Two executions are isomorphic when they share the same set of nodes and have
identical edge relationships, including for the derived relations
$\mathit{hb}$ and $\mathit{sw}$. In the graph analogy, the set of nodes
corresponds to the set of opaque action names $\mathcal{A}$. Hence we have:

###### Definition 5.2 (Isomorphic).

Two whole-program executions
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathit{res}^{\prime},\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
are _isomorphic_ if and only if for all $a,b\in\mathcal{A}$,
$(\mathit{hb}_{{\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}}(a,b)\iff\mathit{hb}_{{\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}}(a,b))\land(\mathit{sw}_{{\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}}(a,b)\iff\mathit{sw}_{{\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}}(a,b))$.

Execution indistinguishability is defined by the two aforementioned properties
of location safety and low safety. The former implies condition (1) above
(identical allocation decisions) and implies that the executions are
indistinguishable to an attacker who can observe which locations are being
accessed but not the contents of those locations. It does so by saying that
the labels on isomorphic actions must either match or, if not, they must both
be a non-atomic write (respectively read) to the same location.

###### Definition 5.3 (Location Safety).

Two isomorphic whole-program executions
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\linebreak\mathit{mo},\mathit{sc}\rangle$
and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathit{res}^{\prime},\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
satisfy _location safety_ if and only if
for all $a\in\mathcal{A}.\ \mathit{lab}(a)=lab^{\prime}(a)\ \lor$
$\qquad(\exists\ \ell\ v\ v^{\prime}.\
\mathit{lab}(a)=\mathrm{R}_{\textbf{na}}(\ell,v)\land\mathit{lab}^{\prime}(a)=\mathrm{R}_{\textbf{na}}(\ell,v^{\prime}))\
\lor$
$(\exists\ \ell\ v\ v^{\prime}.\
\mathit{lab}(a)=\mathrm{W}_{\textbf{na}}(\ell,v)\land\mathit{lab}^{\prime}(a)=\mathrm{W}_{\textbf{na}}(\ell,v^{\prime}))$

The second indistinguishability property _low safety_ defines
indistinguishability against an attacker who can observe low memory locations.
It says that any low location must be accessed identically (including the
operations performed on that location and the values written or read to it)
between the two executions.

###### Definition 5.4 (Low Safety).

Two isomorphic whole-program executions
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\linebreak\mathit{mo},\mathit{sc}\rangle$
and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathit{res}^{\prime},\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
satisfy _low safety_ if and only if for all locations $\ell$ for which
$(\exists a\in\mathcal{A}.\
\mathit{lab}(a)=\mathrm{A}_{\textbf{low}}(\ell)\lor\mathit{lab}^{\prime}(a)=\mathrm{A}_{\textbf{low}}(\ell))$
it is the case that
for all $b\in\mathcal{A}$ such that $\mathit{lab}(b)$ or
$\mathit{lab}^{\prime}(b)$ is an action on $\ell$, then
$\mathit{lab}(b)=\mathit{lab}^{\prime}(b)$.

With these definitions, SecRSL’s adequacy theorem can be formally stated.

###### Theorem 5.5 (Adequacy).

Let $E$ and $E^{\prime}$ be two programs such that, for some $Q$ and $HQ$, if
a SecRSL judgement $\left[\emptyset\right],\ \\{\mathsf{true}\\}\ E,\
E^{\prime}\ \\{(y,y^{\prime}).Q\\},\ \left[(y,y^{\prime}).HQ\right]$ holds,
then, for every whole-program execution
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}\in\mathit{CC}[\\![E]\\!]$
there exists some
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}\in\mathit{CC}[\\![E^{\prime}]\\!]$
such that $\textstyle\chi$ and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}$
are isomorphic, and satisfy location safety and low safety. Moreover, each
execution is memory safe, has no reads from uninitialised locations, and no
data races.

We omit the definitions of the safety properties (namely memory safety, plus
absence of uninitialised reads and data races), since they are unchanged from
RSL (Vafeiadis and Narayan, 2013, Section 7.3).

###  5.2. Semantics of Assertions and Local Relational Validity

As in RSL and its descendants (Doko and Vafeiadis, 2016, 2017), SecRSL
assertions are given a semantics over heaps (memories) $h$. Because the
axiomatic weak memory model defines executions only in terms of actions and
relations between those actions, memories do not appear in the semantics. As
with logics like RSL, we define what it means for a pair of executions
$\textstyle\chi$,
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}$
to be valid with respect to a judgement $\left[HP\right],\ \\{P\\}\ E,\
E^{\prime}\ \\{(y,y).\ Q\\},\ \left[HQ\right]$ by asserting the existence of
memories that annotate the edges of the executions, and are consistent with
the actions being performed, and satisfy the SecRSL assertions in the
judgement.

We reuse the heap model of RSL (Vafeiadis and Narayan, 2013, Section 7.1).
However, since SecRSL assertions are relational, each assertion is evaluated
over a _pair_ $(h,h^{\prime})$ of heaps (Ernst and Murray, 2019; Yang, 2007).
Thus the meaning of an assertion $P$ we denote $[\\![P]\\!]$ and define
$[\\![-]\\!]$ inductively as a function that maps an assertion to a set of
pairs $(h,h^{\prime})$ for which the assertion holds.

The full definition appears in Appendix A as Definition A.1. For instance, the
meaning of the points-to assertion $(\ell,\ell^{\prime})\mapsto(v,v^{\prime})$
for non-atomic locations is analogous to its SecCSL counterpart and holds for
a pair of heaps $(h,h^{\prime})$ when $\ell\mapsto v$ in $h$ and
$\ell^{\prime}\mapsto v^{\prime}$ in $h^{\prime}$:

$[\\![(\ell,\ell^{\prime})\mapsto(v,v^{\prime})]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}\
\\{(\\{\ell\mapsto\mathsf{NA}\left[v\right]\\},\\{\ell^{\prime}\mapsto\mathsf{NA}\left[v^{\prime}\right]\\})\\}$

The assertion $\mathsf{Low}(e,e^{\prime})$ requires that $e$ and $e^{\prime}$
are indistinguishable to the attacker and is equivalent to $\mathit{if}\
e=e^{\prime}\ \mathit{then}\ \mathsf{emp}\ \mathit{else}\ \mathsf{false}$:

$[\\![\mathsf{Low}(e,e^{\prime})]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}\
\mathit{if}\ e=e^{\prime}\ \mathit{then}\ \\{(\emptyset,\emptyset)\\}\
\mathit{else}\ \emptyset$

This assertion we include as SecRSL’s analogue of SecCSL’s _value sensitivity_
assertion $\cdot::\texttt{low}$.

From the relational assertion semantics, we lift the traditional notion of
what it means for a separation logic assertion to be _precise_ (O’Hearn, 2004;
Vafeiadis and Narayan, 2013) to SecRSL’s relational assertions.

###### Definition 5.6 (Precise).

A SecRSL assertion $P$ is _precise_ , written $\mathsf{precise}(P)$, if and
only if
For all $h_{1},h_{2}$ such that
$((h_{1},\\_)\in[\\![P]\\!]\land(h_{2},\\_)\in[\\![P]\\!])$ or
$((\\_,h_{1})\in[\\![P]\\!]\land(\\_,h_{2})\in[\\![P]\\!])$,
for all $h_{3},h_{4}$ such that $h_{1}\oplus h_{3}=h_{2}\oplus
h_{4}\neq\mathsf{undef}$, we have $h_{1}=h_{2}\land h_{3}=h_{4}$

In this definition $\oplus$ refers to the heap addition operator of RSL’s heap
model (Vafeiadis and Narayan, 2013, Figure 15).

##### Local Relational Validity

The concept of _local relational validity_ is a key building block of our
definition of semantic relational validity (i.e. the semantic meaning) of
SecRSL judgements (which we present later in Section 5.3). It is the
relational analogue of RSL’s local validity (Vafeiadis and Narayan, 2013,
Definition 4). It is defined for a pair of executions
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathit{res}^{\prime},\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
and a subset $\mathit{V}\subseteq\mathcal{A}$ of their actions whose validity
is being asserted. Given heap annotation functions $\mathit{hmap}$ and
$\mathit{hmap}^{\prime}$ that annotate the $\mathit{sb}$ and $\mathit{sw}$
edges of $\textstyle\chi$ and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}$
respectively with heaps (to witness the memory of each program at that point
during its execution), plus a high location set $H$, local relational validity
asserts that the heap annotations are consistent with the actions
$a\in\mathit{V}$ being performed at each point in those executions; plus
imposing sufficient conditions to ensure that the executions are isomorphic
and indistinguishable, and that each is safe. It also asserts that all high
allocations must appear in $H$ and all low allocations must not appear in $H$.

We relegate its definition to Definition A.2 in Appendix A. For executions
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathit{res},\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\linebreak\mathit{mo},\mathit{sc}\rangle$
and
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathit{res}^{\prime},\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$,
actions $\mathit{V}\subseteq\mathcal{A}$, heap annotation functions
$\mathit{hmap}$ and $\mathit{hmap}^{\prime}$ and location set $H$, we write
$\mathsf{Valid}({\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}},V,lab^{\prime},\mathit{hmap},\mathit{hmap}^{\prime},H)$
when local relational validity holds for the subparts of the two executions
identified by $\mathit{V}$.

Local relational validity considers just the subparts of the graphs identified
by $\mathit{V}$ in order to allow it to be inductively asserted over an ever-
increasing part of the two executions, by the inductive definition of
relational validity of SecRSL judgements. Finally, we now present that
definition.

###  5.3. Relational Validity

We now define the semantic meaning of SecRSL’s judgements $\left[HP\right],\
\\{P\\}\ E,\ E^{\prime}\ \\{(y,y^{\prime}).\ Q\\},\ \left[HQ\right]$. This
definition is a novel, compositional and inductive relational validity
property and, to our knowledge, the first such defined for an axiomatic weak
memory semantics. As with the top-level security properties, we believe its
design is of independent interest and should also be applicable to other
axiomatic weak memory models. However, unlike the top-level definitions, it
does not need to be trusted: it is an internal definition used to carry out
the soundness proof of the logic; not a statement of any guarantees provided
by the logic—instead those guarantees are provided by SecRSL’s adequacy
theorem (Theorem 5.5).

Recall that we refer to the semantic definition that encodes the meaning of
SecRSL’s judgements as _relational validity_. It is defined formally in
Appendix A as Definition A.5. Its formal definition uses various notations
introduced in Vafeiadis and Narayan (2013); however it is not necessary to
parse the mathematics in order to understand it, which we carefully explain
here.

In order to be compositional, relational validity considers executions of $E$
and $E^{\prime}$ over all possible contexts. That is it considers (what we
call) _contextual executions_ in which the actions of $E$ are embedded in
those of some larger context. As is common in definitions of validity for
separation logic judgements (Vafeiadis, 2011), relational validity also
quantifies over all possible frame assertions $R$, to be conjoined with the
precondition $P$ and postcondition $Q$, in order to derive the Frame rule. In
addition it quantifies over all possible supersets $H$ of the initial high-
location set $HP$.

Relational validity of the judgement $\left[HP\right],\ \\{P\\}\ E,\
E^{\prime}\ \\{(y,y^{\prime}).\ Q\\},\ \left[HQ\right]$ considers each
consistent contextual execution of $E$. For each it considers all potential
contexts of executions of $E^{\prime}$ in which the executions preceding $E$
and $E^{\prime}$ satisfy local relational validity wrt $H$ and the memories
directly preceding $E$ and $E^{\prime}$ satisfy $P\mathrel{\star}R$. For each
it then asserts _configuration safety_ (Definition A.4 in Appendix A).
Configuration safety inductively asserts the existence of an execution of
$E^{\prime}$ in this context whose final memories satisfy $Q\mathrel{\star}R$.
It requires that at each step of the induction the execution of $E^{\prime}$
constructed so far satisfies local relational validity wrt the same part of
the execution of $E$, under the assumption that the same is true for actions
contributed by the contexts. In this way, configuration safety guarantees that
the executions obtained when $E$ and $E^{\prime}$ finish are isomorphic,
indistinguishable, and that both are safe (i.e. free of undefined behaviour
like reads from uninitialised memory or data races, etc.)

In order to define configuration safety, we had to develop an inductive
characterisation that asserts _partial consistency_ of the execution of
$E^{\prime}$ constructed at each step of the induction. This property asserts
a subset of the memory model’s consistency axioms and can be applied
inductively to an ever growing subpart of the execution of $E^{\prime}$ as it
is being constructed. When combined together with local relational validity,
partial consistency guarantees that for whole programs $E^{\prime}$ the entire
constructed contextual execution will be consistent with the axioms of the
memory model. Partial consistency is defined in Appendix A (Definition A.3).

###  5.4. Discussion

##### Soundness Proof

With the definition of relational validity, the soundness proof of SecRSL
proceeds by proving the soundness of each of the rules against this
definition. This proof follows a similar structure to that of RSL; however is
considerably more complicated because of the additional need to construct the
witness execution of $E^{\prime}$.

The resulting Coq proof is ${\sim}21,600$ lines, as compared to the original
Coq proof for RSL which is ${\sim}15,000$ lines. The two proofs share
${\sim}6,000$ lines in common (basic libraries, C11 language definition and
memory model) that, when excluded, make the SecRSL proof about ${\sim}73\%$
larger.

##### The high location set

Readers familiar with logics for information-flow security might wonder why
SecRSL tracks the locations known to be high (unobservable to the attacker).
Most other logics instead track which locations are known to be observable to
the attacker, whether through special assertions like SecCSL’s _location
sensitivity assertions_ (Ernst and Murray, 2019) or through a static labelling
function or otherwise.

The reason is that the sets $HP$ and $HQ$ used for this purpose in SecRSL’s
judgements $\left[HP\right],\ \\{P\\}\ E,\ \linebreak E^{\prime}\ \\{(y,y).\
Q\\},\ \left[HQ\right]$ necessarily _under-approximate_ the set of high
locations. They must since the context in which $E$ (or $E^{\prime}$) executes
might have allocated additional memory locations unused by $E$. Were these
sets instead used to track low locations, they would still need to under-
approximate the true set of attacker-observable locations. However, under-
approximating the set of attacker visible locations is not sound, as it would
allow the logic to “forget” that a location was attacker-visible and so allow
it to be written with sensitive data.

##### Points-To Assertion

Notice that all points-to assertions generated by SecRSL are of the form
$(\ell,\ell)\mapsto(v,v^{\prime})$ in which the _same_ location $\ell$ is
referenced, albeit with two possibly different values $v$ and $v^{\prime}$.
This design choice is intentional and ensures SecRSL’s constant-time guarantee
(which requires that _which_ memory locations are accessed by the program and
the _order_ in which they are accessed never depends on secrets). We
purposefully chose to retain a pair of locations $(\ell,\ell)$ to emphasise
the relational nature of this assertion.

Indeed, while SecRSL’s rules support compositional reasoning about partial
programs, its adequacy theorem (Theorem 5.5) necessarily applies only to whole
programs (a fundamental limitation it shares with prior separation logics
defined for axiomatic memory models (Vafeiadis and Narayan, 2013; Doko and
Vafeiadis, 2016, 2017) that can give meaningful semantics only to whole
programs). For this reason, modifying SecRSL to attempt to weaken its
constant-time guarantee would not yield a more expressive logic.

##### Beyond SecRSL

We argue explicitly that the ideas underpinning SecRSL’s design and soundness
proof should be readily applicable to other logics that extend the RSL memory
model. Doko and Vafeiadis’ Fenced Separation Logic (FSL) (Doko and Vafeiadis,
2016) is an obvious target. Indeed an information-flow security analogue of
FSL would allow reasoning about a wider class of programs beyond the Release-
Acquire fragment of C11 considered here.

FSL’s memory model is a small extension of the strengthened memory model of
Section 3.2 to add support for fences. A security analogue of FSL would treat
fence operations as potentially attacker observable, much like accesses to
atomic locations in SecRSL (which, recall, must be low). With this insight,
SecRSL’s adequacy statement would apply with almost no modification to the FSL
semantics.

Just as RSL’s atomic location permissions (like $\mathsf{Acq}(\ell,Q)$) were
readily adapted to SecRSL’s relational setting while ensuring they behaved
identically to their original counterparts, we conjecture the same should be
true for the additional assertion modalities that FSL introduces for reasoning
about fences.

The definitions of local relational validity (Definition A.2) could be applied
to FSL by simply extending it to add a case for fence actions, while keeping
its current structure. Given the similar structure of SecRSL’s soundness proof
to that of RSL, and the close similarity of the soundness proofs for FSL and
RSL, there is strong evidence to suggest that the soundness proof for a
security analogue of FSL should follow a similar structure to that used in
this paper. We leave its development for future work.

##  6\. Applying the Logic

We demonstrate SecRSL by verifying a number of case studies in Coq.

###  6.1. Verifying a Spinlock Module

For our first demonstration of SecRSL we show that, by virtue of its
intentional similarity to RSL, SecRSL allows one to replay RSL proofs and, in
doing so, obtain stronger guarantees than those provable in RSL.

Specifically we consider the spinlock case study of Vafeiadis and Narayan
(2013), which we repeat below and modify only slightly to ensure that the
location $x$ that is allocated to create the lock is low.

$\displaystyle new\\_lock()\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \mathbf{let}\ x=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\
[x]_{\textbf{rel}}:=1;x$ $\displaystyle
spin(x)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle\
\mathbf{repeat}\ [x]_{\textbf{rlx}}\ \mathbf{end}$ $\displaystyle
lock(x)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle\
\mathbf{repeat}\ spin(x);\mathbf{CAS}_{\textbf{acq},\textbf{rlx}}(x,1,0)\
\mathbf{end}$ $\displaystyle unlock()\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ [x]_{\textbf{rel}}:=1$

This module has a SecRSL specification that is almost identical to its RSL
specification.

$\displaystyle\\{J\\}\ $ $\displaystyle new\\_lock()\
\\{(x,x).\mathit{Lock}(x,J)\\}$ $\displaystyle\\{\mathit{Lock}(x,J)\\}\ $
$\displaystyle lock(x)\ \\{J\mathrel{\star}\mathit{Lock}(x,J)\\}$
$\displaystyle\\{J\mathrel{\star}\mathit{Lock}(x,J)\\}\ $ $\displaystyle
unlock(x)\ \\{\mathit{Lock}(x,J)\\}$ $\displaystyle\mathit{Lock}(x,J)\ $
$\displaystyle\iff\mathit{Lock}(x,J)\mathrel{\star}\mathit{Lock}(x,J)$

While syntactically identical, note that these specifications once expressed
in SecRSL say that the lock module is not only correct, but also adheres to
SecRSL’s constant-time security guarantee. Thus the lock module will not leak
information.

We also observe that these specifications correspond to the rules for the lock
and unlock operations of SecCSL (Ernst and Murray, 2019). The proof of these
specifications is sketched in Fig. 10, in Section B.1.

It is no accident that this proof is almost syntactically identical to its RSL
counterpart. This arises not only because the sketch follows the notational
shorthands mentioned on page 4 and in the caption of Fig. 3, but—more
importantly—because we carefully designed SecRSL to support all of RSL’s
reasoning principles unchanged.

###  6.2. Mixed-Sensitivity Mutex

A common theme in much recent work on verified information flow security has
been _mixed-sensitivity_ (also known as _value-dependent classification_) data
structures (Lourenço and Caires, 2015; Murray et al., 2018; Sison and Murray,
2019; Ernst and Murray, 2019; Frumin et al., 2021). These are ones that can
hold data of varying sensitivity over time, where the data structure maintains
information about the sensitivity of the data it currently contains.

We demonstrate SecRSL’s ability to reason about the implementations of such
concurrent data structures for the first time, while taking account of weak
memory effects. We extend the prior spinlock module so that it protects access
to a mixed-sensitivity memory location. We refer to this resulting abstraction
as a _mixed-sensitivity mutex_.

$\mathsf{new\\_MSM}()$ creates a mixed sensitivity mutex $a$. The
$\mathsf{lock\\_MSM}(a)$ operation acquires access to the mixed-sensitivity
location and returns a boolean indicating whether it currently holds sensitive
(high) data or not. The module provides two operations,
$\mathsf{unlock\\_MSM\\_H}(a)$ and $\mathsf{unlock\\_MSM\\_L}(a)$, to
relinquish access to the mixed-sensitivity location, depending on whether the
data it now contains is high or low respectively.

$\mathsf{new\\_MSM}()\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}$ $\mathbf{let}\ b=\mathbf{alloc}_{\textbf{high}}()\ \mathbf{in}\ $ $\mathbf{let}\ a=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $ $[b]_{\textbf{na}}:=0;$ $[a]_{\textbf{rel}}:=1;$ |  $\mathsf{lock\\_MSM}(a)\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}$ $\mathbf{repeat}$ $\quad\mathbf{let}\ x=(\mathbf{repeat}\ [a]_{\textbf{rlx}}\ \mathbf{end})\ \mathbf{in}\ $ $\quad\mathbf{let}\ y=\mathbf{CAS}_{\textbf{acq},\textbf{rlx}}(a,x,0)\ \mathbf{in}\ $ $\quad\mathbf{if}\ (x==y)\ \mathbf{then}\ x\ \mathbf{else}\ 0$ $\mathbf{end}$
---|---

$\mathsf{unlock\\_MSM\\_L}(a)\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}\ \
[a]_{\textbf{rel}}:=1$ $\mathsf{unlock\\_MSM\\_H}(a)\ \
\stackrel{{\scriptstyle\text{def}}}{{=}}\ \ [a]_{\textbf{rel}}:=2$

Figure 8. The mixed-sensitivity mutex implementation.

Fig. 8 shows its implementation. The original spinlock writes 0 to location
$a$ to indicate that the lock is occupied (acquired) and 1 for unoccupied
(free). The mixed-sensitivity mutex uses 0 to indicate that the mutex is
occupied, while 1 and 2 indicate it is unoccupied and holding low (1) or high
(2) data.

Defining the predicates $\mathsf{ClassLow}(\ell)$ (respectively
$\mathsf{ClassHigh}(\ell)$) to denote when (non-atomic) location $\ell$ holds
a possibly high (respectively definitely low) value, we verify the mixed-
sensitivity mutex against the following specifications. Here the predicate
$\mathsf{LockMSM}(a)$ says that location $a$ refers to a mixed-sensitivity
mutex.

$\left[\right],\ \\{\mathsf{emp}\\}\ \mathsf{new\\_MSM}(),\
\mathsf{new\\_MSM}()\ \\{\mathsf{LockMSM}(a)\\},\ \left[b\right]$

$\mathsf{LockMSM}(a)\iff\mathsf{LockMSM}(a)\mathrel{\star}\mathsf{LockMSM}(a)$

$\left[b\right],\
\\{\mathsf{LockMSM}(a)\mathrel{\star}\mathsf{ClassLow}(b)\\}\
\mathsf{unlock\\_MSM\\_L}(a)\ \\{\mathsf{LockMSM}(a)\\},\ \left[b\right]$

$\left[b\right],\
\\{\mathsf{LockMSM}(a)\mathrel{\star}\mathsf{ClassHigh}(b)\\}\
\mathsf{unlock\\_MSM\\_H}(a)\ \\{\mathsf{LockMSM}(a)\\},\ \left[b\right]$

$\left[b\right],\ \\{\mathsf{LockMSM}(a)\\}\ \mathsf{lock\\_MSM}(a)\
\\{(y,y).\ \mathsf{LockMSM}(a)\mathrel{\star}(\mathit{if}\ y=1\ \mathit{then}\
\mathsf{ClassLow}(b)\ \mathit{else}\ \mathsf{ClassHigh}(b))\\},\
\left[b\right]$

The first says that $\mathsf{new\\_MSM}()$ creates mixed-sensitivity mutexes;
the second that $\mathsf{LockMSM}(a)$ is freely duplicable; the third requires
that when unlocking with the $\mathsf{unlock\\_MSM\\_L}(a)$ operation, that
$a$ holds a low value ($\mathsf{ClassLow}(a)$); the final specification says
that after locking, the (necessarily low) return value $y$ correctly indicates
the sensitivity of the data held in location $a$.

The proof sketch for this example appears in Section B.2.

###  6.3. Implementing Verified Synchronous Channels

Message-passing concurrency, in which concurrent threads transfer data over
_channels_ rather than (raw) shared memory, is a common programming
abstraction and has been widely studied in the context of information-flow
security (Allen, 1991; Roscoe et al., 1994; Roscoe, 1995; Honda et al., 2000;
Zdancewic and Myers, 2003; Terauchi, 2008; Murray and Lowe, 2010; Karbyshev et
al., 2018).

One of the most common message-passing abstractions is the _synchronous
channel_ , e.g. as widely studied in various process calculi like CSP, CCS,
and the synchronous $\pi$-calculus, and implemented in various programming
languages like Go and generalised by Ada’s rendezvous mechanism.

A synchronous channel allows data to be transmitted from a sending thread to a
receiving thread. Both threads block until the other is ready, which means
that this type of channel also forces the sender and receiver to synchronise
each time that data is transmitted on the channel.

####  6.3.1. Release/Acquire Synchronous Channel

We implemented in C, and verified in SecRSL in Coq, a synchronous channel
abstraction which is specifically designed to support transmitting data of
varying sensitivity. The (inline) $\mathsf{new\\_channel()}$ operation creates
a new channel; $\mathsf{send}(v,\mathit{ishigh})$ synchronously sends the
value $v$ on the channel, where $v$’s sensitivity is given by the boolean
$\mathit{ishigh}$; $\mathsf{recv}(d)$ takes a pointer argument $d$ and waits
to receive the next value from the channel, which is written to location $d$
and whose sensitivity is returned as the (boolean) return-value of
$\mathsf{recv}(\,)$.

The code for the synchronous channel appears in Fig. 9. The verified
$\mathsf{new\\_channel()}$ operation yields distinct permissions (in the form
of SecRSL predicates) to send and receive on the channel. The
$\mathsf{new\\_channel()}$ operation creates three locations: an atomic
location $a$ and two non-atomic locations $b$ and $c$. Location $c$ is used
only by the receiver. The sender begins with permission to perform a release
write to location $a$, and ownership of non-atomic location $b$. The receiver
has permission to perform an acquire read to $a$ and owns the non-atomic
location $c$.

A synchronous communication on the channel involves the sender writing to $b$
the value $v$ to be transmitted and then performing a release write to $a$ to
encode the sensitivity of $v$ (similarly to the message-passing program in
Fig. 1). In doing so, the sender transfers ownership of $b$ to the receiver.
The sender then busywaits for the receiver to return the ownership to the
sender (so that it can be used to perform subsequent sends).

The receiver does so after waiting to receive on the channel, which involves
polling $a$ via acquire reads until its value changes. At this point the
receiver has acquired ownership of $b$ to perform a release write to $a$. The
receiver reads $b$ to learn the value $v$ that was transmitted, and infers
$v$’s sensitivity from the value it read from $a$. Finally it releases the
ownership it got from the sender by performing a release write to $a$.

Thus each send/receive pair involves a two-way transfer of location $b$,
neatly illustrating SecRSL’s power for reasoning about concurrency
abstractions involving ownership transfer.

To learn when $a$’s value changes, the receiver keeps a local copy in location
$c$ of the most recent value that the receiver wrote to $a$. The sender
encodes $v$’s sensitivity ($\mathit{ishigh}$) by incrementing $a$ either by 2
(if $\mathit{ishigh}$ is true) or 1 (otherwise). The receiver releases the
location it got from the sender by incrementing $a$ by 3 from its original
value (before it was modified by the sender). Thus the sender owns $b$
whenever $a$’s value is divisible by 3; the receiver owns $b$ otherwise, in
which case its sensitivity is determined by the (nonzero) value of $(n\
\mathbf{mod}\ 3)$.

$\mathsf{new\\_channel()}\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}\ \ $ $\mathbf{let}\ b=\mathbf{alloc}_{\textbf{high}}()\ \mathbf{in}\ $ $\mathbf{let}\ c=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $ $\mathbf{let}\ a=\mathbf{alloc}_{\textbf{low}}()\ \mathbf{in}\ $ $[b]_{\textbf{na}}:=0;$ $[c]_{\textbf{na}}:=0;$ $[a]_{\textbf{rel}}:=0;$ |  $\mathsf{send}(v,\mathit{ishigh})\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}$ $\mathbf{let}\ x=[b]_{\textbf{na}}\ \mathbf{in}\ $ $[b]_{\textbf{na}}:=v;$ $[a]_{\textbf{rel}}:=x+(\mathit{ishigh}\ ?\ 2:1);$ $\mathbf{repeat}$ $\quad\mathbf{let}\ z=[a]_{\textbf{acq}}\ \mathbf{in}\ $ $\quad\quad\mathbf{if}\ z==x+3\ \mathbf{then}\ 1\ \mathbf{else}\ 0$ $\mathbf{end}$ $[b]_{\textbf{na}}:=x+3;$
---|---

$\mathsf{recv}(d)\ \ \stackrel{{\scriptstyle\text{def}}}{{=}}$

$\mathbf{let}\ t=[c]_{\textbf{na}}\ \mathbf{in}\ $
---
$\mathbf{let}\ lv\ =\ \mathbf{(repeat}$
$\qquad\qquad\qquad\mathbf{let}\ z=[a]_{\textbf{acq}}\ \mathbf{in}\ $
$\qquad\qquad\qquad\quad\mathbf{if}\ (z==t+1)||(z==t+2)\ \mathbf{then}\ z\
\mathbf{else}\ 0$
$\qquad\qquad\quad\ \mathbf{end)}\ \mathbf{in}$
$\mathbf{let}\ v=[b]_{\textbf{na}}\ \mathbf{in}\ $
$[d]_{\textbf{na}}:=v;$
$[a]_{\textbf{rel}}:=t+3;$
$[c]_{\textbf{na}}:=t+3;$
$lv-t;$

Figure 9. The synchronous channel implementation. Here “$||$” denotes boolean
“or” (disjunction).

The permission to send on the channel is encoded in the $\mathsf{Sender}(n)$
predicate, where $n$ denotes the value currently stored in location $b$, the
sender’s counter. Likewise, $\mathsf{Recver}(n)$ is the permission to receive,
where $n$ records the current value stored in $c$, the receiver’s counter.
Reusing the predicates $\mathsf{ClassLow}(\ell)$ and
$\mathsf{ClassHigh}(\ell)$ from Section 6.2 to denote when (non-atomic)
location $\ell$ holds a possibly-high (respectively definitely low) value, we
prove the following SecRSL specifications, for all $n$ such that $(n\
\mathbf{mod}\ 3)$ = 0:

$\left[\right],\ \\{\mathsf{emp}\\}\ \linebreak\mathsf{new\\_channel()},\
\mathsf{new\\_channel()}\linebreak\ \\{\ \mathsf{Sender}(0)\ \mathrel{\star}\
\mathsf{Recver}(0)\ \\},\ \left[b\right]$

$\left[b\right],\ \\{\ \mathsf{Sender}(n)\ \mathrel{\star}(\mathit{if}\
\mathit{ishigh}\ \mathit{then}\ \mathsf{emp}\ \mathit{else}\
\mathsf{Low}(v,v^{\prime}))\ \\}\ \linebreak\mathsf{send}(v,\mathit{ishigh}),\
\mathsf{send}(v^{\prime},\mathit{ishigh})\linebreak\ \\{\
\mathsf{Sender}(n+3)\ \\},\ \left[b\right]$

$\left[b,d\right],\ \\{\ \mathsf{Recver}(n)\
\mathrel{\star}(\mathsf{ClassHigh}(d))\ \\}\ \linebreak\mathsf{recv}(d),\
\mathsf{recv}(d)\linebreak\ \\{(y,y^{\prime}).\ \mathsf{Recver}(n+3)\
\mathrel{\star}(\mathit{if}\ y=1\ \mathit{then}\ \mathsf{ClassLow}(d)\
\mathit{else}\
\mathsf{ClassHigh}(d))\mathrel{\star}\ldots\linebreak\land(y=y^{\prime})\land(y=1\lor
y=2)\\},\ \left[b,d\right]$

$\mathsf{ClassLow}(\ell)\ \stackrel{{\scriptstyle\text{def}}}{{=}}\
\exists(v,v^{\prime}),(\ell,\ell)\mapsto(v,v^{\prime})\mathrel{\star}\mathsf{Low}(v,v^{\prime})$

$\mathsf{ClassHigh}(\ell)\ \stackrel{{\scriptstyle\text{def}}}{{=}}\
\exists(v,v^{\prime}),(\ell,\ell)\mapsto(v,v^{\prime})$

These say that $\mathsf{new\\_channel()}$ yields the permissions to send and
receive, initialising the locations to 0. To call
$\mathsf{send}(v,\mathit{ishigh})$, we must have the sender permission and
$v$’s classification must match $\mathit{ishigh}$. After sending, the
permission to subsequently send is returned to allow the sender to send
repeatedly. The specification for $\mathsf{recv}(\,)$ has a similar structure
and additionally requires the location $d$, where the value received will be
written, is valid. The “…” in the postcondition for $\mathsf{recv}(\,)$ elides
additional permissions that the logic tracks: namely the now-useless
permission for $\mathsf{recv}($) to read the alternative value ($n+1$ or
$n+2$) from $a$, other than the value it _did_ read and that will now never be
written to $a$ (see Section B.3). Of course one can always safely ignore the
additional permission in proofs by employing the frame rule.

The proof sketch appears in Section B.3.

####  6.3.2. Release/CAS Synchronous Channel

To showcase SecRSL’s flexibility, we also implemented and verified an
alternative synchronous channel implementation. Rather than using
release/acquire synchronisation, this implementation instead uses release/CAS
pairs. Doing so avoids the need for the counter $n$ and leads to a simpler
proof, albeit with a similar structure to the original. This implementation we
also verified in Coq, against the following specifications, where
$\mathsf{Sender}$ and $\mathsf{Recver}$ denote the permissions to send and
receive respectively:

$\left[\right],\ \\{\mathsf{emp}\\}\
\linebreak\mathsf{new\\_channel\\_CAS}(),\
\mathsf{new\\_channel\\_CAS}()\linebreak\ \\{\ \mathsf{Sender}\
\mathrel{\star}\ \mathsf{Recver}\ \\},\ \left[b\right]$

$\left[b\right],\ \\{\ \mathsf{Sender}\ \mathrel{\star}(\mathit{if}\
\mathit{ishigh}\ \mathit{then}\ \mathsf{emp}\ \mathit{else}\
\mathsf{Low}(v,v^{\prime}))\ \\}\
\linebreak\mathsf{send\\_CAS}(v,\mathit{ishigh}),\
\mathsf{send\\_CAS}(v^{\prime},\mathit{ishigh})\linebreak\ \\{\
\mathsf{Sender}\ \\},\ \left[b\right]$

$\left[b,d\right],\ \\{\ \mathsf{Recver}\
\mathrel{\star}(\mathsf{ClassHigh}(d))\ \\}\
\linebreak\mathsf{recv\\_CAS}(d),\ \mathsf{recv\\_CAS}(d)\linebreak\
\\{(y,y^{\prime}).\ \mathsf{Recver}\ \mathrel{\star}(\mathit{if}\ y=1\
\mathit{then}\ \mathsf{ClassLow}(d)\ \mathit{else}\
\mathsf{ClassHigh}(d))\linebreak\land(y=y^{\prime})\land(y=1\lor y=2)\\},\
\left[b,d\right]$

####  6.3.3. Performance Comparison

We implemented both verified channel implementations in C, and performed a
rudimentary comparison of their performance. As a baseline we implemented a
sequentially-consistent version of the synchronous channel, shown in Fig. 11
(in Appendix C). We constructed this implementation by taking the one from
Fig. 9 and marking all shared variable accesses with the sc mode, in order to
make its execution sequentially consistent (i.e. insulate it from weak memory
effects). While this implementation is not verified, we posit that it might be
verifiable using a suitable adaptation of the fine-grained security separation
logic of Frumin et al. (2021).

The results are summarised in Table 1. We report maximum and minimum average
bandwidths observed when transferring 1 GiB (1024 MiB) of random data over
four trials, across various platforms. We also report the average number of
rounds per second observed across all trials for each platform. The results
include a version of the release/acquire channel implementation that transmits
8-byte values (long ints); all other implementations transmit 4-byte values
(ints).

| Observed Bandwidth MiB/sec (avg. rounds/sec)
---|---
Implementation | Intel MacBook | Intel Server | ARM Server
Rel/Acq (4 bytes) | 31–33 ($8.3\times 10^{6}$) | 17–19 ($4.7\times 10^{6}$) | 13–19 ($4.1\times 10^{6}$)
Rel/Acq (8 bytes) | 60–65 ($8.3\times 10^{6}$) | 33–36 ($4.6\times 10^{6}$) | 23–26 ($3.2\times 10^{6}$)
Rel/CAS (4 bytes) | 15–18 ($4.2\times 10^{6}$) | 13–15 ($3.7\times 10^{6}$) | 9–12 ($2.7\times 10^{6}$)
SC (4 bytes) | 17–18 ($4.8\times 10^{6}$) | 9.2–9.6 ($2.5\times 10^{6}$) | 14–19 ($4.2\times 10^{6}$)
Table 1. Performance comparison of the verified synchronous channel
implementations. Platforms: _Intel MacBook_ : MacBook 13-inch, 2020, 2 GHz
Quad-Core Intel Core i5, MacOS. _Intel Server_ : 8 CPU Xeon(R) Gold 6248 @
2.50GHz, Linux x86_64 on VMWare hypervisor with full visualisation. _ARM
Server_ : 2 CPU Neoverse-N1, Linux ARM64 (aarch64), Amazon AWS EC2 t4g.micro
instance.

The release/acquire implementation consistently outperforms the others on both
Intel platforms, with observed throughput improvements of up to 88%. Naturally
doubling the size of the quantity transferred in each round tends to double
the observed bandwidth. On ARMv8 AArch64, acq loads and sc loads both map to
the LDAR Load-Acquire instruction; likewise rel and sc stores both map to the
STLR Store-Release instruction (Ševčík and Sewell, 2016). We conjecture that
this is why the release/acquire version was observed to perform no better on
the ARM platform than the sequentially-consistent baseline. Indeed, the latter
was observed to perform slightly better than the former; however, the results
on this platform show considerable variability and this observed difference is
well within the noise.

These empirical results demonstrate that, depending on the deployment
platform, significant performance improvements can be obtained by utilising
the C11 weak memory primitives, backed by the formal guarantees afforded by
SecRSL. They clearly demonstrate the power of SecRSL over prior logics like
SecCSL (Ernst and Murray, 2019) which can reason only about data-race free
programs, or even more recent logics (Frumin et al., 2021) that implicitly
assume sequential consistency.

##  7\. Further Related Work

Prior security logics and type systems for information-flow security on weak
memory models include that of Vaughan and Millstein (2012) who developed a
simple security type system for an operational semantics of the TSO memory
model, and Mantel et al. (2014) who developed a transforming type system for
ensuring security also on PSO and the IBM370. As security type systems,
neither supported the precision afforded by a logic like SecRSL.

Smith et al. (2019) present a program logic for proving secure information
flow of ARMv8. Unlike SecRSL which targets C11, they target a low level memory
model. Like SecRSL, their logic supports reasoning about value-dependent
classification. However, unlike SecRSL, theirs does not support local
reasoning with ownership transfer and invariants. As LABEL:fig:mp-
proof\ifExtended and LABEL:spinlock\fi demonstrates, such support is vital for
practical reasoning about expressive security policies.

Our security definitions over the C11 axiomatic memory model are an instance
of noninterference (Goguen and Meseguer, 1982) for a so-called “true
concurrency” semantics. It would be interesting to compare how our definitions
relate to those for other true concurrency models, e.g. those for Petri Nets
(Baldan and Carraro, 2014; Baldan and Beggiato, 2018).

##  8\. Conclusion

We presented SecRSL, a security separation logic for C11 Release-Acquire
concurrency. SecRSL inherits RSL’s virtues of compositional, local reasoning
about Release-Acquire atomics, plus SecCSL’s ability to reason about
expressive security policies like value-dependent classification.

We also presented the first definition of information-flow security for an
axiomatic weak memory model, against which we proved SecRSL sound. SecRSL
ensures that programs satisfy a constant-time security guarantee, while being
free of undefined behaviour.

We demonstrated SecRSL by using it to implement and verify the functional
correctness and security of various concurrency primitives, including a
spinlock module, a mixed-sensitivity mutex, and two synchronous channel
implementations. Benchmarking the latter against an unverified sequentially-
consistent implementation showed that SecRSL can enable significant
performance gains.

Beyond these examples, we also believe (as Section 5.4 argues) these ideas are
of interest—and can be readily applied—beyond the Release-Acquire fragment of
C11.

###### Acknowledgements.

We thank the anonymous reviewers for their insightful feedback on earlier
drafts of this paper. This material is based upon work supported by the
Commonwealth of Australia Defence Science and Technology Group, Next
Generation Technologies Fund (NGTF).

## References

  * (1)
  * Alglave et al. (2009) Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. 2009.  The semantics of Power and ARM multiprocessor machine code. In _Proceedings of the 4th workshop on Declarative aspects of multicore programming_. 13–24.
  * Allen (1991) PG Allen. 1991.  A comparison of non-interference and non-deducibility using CSP. In _IEEE Computer Security Foundations Workshop (CSFW)_. IEEE, 43–54.
  * Baldan and Beggiato (2018) Paolo Baldan and Alessandro Beggiato. 2018.  Multilevel transitive and intransitive non-interference, causally.  _Theoretical Computer Science_ 706 (2018), 54–82.
  * Baldan and Carraro (2014) Paolo Baldan and Alberto Carraro. 2014.  Non-interference by unfolding. In _International Conference on Applications and Theory of Petri Nets and Concurrency_. Springer, 190–209.
  * Barthe et al. (2019) Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019.  Formal verification of a constant-time preserving C compiler.  _Proceedings of the ACM on Programming Languages_ 4, POPL (2019), 1–30.
  * Barthe et al. (2017) Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017\.  Proving expected sensitivity of probabilistic programs.  _Proceedings of the ACM on Programming Languages_ 2, POPL (2017), 1–29.
  * Batty et al. (2016) Mark Batty, Alastair F Donaldson, and John Wickerson. 2016\.  Overhauling SC atomics in C11 and OpenCL. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. 634–648.
  * Batty et al. (2011) Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011.  Mathematizing C++ concurrency. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. 55–66.
  * Batty (2014) Mark John Batty. 2014\.  _The C11 and C++11 Concurrency Model_.  Ph.D. Dissertation. University of Cambridge.
  * Benton (2004) Nick Benton. 2004\.  Simple relational correctness proofs for static analyses and program transformations. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. 14–25.
  * Doko and Vafeiadis (2016) Marko Doko and Viktor Vafeiadis. 2016.  A program logic for C11 memory fences. In _International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)_. Springer, 413–430.
  * Doko and Vafeiadis (2017) Marko Doko and Viktor Vafeiadis. 2017.  Tackling real-life relaxed concurrency with FSL++. In _European Symposium on Programming (ESOP)_. Springer, 448–475.
  * Ernst and Murray (2019) Gidon Ernst and Toby Murray. 2019.  SecCSL: Security Concurrent Separation Logic. In _International Conference on Computer Aided Verification (CAV)_. 208–230.
  * Flanagan et al. (1993) Cormac Flanagan, Amr Sabry, Bruce F Duba, and Matthias Felleisen. 1993.  The essence of compiling with continuations. In _ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)_. 237–247.
  * Frumin et al. (2021) Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021\.  Compositional Non-Interference for Fine-Grained Concurrent Programs. In _IEEE Symposium on Security & Privacy (S&P)_.  To appear.
  * Goguen and Meseguer (1982) Joseph Goguen and José Meseguer. 1982.  Security Policies and Security Models. In _IEEE Symposium on Security & Privacy (S&P)_. IEEE Computer Society, Oakland, California, USA, 11–20.
  * Honda et al. (2000) Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida. 2000\.  Secure information flow as typed process behaviour. In _European Symposium on Programming (ESOP)_. Springer, 180–199.
  * Karbyshev et al. (2018) Aleksandr Karbyshev, Kasper Svendsen, Aslan Askarov, and Lars Birkedal. 2018.  Compositional Non-Interference for Concurrent Programs via Separation and Framing. In _International Conference on Principles of Security and Trust (POST)_.
  * Lourenço and Caires (2015) Luísa Lourenço and Luís Caires. 2015.  Dependent Information Flow Types. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. Mumbai, India, 317–328.
  * Mador-Haim et al. (2012) Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo MK Martin, Peter Sewell, and Derek Williams. 2012\.  An axiomatic memory model for POWER multiprocessors. In _International Conference on Computer Aided Verification (CAV)_. 495–512.
  * Maillard et al. (2019) Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder. 2019\.  The next 700 relational program logics.  _Proceedings of the ACM on Programming Languages_ 4, POPL (2019), 1–33.
  * Manson et al. (2005) Jeremy Manson, William Pugh, and Sarita V Adve. 2005\.  The Java memory model. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. 378–391.
  * Mantel et al. (2014) Heiko Mantel, Matthias Perner, and Jens Sauer. 2014\.  Noninterference under weak memory models. In _IEEE Computer Security Foundations Symposium (CSF)_. IEEE, 80–94.
  * Murray and Lowe (2009) Toby Murray and Gavin Lowe. 2009.  On Refinement-Closed Security Properties and Nondeterministic Compositions. In _International Workshop on Automated Verification of Critical Systems_ _(Electronic Notes in Theoretical Computer Science, Vol. 250)_. 49–68.  https://doi.org/10.1016/j.entcs.2009.08.017
  * Murray and Lowe (2010) Toby Murray and Gavin Lowe. 2010.  Analysing the Information Flow Properties of Object-Capability Patterns. In _Formal Aspects of Security and Trust_ _(Lecture Notes in Computer Science, Vol. 5983)_. Eindhoven, The Netherlands, 81–95.  https://doi.org/10.1007/978-3-642-12459-4_7
  * Murray et al. (2018) Toby Murray, Robert Sison, and Kai Engelhardt. 2018\.  COVERN: A Logic for Compositional Verification of Information Flow Control. In _IEEE European Symposium on Security and Privacy (EuroS &P)_. London, United Kingdom.
  * Murray et al. (2016) Toby Murray, Robert Sison, Edward Pierzchalski, and Christine Rizkallah. 2016.  Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In _IEEE Computer Security Foundations Symposium (CSF)_. 417–431.
  * O’Hearn (2004) Peter W O’Hearn. 2004\.  Resources, concurrency and local reasoning. In _International Conference on Concurrency Theory (CONCUR)_. Springer, 49–67.
  * Roscoe et al. (1994) AW Roscoe, JCP Woodcock, and Lars Wulf. 1994.  Non-interference through determinism. In _European Symposium on Research in Computer Security (ESORICS)_. Springer, 31–53.
  * Roscoe (1995) A William Roscoe. 1995\.  CSP and determinism in security modelling. In _IEEE Symposium on Security & Privacy (S&P)_. IEEE, 114–127.
  * Sarkar et al. (2009) Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O Myreen, and Jade Alglave. 2009\.  The semantics of x86-CC multiprocessor machine code. In _ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_.
  * Schoepe et al. (2020) Daniel Schoepe, Toby Murray, and Andrei Sabelfeld. 2020\.  VERONICA: Expressive and Precise Concurrent Information Flow Security. In _IEEE Computer Security Foundations Symposium (CSF)_. IEEE, 79–94.
  * Sison and Murray (2019) Robert Sison and Toby Murray. 2019.  Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In _International Conference on Interactive Theorem Proving (ITP)_. 27:1–27:19.
  * Smith et al. (2019) Graeme Smith, Nicholas Coughlin, and Toby Murray. 2019\.  Value-Dependent Information-Flow Security on Weak Memory Models. In _International Symposium on Formal Methods (FM)_. Springer, 539–555.
  * Terauchi (2008) Tachio Terauchi. 2008\.  A type system for observational determinism. In _IEEE Computer Security Foundations Symposium (CSF)_. IEEE, 287–300.
  * Vafeiadis (2011) Viktor Vafeiadis. 2011\.  Concurrent Separation Logic and Operational Semantics. In _Mathematical Foundations of Programming Semantics (MFPS)_. 335–351.
  * Vafeiadis and Narayan (2013) Viktor Vafeiadis and Chinmay Narayan. 2013.  Relaxed separation logic: A program logic for C11 concurrency. In _Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)_. 867–884.
  * Vaughan and Millstein (2012) Jeffrey A Vaughan and Todd Millstein. 2012.  Secure information flow for concurrent programs under Total Store Order. In _IEEE Computer Security Foundations Symposium (CSF)_. IEEE, 19–29.
  * Ševčík and Sewell (2016) Jaroslav Ševčík and Peter Sewell. 2016.  C/C++11 mappings to processors.  https://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html. Accessed 2021-08-12.
  * Yan (2021) Pengbo Yan. 2021\.  _SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency - Coq Formalisation_.  https://doi.org/10.5281/zenodo.5493554
  * Yang (2007) Hongseok Yang. 2007\.  Relational separation logic.  _Theoretical Computer Science_ 375, 1-3 (2007), 308–334.
  * Zdancewic and Myers (2003) Steve Zdancewic and Andrew C Myers. 2003.  Observational determinism for concurrent program security. In _IEEE Computer Security Foundations Workshop (CSFW)_. IEEE, 29–43.

##  Appendix A Formal Definitions

###  A.1. Assertion Semantics

###### Definition A.1 (Assertion Semantics).

Let [[-]] be a function from assertions to sets of pairs of heaps
$(h,h^{\prime})$ defined as follows.

$\displaystyle[\\![\mathsf{false}]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \emptyset$
$\displaystyle[\\![\mathsf{emp}]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(\emptyset,\emptyset)\\}$ $\displaystyle[\\![P\Rightarrow
Q]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle\
\\{(h,h^{\prime})\mid(h,h^{\prime})\in[\\![P]\\!]\implies(h,h^{\prime})\in[\\![Q]\\!]\\}$
$\displaystyle[\\![\mathsf{Low}(e,e^{\prime})]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \mathit{if}\ e=e^{\prime}\ \mathit{then}\
\\{(\emptyset,\emptyset)\\}\ \mathit{else}\ \emptyset$
$\displaystyle[\\![\forall(x,x^{\prime}),P]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\
\\{(h,h^{\prime})\mid\forall(v,v^{\prime}).\leavevmode\nobreak\
(h,h^{\prime})\in[\\![P\left[(v,v^{\prime})/(x,x^{\prime})\right]]\\!]\\}$
$\displaystyle[\\![P\star Q]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(h1\oplus h2,h1^{\prime}\oplus
h2^{\prime})\mid(h1,h1^{\prime})\in[\\![P]\\!]\land(h2,h2^{\prime})\in[\\![Q]\\!]\\}$
$\displaystyle[\\![\mathsf{Uninit}(\ell,\ell^{\prime})]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\
\\{(\\{\ell\mapsto\mathsf{NA}\left[\mathbb{U}\right]\\},\\{\ell^{\prime}\mapsto\mathsf{NA}\left[\mathbb{U}\right]\\})\\}$
$\displaystyle[\\![(\ell,\ell^{\prime})\mapsto(v,v^{\prime})]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\
\\{(\\{\ell\mapsto\mathsf{NA}\left[v\right]\\},\\{\ell^{\prime}\mapsto\mathsf{NA}\left[v^{\prime}\right]\\})\\}$
$\displaystyle[\\![\mathsf{Init}(\ell)]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(h,h)\mid
h=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},\mathsf{Emp},\texttt{false},\texttt{true}\right]\\}\\}$
$\displaystyle[\\![\mathsf{Rel}(\ell,Q)]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(h,h)\mid
h=\\{\ell\mapsto\mathsf{Atom}\left[Q,\mathsf{Emp},\texttt{false},\texttt{false}\right]\\}\\}$
$\displaystyle[\\![\mathsf{Acq}(\ell,Q)]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(h,h)\mid
h=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},Q,\texttt{false},\texttt{false}\right]\\}\\}$
$\displaystyle[\\![\mathsf{RMWAcq}(\ell,Q)]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\ \\{(h,h)\mid
h=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},Q,\texttt{true},\texttt{false}\right]\\}\\}$
$\displaystyle\text{where}\
\mathsf{False}\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle(\lambda
v.\leavevmode\nobreak\ \texttt{false})\ and\
\mathsf{Emp}\stackrel{{\scriptstyle\text{def}}}{{=}}(\lambda
v.\leavevmode\nobreak\ \mathsf{emp}).$

###  A.2. Local Relational Validity

The definitions of local relational validity makes use of the following
auxiliary functions.

Given an execution
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$
and a action $a\in\mathcal{A}$, we define:

$\mathsf{SBin}_{\chi}(a)\stackrel{{\scriptstyle\text{def}}}{{=}}\\{(``sb",b,a)\mid\mathit{sb}(b,a)\\}$

$\mathsf{SBout}_{\chi}(a)\stackrel{{\scriptstyle\text{def}}}{{=}}\\{(``sb",a,b)\mid\mathit{sb}(a,b)\\}$

$\mathsf{SWin}_{\chi}(a)\stackrel{{\scriptstyle\text{def}}}{{=}}\\{(``sw",b,a)\mid\mathit{rf}(b,a)\land\mathsf{isAcq}(\mathit{lab}(a))\land\mathsf{isRel}(\mathit{lab}(b))\\}$

$\mathsf{SWout}_{\chi}(a)\stackrel{{\scriptstyle\text{def}}}{{=}}\\{(``sw",a,b)\mid\mathit{rf}(a,b)\land\mathsf{isAcq}(\mathit{lab}(b))\land\mathsf{isRel}(\mathit{lab}(a))\\}$

$\mathsf{Pre}_{\chi}(\mathit{V})\stackrel{{\scriptstyle\text{def}}}{{=}}\\{a\mid\exists
b\in\mathit{V}.\mathit{sb}(a,b)\lor(\mathit{rf}(a,b)\land\mathsf{isAcq}(\mathit{lab}(b))\land\mathsf{isRel}(\mathit{lab}(a)))\lor$

$\quad\quad(\mathit{rf}(a,b)\land(\mathsf{isNA}(\mathit{lab}(b))\lor\mathsf{isNA}(\mathit{lab}(a))))\\}$

$\mathsf{Resp}_{\chi}(\mathit{V})\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{a\in\mathit{V}}(\mathsf{SBout}_{\chi}(a)\cup\mathsf{SWin}_{\chi}(a))$

###### Definition A.2 (Local Relational Validity).

Given an execution
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}=\langle\mathcal{A},\mathit{lab},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$,
a set of actions $V\subseteq\mathcal{A}$, another label function
$\mathit{lab}^{\prime}$, two heap maps
$(\mathit{hmap}:\mathsf{Resp}_{\chi}(V)\rightarrow\mathsf{Heap}_{\mathsf{spec}})$
and
$(\mathit{hmap}^{\prime}:\mathsf{Resp}_{\chi^{\prime}}(\mathit{V})\rightarrow\mathsf{Heap}_{\mathsf{spec}})$,
and a locations set $\mathit{H}$, and letting
${\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}}^{\prime}=\langle\mathcal{A},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo},\mathit{sc}\rangle$,
we define _local relational validity_ as follows and denote it
$\mathsf{Valid}({\mathchoice{\raisebox{0.0pt}{$\displaystyle\chi$}}{\raisebox{0.0pt}{$\textstyle\chi$}}{\raisebox{0.0pt}{$\scriptstyle\chi$}}{\raisebox{0.0pt}{$\scriptscriptstyle\chi$}}},\mathit{V},\mathit{lab}^{\prime},\mathit{hmap},\mathit{hmap}^{\prime},\mathit{H})$.
It holds if and only if

For all a $\in\mathit{V}$, exists
$\ell,b,v,v^{\prime},v_{1},v_{2},Q,Q^{\prime},Z,h_{F},h_{F}^{\prime},h_{1},h_{1}^{\prime},h_{sink},h_{sink}^{\prime},$
such that
$\left(\begin{array}[]{l}\mathit{lab}(a)=\mathrm{skip}\leavevmode\nobreak\
\land\leavevmode\nobreak\ \mathit{lab}^{\prime}(a)=\mathrm{skip}\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))=\mathit{hmap}(\mathsf{SBout}_{\chi}(a))\oplus
h_{sink}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))\oplus
h^{\prime}_{sink}\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathrm{A}_{F}(\ell)\leavevmode\nobreak\
\land\leavevmode\nobreak\
\mathit{lab}^{\prime}(a)=\mathrm{A}_{F}(\ell)\leavevmode\nobreak\
\land\leavevmode\nobreak\ (F=\textbf{high}\iff\ell\in\mathit{H})\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBout}_{\chi}(a))=\mathit{hmap}(\mathsf{SBin}_{\chi}(a))\oplus\\{\ell\mapsto\mathsf{Atom}\left[Q,Q,b,\texttt{false}\right]\\}\\\
\land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))\oplus\\{\ell\mapsto\mathsf{Atom}\left[Q,Q,b,\texttt{false}\right]\\}\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathrm{A}_{F}(\ell)\leavevmode\nobreak\
\land\leavevmode\nobreak\
\mathit{lab}^{\prime}(a)=\mathrm{A}_{F}(\ell)\leavevmode\nobreak\
\land\leavevmode\nobreak\ (F=\textbf{high}\iff\ell\in\mathit{H})\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBout}_{\chi}(a))=\mathit{hmap}(\mathsf{SBin}_{\chi}(a))\oplus\\{\ell\mapsto\mathsf{NA}\left[\mathbb{U}\right]\\}\\\
\land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))\oplus\\{\ell\mapsto\mathsf{NA}\left[\mathbb{U}\right]\\}\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathrm{W}_{\textbf{na}}(\ell,v)\leavevmode\nobreak\
\land\leavevmode\nobreak\
\mathit{lab}^{\prime}(a)=\mathrm{W}_{\textbf{na}}(\ell,v^{\prime})\leavevmode\nobreak\
\land\leavevmode\nobreak\ (v\neq v^{\prime}\implies\ell\in\mathit{H})\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))(\ell)\in\\{\mathsf{NA}\left[\mathbb{U}\right],\leavevmode\nobreak\
\mathsf{NA}\left[\\_\right]\\}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))(\ell)\in\\{\mathsf{NA}\left[\mathbb{U}\right],\mathsf{NA}\left[\\_\right]\\}\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBout}_{\chi}(a))=\mathit{hmap}(\mathsf{SBin}_{\chi}(a))[\ell\mapsto\mathsf{NA}\left[v\right]]\\\
\land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))[\ell\mapsto\mathsf{NA}\left[v^{\prime}\right]]\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathrm{R}_{\textbf{na}}(\ell,v)\leavevmode\nobreak\
\land\leavevmode\nobreak\
\mathit{lab}^{\prime}(a)=\mathrm{R}_{\textbf{na}}(\ell,v^{\prime})\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))(\ell)=\mathsf{NA}\left[\\_\right]\land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))(\ell)=\mathsf{NA}\left[\\_\right]\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))=\mathit{hmap}(\mathsf{SBout}_{\chi}(a))\land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathit{lab}^{\prime}(a)=\mathrm{R}_{Z}(\ell,v)\leavevmode\nobreak\
\land\leavevmode\nobreak\ Z\in\\{\textbf{rlx},\textbf{acq},\textbf{sc}\\}\\\
\land\leavevmode\nobreak\
(\mathit{hmap}(\mathsf{SWin}_{\chi}(a)),\mathit{hmap}^{\prime}(\mathsf{SWin}_{\chi^{\prime}}(a)))\in[\\![Q(v)]\\!]\land\mathsf{precise}(Q(v))\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},Q,\texttt{false},\texttt{true}\right]\\}\oplus
h_{F}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},Q,\texttt{false},\texttt{true}\right]\\}\oplus
h^{\prime}_{F}\\\ \land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBout}_{\chi}(a))=\mathit{hmap}(\mathsf{SWin}_{\chi}(a))\oplus
h_{F}\oplus h_{1}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))=\mathit{hmap}^{\prime}(\mathsf{SWin}_{\chi^{\prime}}(a))\oplus
h_{F}^{\prime}\oplus h_{1}\\\ \land\leavevmode\nobreak\
h_{1}=\\{\ell\mapsto\mathsf{Atom}\left[\mathsf{False},Q[v:=\mathsf{emp}],\texttt{false},\texttt{true}\right]\\}\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathit{lab}^{\prime}(a)=\mathrm{W}_{Z}(\ell,v)\leavevmode\nobreak\
\land\leavevmode\nobreak\ Z\in\\{\textbf{rlx},\textbf{rel},\textbf{sc}\\}\\\
\land\leavevmode\nobreak\ h_{1}=\mathit{hmap}(\mathsf{SWout}_{\chi}(a))\oplus
h_{sink}\leavevmode\nobreak\ \land\leavevmode\nobreak\
h^{\prime}_{1}=\mathit{hmap}^{\prime}(\mathsf{SWout}_{\chi^{\prime}}(a))\oplus
h^{\prime}_{sink}\\\ \land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q,\mathsf{Emp},\texttt{false},b\right]\\}\oplus
h_{1}\oplus h_{F}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q,\mathsf{Emp},\texttt{false},b\right]\\}\oplus
h^{\prime}_{1}\oplus h^{\prime}_{F}\\\ \land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBout}_{\chi}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q,\mathsf{Emp},\texttt{false},\texttt{true}\right]\\}\oplus
h_{F}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q,\mathsf{Emp},\texttt{false},\texttt{true}\right]\\}\oplus
h^{\prime}_{F}\\\ \land\leavevmode\nobreak\
(h_{1},h^{\prime}_{1})\in[\\![Q(v)]\\!]\leavevmode\nobreak\
\land\leavevmode\nobreak\ (Z\leavevmode\nobreak\ =\leavevmode\nobreak\
\textbf{rlx}\implies Q(v)=\mathsf{emp})\end{array}\right)$

$\lor\left(\begin{array}[]{l}\mathit{lab}(a)=\mathit{lab}^{\prime}(a)=\mathrm{RMW}_{Z}(\ell,v_{1},v_{2})\leavevmode\nobreak\
\land\leavevmode\nobreak\ Z\neq\textbf{na}\\\ \land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))(\ell)=\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))(\ell)=\mathsf{Atom}\left[\\_,Q,\texttt{true},\texttt{true}\right]\\\
\land\leavevmode\nobreak\
\mathit{hmap}(\mathsf{SBin}_{\chi}(a))\oplus\mathit{hmap}(\mathsf{SWin}_{\chi}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q^{\prime},\mathsf{Emp},\texttt{false},\texttt{false}\right]\\}\\\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\
\oplus\mathit{hmap}(\mathsf{SBout}_{\chi}(a))\oplus\mathit{hmap}(\mathsf{SWout}_{\chi}(a))\oplus
h_{sink}\\\ \land\leavevmode\nobreak\
\mathit{hmap}^{\prime}(\mathsf{SBin}_{\chi^{\prime}}(a))\oplus\mathit{hmap}^{\prime}(\mathsf{SWin}_{\chi^{\prime}}(a))=\\{\ell\mapsto\mathsf{Atom}\left[Q^{\prime},\mathsf{Emp},\texttt{false},\texttt{false}\right]\\}\\\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\
\oplus\mathit{hmap}^{\prime}(\mathsf{SBout}_{\chi^{\prime}}(a))\oplus\mathit{hmap}^{\prime}(\mathsf{SWout}_{\chi^{\prime}}(a))\oplus
h^{\prime}_{sink}\\\ \land\leavevmode\nobreak\
(\mathit{hmap}(\mathsf{SWin}_{\chi}(a)),\mathit{hmap}^{\prime}(\mathsf{SWin}_{\chi^{\prime}}(a)))\in[\\![Q(v)]\\!]\\\
\land\leavevmode\nobreak\ (\mathit{hmap}(\mathsf{SWout}_{\chi}(a))\oplus
h_{sink},\mathit{hmap}^{\prime}(\mathsf{SWout}_{\chi^{\prime}}(a))\oplus
h^{\prime}_{sink})\in[\\![Q^{\prime}(v^{\prime})]\\!]\\\
\land\leavevmode\nobreak\ (Z\in\\{\textbf{rlx},\textbf{rel}\\}\implies
Q(v)=\mathsf{emp})\leavevmode\nobreak\ \land\leavevmode\nobreak\
(Z\in\\{\textbf{rlx},\textbf{acq}\\}\implies
Q^{\prime}(v^{\prime})=\mathsf{emp})\end{array}\right)$

where “_” denotes a wildcard here and in the following pages.

###  A.3. Partial Consistency

The definition of partial consistency refers to various axioms of the memory
model, introduced in Vafeiadis and Narayan (2013).

###### Definition A.3 (Partial Consistency).

Given a set $\mathit{V}\subseteq\mathsf{AName}$ and three binary relations
$\mathit{sb}$, $\mathit{rf}$, $\mathit{mo}$ on $\mathit{V}$. a subset
$\mathit{V}^{\prime}\subseteq\mathit{V}$, and an action labelling function
$lab^{\prime}$ whose domain is $\mathit{V}^{\prime}$, we define _partial
consistency_ as follows, and denote it
$\mathsf{PartialConsistent}(\mathit{V},\mathit{V}^{\prime},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo})$:
$\mathsf{PartialConsistent}(\mathit{V},\mathit{V}^{\prime},\mathit{lab}^{\prime},\mathit{sb},\mathit{rf},\mathit{mo})\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\hskip
28.45274pt\mathsf{IrreflexiveHB}(\mathit{lab}^{\prime},_{,}\mathit{rf},\mathit{mo})\land\mathsf{ConsistentAlloc}(\mathit{lab}^{\prime})\
\land$
$\hskip 28.45274pt(\forall a,(a\in