# Branching Bisimulation Semantics Enables Noninterference Analysis of Reversible Systems

Andrea Esposito, Alessandro Aldini, Marco Bernardo

<figure><img src="image_1.png" /></figure>

To cite this version:

Andrea Esposito, Alessandro Aldini, Marco Bernardo. Branching Bisimulation Semantics Enables Noninterference Analysis of Reversible Systems. 43th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal. pp.57-74, 10.1007/978-3-031-35355-0_5 . hal-04731937

HAL Id: hal-04731937

https://inria.hal.science/hal-04731937v1

Submitted on 11 Oct 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_3.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Branching Bisimulation Semantics Enables Noninterference Analysis of Reversible Systems

Andrea Esposito(✉), Alessandro Aldini, and Marco Bernardo

Dipartimento di Scienze Pure e Applicate, Università di Urbino, Urbino, Italy

a.esposito30@campus.uniurb.it

**Abstract.** The theory of noninterference supports the analysis and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back and forth computations, it is necessary to move to a sufficiently expressive semantics that, in an interleaving framework, has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the classical hierarchy based on weak bisimilarity.

## 1 Introduction

Noninterference was introduced by Goguen and Meseguer [22] to reason about the way in which illegitimate information flows can occur in multi-level security systems from high-level agents to low-level ones due to covert channels. Since the first definition conceived for deterministic state machines, in the last four decades a lot of work has been done that led to a variety of extensions (dealing with non-determinism or quantitative domains) in multiple frameworks (from language-based security to concurrency theory); see, e.g., [15,2,32,24,25] and the references therein. Analogously, the techniques proposed to verify information-flow security properties based on noninterference have followed several different approaches, ranging from the application of type theory [44] and abstract interpretation [19] to control flow analysis and equivalence or model checking [16,33,3].

Noninterference guarantees that low-level agents can never infer from their observations what high-level agents are doing. Regardless of its specific definition, noninterference is closely tied to the notion of behavioral equivalence, because the idea is to compare the system behavior with high-level actions being prevented and the system behavior with those actions being hidden. Historically, one of the most established formal definitions of noninterference properties relies
on weak bisimilarity in a process algebraic framework [34], as it naturally lends
itself to reason formally about covert channels and illegitimate information flows.

While the literature concentrated on weak bisimilarity so far [15], in this
paper we claim that it is worth studying nondeterministic noninterference
in a different setting, relying on branching bisimulation semantics. Branch-
ing bisimilarity was introduced in [21] as a refinement of weak bisimilarity
to preserve the branching structure of processes also when abstracting from
invisible actions. It features a complete axiomatization whose only τ-axiom is
a.(τ.(y + z) + y) = a.(y + z), where a is an action, τ is an invisible action, and
y and z are process terms. Moreover, while weak bisimilarity can be verified in
O(n² · m · log n), where m is the number of transitions and n is the number of
states of the labeled transition system underlying the process at hand, branch-
ing bisimilarity can be verified more efficiently. An O(m · n) algorithm has been
provided in [23] and, more recently, an even faster O(m · log n) algorithm has
been developed in [26].

A clear motivation for passing to branching bisimilarity is provided by the
setting of reversible computing – for which no information flow security approach
exists to the best of our knowledge – where weak bisimilarity does not represent
a proper tool for the comprehensive analysis of covert channels. In this setting,
the model of computation features both forward and backward computations,
i.e., computational processes are reversible [28,6]. This paradigm has turned
out to have interesting applications in computational biology [38,39], parallel
discrete-event simulation [36,41], robotics [31], control theory [42], fault tolerant
systems [10,12,29,43], and concurrent program debugging [18,30].

Behavioral equivalences for reversible processes must take into account the
fact that computations are allowed to proceed not only forward but also back-
ward. To this aim, back-and-forth bisimilarity, introduced in [11], requires that
two systems are able to mimic each other’s behavior stepwise not only in per-
forming actions that follow the arrows of the labeled transition systems, but
also in undoing those actions when going backwards. Formally, back-and-forth
bisimulations are defined on computation paths instead of states thus preserving
not only causality but also history, as backward moves are constrained to take
place along the same path followed in the forward direction even in the pres-
ence of concurrency. In [11] it was shown that strong back-and-forth bisimilarity
coincides with the usual notion of strong bisimilarity, while weak back-and-forth
bisimilarity is surprisingly finer than standard weak bisimilarity, and it coincides
with branching bisimilarity. In particular, this latter result will allow us to inves-
tigate the nature of covert channels in reversible systems by using a standard
process calculus, e.g., without having to decorate executed actions like in [37] or
store them into stack-based memories like in [9].

Once established that branching bisimilarity enables noninterference analysis
of reversible systems, the novel contribution of this paper is the study of non-
interference security properties based on branching bisimilarity. In addition to
investigating preservation and compositionality features, we compare the result-
ing properties with those based on weak bisimilarity [15] and we establish a
taxonomy of the former that can be naturally applied to those based on weak
back-and-forth bisimilarity for reversible systems. Moreover, we show that, in the
<figure><img src="image_4.png" /><figcaption>Fig. 1. States $s_1$ and $s_2$ are weakly bisimilar but not branching bisimilar</figcaption></figure>

whenever $(s_1, s_2) \in \mathcal{B}$, then for all actions $a \in A$:

$$\text{ whenever } s_1 \xrightarrow{a} s'_1, \text{ then } s_2 \xrightarrow{a} s'_2 \text{ with } (s'_1, s'_2) \in \mathcal{B}. \quad \blacksquare$$

Weak bisimilarity [34] abstracts from unobservable actions, which are denoted by $\tau$. Let $s \xrightarrow{\tau^*} s'$ means that $s' \in \text{reach}(s)$ and, whenever $s' \neq s$, there is a finite sequence of transitions from $s$ to $s'$ each of which is labeled with $\tau$.

**Definition 3.** Let $(S, A, \rightarrow)$ be an LTS and $s_1, s_2 \in S$. We say that $s_1$ and $s_2$ are weakly bisimilar, written $s_1 \approx s_2$, iff $(s_1, s_2) \in \mathcal{B}$ for some weak bisim-ulation $\mathcal{B}$. A symmetric binary relation $\mathcal{B}$ over $S$ is a weak bisimulation iff, whenever $(s_1, s_2) \in \mathcal{B}$, then:

$$\text{ whenever } s_1 \xrightarrow{\tau} s'_1, \text{ then } s_2 \xrightarrow{\tau^*} s'_2 \text{ with } (s'_1, s'_2) \in \mathcal{B}; \quad \blacksquare$$

$$\text{ whenever } s_1 \xrightarrow{a} s'_1 \text{ for } a \in A \setminus \{\tau\}, \text{ then } s_2 \xrightarrow{a} s'_2 \text{ with } (s'_1, s'_2) \in \mathcal{B}. \quad \blacksquare$$

Branching bisimilarity [21] is finer than weak bisimilarity as it preserves the branching structure of the abstracted $\tau$-actions.

**Definition 4.** Let $(S, A, \rightarrow)$ be an LTS and $s_1, s_2 \in S$. We say that $s_1$ and $s_2$ are branching bisimilar, written $s_1 \approx_b s_2$, iff $(s_1, s_2) \in \mathcal{B}$ for some branching bisimulation $\mathcal{B}$. A symmetric binary relation $\mathcal{B}$ over $S$ is a branching bisimula-tion iff, whenever $(s_1, s_2) \in \mathcal{B}$, then for all actions $a \in A$:

$$\text{ whenever } s_1 \xrightarrow{a} s'_1, \text{ then:} \quad \bullet$$

$$\text{ either } a = \tau \text{ and } (s'_1, s_2) \in \mathcal{B}; \quad \bullet$$

$$\text{ or } s_2 \xrightarrow{\tau^*} \bar{s}_2 \xrightarrow{a} s'_2 \text{ with } (s_1, \bar{s}_2) \in \mathcal{B} \text{ and } (s'_1, s'_2) \in \mathcal{B}. \quad \blacksquare$$

An example that highlights the higher distinguishing power of branching bisimilarity is given in Fig. 1, where every LTS is depicted as a directed graph in which vertices represent states and action-labeled edges represent transitions. The initial states $s_1$ and $s_2$ of the LTSs are weakly bisimilar but not branching bisimilar. The only transition that distinguishes $s_1$ and $s_2$ is the a-transition of $s_2$, which can be mimicked by $s_1$ according to weak bisimilarity by performing the $\tau$-transition followed by the a-transition. However, $s_1$ cannot respond in the same way according to branching bisimilarity. If $s_1$ performs the $\tau$-transition followed by the a-transition, then the state reached after the $\tau$-transition should be branching bisimilar to $s_2$, which is not the case because of the b-transition departing from $s_2$.
## 2.2 A Process Calculus with High and Low Actions

We now introduce a basic process calculus to formalize the security properties of interest. To address two security levels, actions are divided into high and low. We denote by $\mathcal{A} = \mathcal{A}_H \cup \mathcal{A}_L$ the set of visible actions, where $\mathcal{A}_H \cap \mathcal{A}_L = \emptyset$, with $\mathcal{A}_H$ being the set of high-level actions, ranged over by $h$, and $\mathcal{A}_L$ being the set of low-level actions, ranged over by $l$. Furthermore $\mathcal{A}_\tau = \mathcal{A} \cup \{\tau\}$, where $\tau \notin \mathcal{A}$ is the invisible or silent action.

The set $\mathbb{P}$ of process terms is obtained by considering typical operators from [34,8]. In particular, in addition to the usual operators for sequential, alternative, and parallel compositions, we include restriction and hiding as they are necessary to formalize noninterference properties. The syntax is:

$$P ::= \emptyset | a.P | P + P | P \parallel_L P | P \setminus L | P / L$$

where:

- $\emptyset$ is the terminated process.

- $a.\dots$, for $a \in \mathcal{A}_\tau$, is the action prefix describing a process that initially performs action $a$.

- $\_ + \_\_$ is the alternative composition operator expressing a nondeterministic choice between two processes based on their executable actions.

- $\_\_\parallel_L\_$, for $L \subseteq \mathcal{A}$, is the parallel composition operator that forces two processes to synchronize on any action in $L$.

- $\_\_\setminus L$, for $L \subseteq \mathcal{A}$, is the restriction operator, which prevents the execution of actions in $L$.

- $\_\_\slash L$, for $L \subseteq \mathcal{A}$, is the hiding operator, which turns all the executed actions in $L$ into the invisible action $\tau$.

The operational semantic rules for the process language are shown in Table 1 and produce the LTS $(\mathbb{P}, \mathcal{A}_\tau, \rightarrow)$ where $\rightarrow \subseteq \mathbb{P} \times \mathcal{A}_\tau \times \mathbb{P}$, to which the bisimulation equivalences defined in the previous section are applicable.

## 2.3 Weak-Bisimilarity-Based Information-Flow Security Properties

The intuition behind noninterference in a two-level security system is that, whenever a group of agents at the high security level performs some actions, the effect of those actions should not be seen by any agent at the low security level. Below is a representative selection of weak-bisimilarity-based noninterference properties – *Nondeterministic Non-Interference* (NNI) and *Non-Deducibility on Composition* (NDC) – followed by their relationships [15], which we then comment.

**Definition 5.** Let $P \in \mathbb{P}$:

- $P \in \text{BSNNI} \iff P \setminus \mathcal{A}_H \approx P / \mathcal{A}_H$.

- $P \in \text{BNDC} \iff \text{ for all } Q \in \mathbb{P} \text{ such that every } Q' \in \text{reach}(Q) \text{ can execute only actions in } \mathcal{A}_H \text{ and for all } L \subseteq \mathcal{A}_H, P \setminus \mathcal{A}_H \approx ((P \parallel_L Q) / L) \setminus \mathcal{A}_H$.

- $P \in \text{SBSNNI} \iff P \in \text{BSNNI} \text{ and for all } P' \in \text{reach}(P), P' \in \text{BSNNI}$.
<table><caption>**Table 1.** Operational semantic rules</caption><tr><td>Prefix</td><td>P<sub>1</sub> &rarr; P'<sub>1</sub><br>P<sub>1</sub> + P<sub>2</sub> &rarr; P'<sub>1</sub></td><td>a &rarr; P &rarr; P<br>P<sub>2</sub> &rarr; P'<sub>2</sub><br>P<sub>1</sub> + P<sub>2</sub> &rarr; P'<sub>2</sub></td></tr><tr><td>Choice</td><td></td><td></td></tr><tr><td>Synchronization</td><td>P<sub>1</sub> &rarr; P'<sub>1</sub><br>P<sub>1</sub> &parallel; L<br>P<sub>2</sub> &rarr; P'<sub>2</sub><br>P<sub>2</sub> &parallel; L</td><td>P<sub>1</sub> &rarr; P'<sub>1</sub><br>P<sub>1</sub> &parallel; L<br>P<sub>2</sub> &rarr; P'<sub>2</sub><br>P<sub>2</sub> &parallel; L</td></tr><tr><td>Interleaving</td><td>P<sub>1</sub> &rarr; P'<sub>1</sub><br>P<sub>1</sub> &parallel; L<br>P<sub>2</sub> &rarr; P'<sub>2</sub><br>P<sub>2</sub> &parallel; L</td><td>P<sub>1</sub> &rarr; P'<sub>2</sub><br>P<sub>1</sub> &parallel; L<br>P<sub>2</sub> &rarr; P'<sub>2</sub><br>P<sub>2</sub> &parallel; L</td></tr><tr><td>Restriction</td><td>P &rarr; P'<br>P &parallel; L</td><td>P &rarr; P'<br>P &parallel; L</td></tr><tr><td>Hiding</td><td>P &rarr; P'<br>P &parallel; L<br>P/L &rarr; P'/L</td><td>P &rarr; P'<br>P &parallel; L<br>P/L &rarr; P'/L</td></tr></table>

- $P \in \text{SBNDC} \iff \text{for all } P' \in \text{reach}(P) \text{ and for all } P'' \text{ such that } P' \xrightarrow{a} P'' \text{ for some } a \in \mathcal{A}_{\mathcal{H}}, P' \setminus \mathcal{A}_{\mathcal{H}} \approx P'' \setminus \mathcal{A}_{\mathcal{H}}$. ■

**Theorem 1.** SBNDC $\subset$ SBSNNI $\subset$ BNDC $\subset$ BSNNI. ■

Historically, one of the first and most intuitive proposals is the *Bisimulation-based Strong Nondeterministic Non-Interference* (BSNNI). Basically, it is satisfied by any process *P* that behaves the same when its high-level actions are prevented (as modeled by $P \setminus \mathcal{A}_{\mathcal{H}}$) or when they are considered as hidden, unobservable actions (as modeled by $P/\mathcal{A}_{\mathcal{H}}$). The equivalence between these two low-level views of *P* states that a low-level observer cannot distinguish the high-level behavior of the system. For instance, in $l.\underline{0} + h.l.\underline{0}$ a low-level agent that observes the execution of *l* cannot infer anything about the execution of *h*. Indeed, $(l.\underline{0} + h.l.\underline{0}) \setminus \{h\} \approx (l.\underline{0} + h.l.\underline{0}) / \{h\}$ because $l.\underline{0} \approx l.\underline{0} + \tau.l.\underline{0}$.

BSNNI is not powerful enough to capture covert channels that derive from the behavior of the high-level agent interacting with the system. For instance, $l.\underline{0} + h_1.h_2.l.\underline{0}$ is BSNNI for the same reason discussed above. However, a high-level agent could decide to enable $h_1$ and then disable $h_2$, thus turning the low-level view of the system into $l.\underline{0} + \tau.\underline{0}$, which is clearly distinguishable from $l.\underline{0}$, as only in the former the low-level observer may not observe *l*. To overcome such a limitation, the most obvious solution consists of checking explicitly the interaction between the system and every possible high-level agent *Q*. The resulting property is the *Bisimulation-based Non-Deducibility on Composition* (BNDC), which is characterized by a universal quantification over *Q*.

To circumvent the verification problems related to such a quantifier, several properties have been proposed that are stronger than BNDC. They all express some persistency conditions, stating that the security checks shall be somehow extended also to the derivatives of a secure process. Three of the most representative ones are the variant of BSNNI that requires every reachable state to satisfy BSNNI itself, called *Strong* BSNNI (SBSNNI), the variant of BNDC that requires every reachable state to satisfy BNDC, called *Persistent* BNDC
(P_BNDC), and the Strong BNDC (SBNDC), which requires the low-level view of every reachable state to be the same before and after the execution of any high-level action. Notice that the SBNDC condition states that the execution of high-level actions must be completely transparent to the low-level agents. The properties P_BNDC and SBSNNI have been proven to be equivalent in [17], hence we will focus only on SBSNNI.

## 3 Use Case: DBMS Transactions – Part I

Consider a multi-threaded system supporting the execution of concurrent transactions operating on a healthcare database. Authorized users can write data on such a database, which is then accessed by a dedicated module to feed the training set for a machine learning model built for data analysis purposes.

On the one hand, different authentication mechanisms can be employed to identify users and ensure data authenticity for each transaction. We address a simple password-based mechanism (pwd), a more sophisticated two-factor authentication system (2fa), and finally a scheme based on single sign on (sso) [7]. On the other hand, to protect the privacy of health data in the trained model, only data transmitted through a highly secure mechanism, i.e., 2fa or sso, can be used to feed the training set. In any case, users must not be aware of which data are actually chosen to train the machine learning model [5]. To this aim, the database management system (DBMS) is enabled to internally and transparently decide not to consider for the training set some transactions.

A simplified model describing how a write transaction is handled by the considered DBMS is represented by the following process term, whose LTS is depicted in Fig. 2:

$$WT := l_{pwd} \cdot \underline{0} + \tau \cdot (\tau \cdot l_{sso} \cdot \underline{0} + \tau \cdot l_{2fa} \cdot \underline{0}) + (h \cdot l_{sso} \cdot \underline{0} + h \cdot l_{2fa} \cdot \underline{0})$$

The low-level actions of the form $l_*$ express that the transaction is conducted under the authentication method represented by $\star$, while the high-level action $h$ expresses a private interaction with the machine learning module intended to avoid the transfer of the transaction data to the training set.

The DBMS is ready to manage the transaction through the password-based mechanism, as described by subterm $l_{pwd} \cdot \underline{0}$. Alternatively, it internally decides that the transaction data will be passed to the training set and, therefore, one of the two highly secure mechanisms must be chosen nondeterministically, as described by subterm $\tau \cdot (\tau \cdot l_{sso} \cdot \underline{0} + \tau \cdot l_{2fa} \cdot \underline{0})$. Otherwise, it can interact with the machine learning module, while nondeterministically choosing one of the two highly secure mechanisms, as described by subterm $h \cdot l_{sso} \cdot \underline{0} + h \cdot l_{2fa} \cdot \underline{0}$. This interaction is intended to confuse the user, who should not infer whether the transaction data will be used for the training set or not by simply observing which kind of authentication is required by the DBMS. This privacy condition is ensured if the interaction with the machine learning module does not interfere with the low-level view of the system perceived by the user, which can be verified as a noninterference property.
<figure><img src="image_5.png" /><figcaption>Fig. 2. LTS underlying WT</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 3. LTSs of the low-level views of WT: $WT \setminus A_H$ (left) and $WT/A_H$ (right)</figcaption></figure>

As far as ≈-based noninterference is concerned, WT does not leak any information from high level to low level. Indeed, the system is SBSNNI and hence also BNDC and BSNNI by virtue of Theorem 1. First, by observing Fig. 3, it is easy to see that $WT \setminus A_H \approx WT / A_H$. The weak bisimulation relating the two low-level views of WT is given by the following partition of the state space:

$$ \{\{s_1, r_1\}, \{s_2, r_2\}, \{s_3, r_3, r'_3\}, \{s_4, r_4, r'_4\}, \{s_5, r_5, r'_5, s_6, r_6, r'_6, s_7, r_7\}\} $$

Then, by observing that the only high-level action is enabled at the initial state of WT, it follows that WT is SBSNNI.

# 4 Security Properties Based on Branching Bisimilarity

While the literature on noninterference mainly concentrates on weak bisimilarity semantics, in this section we recast information-flow security definitions in terms of branching bisimilarity and investigate their characteristics as well as their relationships with the definitions based on weak bisimilarity.
The noninterference properties that reformulate the ones in Definition 5 by replacing the weak bisimilarity check with the branching bisimilarity check are termed, respectively, BrSNNI, BrNDC, SBrSNNI, and SBrNDC.

## 4.1 Preservation and Compositionality

All the $\approx_b$-based noninterference properties turn out to be preserved by $\approx_b$. This means that, whenever a process $P_1$ is secure under any of such properties, then every other branching bisimilar process $P_2$ is secure too. This is very useful for automated property verification, as it allows one to work with the process with the smallest state space among the equivalent ones.

**Theorem 2.** Let $P_1, P_2 \in \mathbb{P}$ and $\mathcal{P} \in \{\text{BrSNNI}, \text{BrNDC}, \text{SBrSNNI}, \text{SBrNDC}\}$. If $P_1 \approx_b P_2$, then $P_1 \in \mathcal{P} \iff P_2 \in \mathcal{P}$. ■

As far as modular verification is concerned, like in the weak bisimilarity case [15] only the local properties SBrSNNI and SBrNDC are compositional, i.e., are preserved by the operators of the calculus.

**Theorem 3.** Let $P, P_1, P_2 \in \mathbb{P}$ and $\mathcal{P} \in \{\text{SBrSNNI}, \text{SBrNDC}\}$. Then:

1. $P \in \mathcal{P} \implies a. P \in \mathcal{P}$ for all $a \in \mathcal{A}_\tau \setminus \mathcal{A}_H$.

2. $P_1, P_2 \in \mathcal{P} \implies P_1 \parallel_L P_2 \in \mathcal{P}$ for all $L \subseteq A$.

3. $P \in \mathcal{P} \implies P \setminus L \in \mathcal{P}$ for all $L \subseteq \mathcal{A}_L$ if $\mathcal{P}=\text{SBrSNNI}$, $L \subseteq \mathcal{A}$ if $\mathcal{P}=\text{SBrNDC}$.

4. $P \in \mathcal{P} \implies P / L \in \mathcal{P}$ for all $L \subseteq \mathcal{A}_L$.

Note that, like for weak bisimilarity, no property based on branching bisimilarity is compositional with respect to alternative composition. As an example, let us consider processes $P_1 := l.\underline{0}$ and $P_2 := h.\underline{0}$. Both are BrSNNI, as $l.\underline{0} \setminus \{h\} \approx_b l.\underline{0} / \{h\}$ and $h.\underline{0} \setminus \{h\} \approx_b h.\underline{0} / \{h\}$, but $P_1 + P_2 \notin \text{BrSNNI}$ because $(l.\underline{0} + h.\underline{0}) \setminus \{h\} \approx_b l.\underline{0} \not\approx_b h.\underline{0} + \tau.\underline{0} \approx_b (l.\underline{0} + h.\underline{0}) / \{h\}$. It can be easily checked that $P_1 + P_2 \notin \mathcal{P}$ for $\mathcal{P} = \{\text{BrNDC}, \text{SBrSNNI}, \text{SBrNDC}\}$.

We point out that compositionality with respect to action prefix and hiding, although limited to non-high actions and low actions respectively, is established by Theorem 3 but was not investigated in [15] under weak bisimilarity.

## 4.2 Taxonomy of Security Properties

First of all, the relationships among the $\approx_b$-based noninterference properties follow the same pattern as Theorem 1.

**Theorem 4.** SBrNDC $\subset$ SBrSNNI $\subset$ BrNDC $\subset$ BrSNNI. ■

All the inclusions above are strict as we now show:

- The process $\tau.l.\underline{0} + l.l.\underline{0} + h.l.\underline{0}$ is SBrSNNI because $(\tau.l.\underline{0} + l.l.\underline{0} + h.l.\underline{0}) \setminus \{h\} \approx_b (\tau.l.\underline{0} + l.l.\underline{0} + h.l.\underline{0}) / \{h\}$ and action $h$ is enabled only by the initial process so every derivative is BrSNNI. It is not SBrNDC because the low-level view of the process reached after action $h$, i.e., $(l.\underline{0}) \setminus \{h\}$, is not branching bisimilar to $(\tau.l.\underline{0} + l.l.\underline{0} + h.l.\underline{0}) \setminus \{h\}$.
- The process $l.\underline{0} + l.l.\underline{0} + l.h.l.\underline{0}$ is BrNDC because, whether there are synchronizations with high-level actions or not, the overall process can always perform either an *l*-action or a sequence of two *l*-actions without incurring any problematic branching. The process is not SBrSNNI because the reachable process $h.l.\underline{0}$ is not BrSNNI.

- The process $l.\underline{0}+h.h.l.\underline{0}$ is BrSNNI due to $(l.\underline{0}+h.h.l.\underline{0})\setminus\{h\} \approx_b (l.\underline{0}+h.h.l.\underline{0})/\{h\}$, but is not BrNDC due to $((l.\underline{0}+h.h.l.\underline{0})\|_{\{h\}}(h.\underline{0}))/\{h\}) \setminus \{h\} \not\approx_b (l.\underline{0}+h.h.l.\underline{0}) \setminus \{h\}$ as $(l.\underline{0}+h.h.l.\underline{0}) \setminus \{h\}$ behaves as $l.\underline{0}$.

Secondly, we observe that all the $\approx_b$-based noninterference properties listed in Theorem 4 imply the corresponding properties listed in Definition 5 due to the fact that $\approx_b$ is finer than $\approx$ [21].

**Theorem 5.** The following properties hold:

1. BrSNNI $\subset$ BSNNI.

2. BrNDC $\subset$ BNDC.

3. SBrSNNI $\subset$ SBSNNI.

4. SBrNDC $\subset$ SBNDC.

<figure><img src="image_7.png" /></figure>

All the inclusions above are strict due to the following result.

**Theorem 6.** Let $P_1, P_2 \in \mathbb{P}$ be such that $P_1 \approx P_2$ but $P_1 \not\approx_b P_2$. If $P_1$ and $P_2$ do not include high-level actions, then $Q \in \{P_1+h.P_2, P_2+h.P_1\}$ is such that:

1. $Q \in$ BSNNI but $Q \notin$ BrSNNI.

2. $Q \in$ BNDC but $Q \notin$ BrNDC.

3. $Q \in$ SBSNNI but $Q \notin$ SBrSNNI.

4. $Q \in$ SBNDC but $Q \notin$ SBrNDC.

<figure><img src="image_8.png" /></figure>

An alternative strategy to explore the differences between $\approx$ and $\approx_b$ with respect to B/BrSNNI and SB/BrSNNI is to consider the two $\tau$-axioms $\tau.x+x = \tau.x$ and $a.(\tau.x+y)+a.x = a.(\tau.x+y)$ for $\approx$ [34]. The strategy is inspired by the initial remarks in [21], where it is noted that the two mentioned axioms are not valid for $\approx_b$ and are responsible for the lack of distinguishing power of $\approx$ over $\tau$-branching processes. For each axiom, the strategy consists of constructing a pair of new processes from the ones equated in the axiom, such that they are weakly bisimilar by construction but not branching bisimilar. Then from this pair of processes we define a new process $P$ such that $P \setminus \mathcal{A}_H$ and $P/\mathcal{A}_H$ are isomorphic to the constructed processes.

**Theorem 7.** From $\tau.x+x = \tau.x$ it is possible to construct $P \in \mathbb{P}$ such that $P \in$ BSNNI but $P \notin$ BrSNNI and $P \in$ SBSNNI but $P \notin$ SBrSNNI.

<figure><img src="image_9.png" /></figure>

**Theorem 8.** From $a.(\tau.x+y)+a.x = a.(\tau.x+y)$ it is possible to construct $P \in \mathbb{P}$ such that $P \in$ BSNNI but $P \notin$ BrSNNI and $P \in$ SBSNNI but $P \notin$ SBrSNNI.

<figure><img src="image_10.png" /></figure>
<figure><img src="image_11.png" /><figcaption>Fig. 4. Taxonomy of security properties based on weak and branching bisimilarities</figcaption></figure>

Based on the results in Theorems 1, 4, and 5, the diagram in Fig. 4 summarizes the inclusions among the various noninterference properties, where $\mathcal{P} \to \mathcal{Q}$ means that $\mathcal{P}$ is strictly included in $\mathcal{Q}$. The missing arrows in the diagram, witnessing incomparability, are justified by the following counterexamples:

- SBNDC vs. SBrSNNI. The process $\tau.l.\underline{0} + l.l.\underline{0} + h.l.\underline{0}$ is BrSNNI as $\tau.l.\underline{0} + l.l.\underline{0} \approx_b \tau.l.\underline{0} + l.l.\underline{0} + \tau.l.\underline{0}$. It is also SBrSNNI because every reachable state does not enable any more high-level actions. However it is not SBNDC, because after the process has performed the high-level action $h$ it can perform a single action $l$, while the original process with the restriction on high-level actions can go down a path where it performs two $l$-actions. On the other hand, the process $Q$ mentioned in Theorem 6 is SBNDC but neither BrSNNI nor SBrSNNI.

- SBSNNI vs. BrNDC. The process $l.h.l.\underline{0} + l.\underline{0} + l.l.\underline{0}$ is BrSNNI as $l.\underline{0} + l.\underline{0} + l.l.\underline{0} \approx_b l.\tau.l.\underline{0} + l.\underline{0} + l.l.\underline{0}$. In particular, the subprocesses $l.\tau.l.\underline{0}$ and $l.l.\underline{0}$ are equated by virtue of the other axiom of weak bisimilarity, $a.\tau.x = a.x$, which holds also for branching bisimilarity. The same process is also BrNDC as it includes only one high-level action, hence the only possible high-level strategy coincides with the check conducted by BrSNNI. However, the process is not SBSNNI because of the reachable process $h.l.\underline{0}$, which is not BSNNI. On the other hand, the process $Q$ mentioned in Theorem 6 is SBSNNI but not BrSNNI and, therefore, cannot be BrNDC.

- BNDC vs. BrSNNI. The process $l.\underline{0} + h_1.h_2.l.\underline{0}$ is not BNDC (see Sect. 2.3), but it is BrSNNI as $l.\underline{0} \approx_b l.\underline{0} + \tau.\tau.l.\underline{0}$. In contrast, the process $Q$ mentioned in Theorem 6 is both BSNNI and BNDC, but not BrSNNI.

It is worth noting that the strongest property based on weak bisimilarity (SBNDC) and the weakest property based on branching bisimilarity (BrSNNI) are incomparable. The former is a very restrictive property because it requires a local check every time a high-level action is performed, while the latter requires a check only on the initial state. On the other hand, as shown in Theorem 6 it is very easy to construct processes that are secure under properties based on $\approx_b$ but not on $\approx_b$, due to the minimal number of high-level actions in $Q$.
# 5 Noninterference in Reversible Processes

As anticipated, we use reversible computing to motivate the study of branching-bisimilarity-based noninterference properties. To this aim, we now recall from [11] back-and-forth bisimilarity and its relationship with standard bisimilarity.

An LTS represents a reversible process if each of its transitions is seen as bidirectional. This means that any transition can be undone and that any undone transition can be redone. When going backward, it is of paramount importance to respect causality. While this is straightforward for sequential processes, it is not obvious for concurrent ones, because the last performed action is the first one to be undone but this action may not necessarily be identifiable uniquely in the presence of concurrency.

Consider for example a process that can perform action *a* in parallel with action *b*. This process can be represented as a diamond-like LTS where from the initial state an *a*-transition and a *b*-transition depart, which are respectively followed by a *b*-transition and an *a*-transition, both of which reach the final state. Suppose that action *a* completes before action *b*, so that the *a*-transition is executed before the *b*-transition. Once in the final state, either the *b*-transition is undone before the *a*-transition, or the *a*-transition is undone before the *b*-transition. Both options are causally consistent, as *a* and *b* are independent of each other, but only the former is history preserving too.

The history-preserving option is the one that was addressed in [11] in order to study reversible processes in an interleaving setting. To accomplish this, strong and weak bisimulations were redefined as binary relations between histories, formalized below as runs, instead of states. The resulting behavioral equivalences are respectively called strong and weak back-and-forth bisimilarities in [11].

**Definition 6.** A sequence $\xi = s_0 \xrightarrow{a_1} s_1 \xrightarrow{a_2} s_2 \dots s_{n-1} \xrightarrow{a_n} s_n$ is called a path from state $s_0$ of length $n \in \mathbb{N}$. We let first($\xi$) = $s_0$ and last($\xi$) = $s_n$; the empty path is indicated with $\varepsilon$. We denote by Path($s$) the set of paths from state $s$. ■

**Definition 7.** A pair $\rho = (s, \xi)$ is called a run from state $s$ iff $\xi \in \text{Path}(s)$, in which case we let path($\rho$) = $\xi$, first($\rho$) = first($\xi$), last($\rho$) = last($\xi$), with first($\rho$) = last($\rho$) = $s$ when $\xi = \varepsilon$. We denote by Run($s$) the set of runs from state $s$. ■

**Definition 8.** Let $\rho = (s, \xi) \in \text{Run}(s)$ and $\rho' = (s', \xi') \in \text{Run}(s')$:

- Their composition $\rho\rho' = (s, \xi\xi') \in \text{Run}(s)$ is defined iff $\text{last}(\rho) = \text{first}(\rho')$.

- We write $\rho \xrightarrow{a} \rho'$ iff there exists $\rho'' = (s, s \xrightarrow{a} s')$ with $s = \text{last}(\rho)$ such that $\rho' = \rho\rho''$. ■

In the behavioral equivalences of [11], for the LTS $(S, A, \rightarrow)$ the set $R$ of its runs is considered in lieu of the set $S$ of its states.

**Definition 9.** Let $(S, A, \rightarrow)$ be an LTS and $s_1, s_2 \in S$. We say that $s_1$ and $s_2$ are strongly back-and-forth bisimilar, written $s_1 \sim_{\text{bf}} s_2$, iff $((s_1, \varepsilon), (s_2, \varepsilon)) \in \mathcal{B}$
for some strong back-and-forth bisimulation $\mathcal{B}$. A symmetric binary relation $\mathcal{B}$
over $R$ is a strong back-and-forth bisimulation iff, whenever $(\rho_1, \rho_2) \in \mathcal{B}$, then
for all actions $a \in A$:

- whenever $\rho_1 \xrightarrow{a} \rho_1'$, then $\rho_2 \xrightarrow{a} \rho_2'$ with $(\rho_1', \rho_2') \in \mathcal{B}$;

- whenever $\rho'_1 \xrightarrow{a} \rho_1$, then $\rho'_2 \xrightarrow{a} \rho_2$ with $(\rho'_1, \rho'_2) \in \mathcal{B}$.

**Definition 10.** Let $(S, A, \rightarrow)$ be an LTS and $s_1, s_2 \in S$. We say that $s_1$ and $s_2$ are weakly back-and-forth bisimilar, written $s_1 \approx_{\text{bf}} s_2$, iff $((s_1, \varepsilon), (s_2, \varepsilon)) \in \mathcal{B}$ for some weak back-and-forth bisimulation $\mathcal{B}$. A symmetric binary relation $\mathcal{B}$ over $R$ is a weak back-and-forth bisimulation iff, whenever $(\rho_1, \rho_2) \in \mathcal{B}$, then:

- whenever $\rho_1 \xrightarrow{\tau} \rho_1'$, then $\rho_2 \xrightarrow{\tau^*} \rho_2'$ with $(\rho_1', \rho_2') \in \mathcal{B}$;

- whenever $\rho'_1 \xrightarrow{\tau} \rho_1$, then $\rho'_2 \xrightarrow{\tau^*} \rho_2$ with $(\rho'_1, \rho'_2) \in \mathcal{B}$;

- whenever $\rho_1 \xrightarrow{a} \rho'_1$ for $a \in A \setminus \{\tau\}$, then $\rho_2 \xrightarrow{a} \rho'_2 \xrightarrow{\tau^*} \rho_2'$ with $(\rho'_1, \rho'_2) \in \mathcal{B}$;

- whenever $\rho'_1 \xrightarrow{a} \rho_1$ for $a \in A \setminus \{\tau\}$, then $\rho'_2 \xrightarrow{a} \rho_2 \xrightarrow{\tau^*} \rho_2'$ with $(\rho'_1, \rho'_2) \in \mathcal{B}$.

In [11] it was shown that strong back-and-forth bisimilarity coincides with
strong bisimilarity. Surprisingly, weak back-and-forth bisimilarity does not coin-
cide with weak bisimilarity. Instead, it coincides with branching bisimilarity.

**Theorem 9.** Let $(S, A, \rightarrow)$ be an LTS and $s_1, s_2 \in S$. Then:

- $s_1 \sim_{\text{bf}} s_2$ iff $s_1 \sim s_2$.

- $s_1 \approx_{\text{bf}} s_2$ iff $s_1 \approx_{\text{b}} s_2$.

As a consequence, the properties BrSNNI, BrNDC, SBrSNNI, and SBrNDC
do not change if $\approx_b$ is replaced by $\approx_{\text{bf}}$. This allows us to study noninterference
properties for reversible systems by using $\approx_b$ in a standard process calculus like
the one of Sect. 2.2, without having to decorate executed actions like in [37] or
store them into stack-based memories like in [9].

6 Use Case: DBMS Transactions – Part II

The example provided in Sect. 3 is useful to illustrate the limitations of weak bisimilarity when investigating potential covert channels in reversible systems.

It turns out that $WT \setminus \mathcal{A}_H \not\approx_b WT / \mathcal{A}_H$, i.e., $WT$ is not BrSNNI, and hence not even BrNDC, SBrSNNI, and SBrNDC by virtue of Theorem 4. As can be seen in Fig. 3, the reason is that, if $WT / \mathcal{A}_H$ performs the leftmost $\tau$-action and hence moves to state $r'_3$, from which the only executable action is $l_{sso}$, then according to the definition of branching bisimilarity $WT \setminus \mathcal{A}_H$ can either:

1. stay idle, but from that state $WT \setminus \mathcal{A}_H$ can then perform actions other than $l_{sso}$ that cannot be matched on the side of $WT / \mathcal{A}_H$;

2. perform two $\tau$-actions thereby reaching state $s_3$, but the traversed state $s_2$ is not branching bisimilar to the initial state of $WT / \mathcal{A}_H$.
In a standard model of execution, where the computation can proceed only forward, the distinguishing power of branching bisimilarity may be considered too severe, as no practical covert channel actually occurs and the system can be considered noninterfering as shown in Sect. 3. Indeed, a low-level user has no possibility of distinguishing the internal move performed by $WT/\mathcal{A}_H$ and leading to $l_{sso} \cdot 0$ from the sequence of internal moves performed by $WT \setminus \mathcal{A}_H$ and leading to $l_{sso} \cdot 0$ as well. This motivates the fact that, historically, weak bisimilarity has been preferred in the setting of noninterference.

Now we know that, if we replace the branching bisimulation semantics with the weak back-and-forth bisimulation semantics, nothing changes about the outcome of noninterference verification. Assuming that the DBMS allows transactions to be reversed, it is instructive to discuss why BrSNNI is not satisfied by following the formalization of the weak back-and-forth bisimulation semantics provided in Sect. 5.

After $WT/\mathcal{A}_H$ performs the run $(r_1, (r_1 \xrightarrow{\tau} r'_3 \xrightarrow{l_{sso}} r'_5))$, process $WT \setminus \mathcal{A}_H$ can respond by performing the run $(s_1, (s_1 \xrightarrow{\tau} s_2 \xrightarrow{\tau} s_3 \xrightarrow{l_{sso}} s_5))$. If either process goes back by undoing $l_{sso}$, then the other one can undo $l_{sso}$ as well and the states $r'_3$ and $s_3$ are reached. However, if $WT \setminus \mathcal{A}_H$ goes further back by undoing $s_2 \xrightarrow{\tau} s_3$, then $WT/\mathcal{A}_H$ can either:

- undo $r_1 \xrightarrow{\tau} r'_3$, but in this case $r_1$ enables action $l_{pwd}$ while $s_2$ does not;

- stay idle, but in this case $r'_3$ enables only $l_{sso}$, while $s_2$ can go down the path $s_2 \xrightarrow{\tau} s_4 \xrightarrow{l_{2fa}} s_6$ as well.

This line of reasoning immediately allows us to reveal a potential covert channel under reversible computing. In fact, let us assume that the transaction modeled by $WT$ is not only executed forward, but also enables backward computations triggered, e.g., whenever debugging mode is activated. This may happen in response to some user-level malfunctioning, which may be due, for instance, to the authentication operation or to the transaction execution. As formally shown above, if the action $l_{sso}$ performed just after the high-level interaction is undone, then the system enables again the execution of the action $l_{pwd}$. This is motivated in our example by the fact that, in any case, the transaction data will not be transferred to the training set, so that any kind of authentication is admissible. On the other hand, this is not possible by undoing the action $l_{sso}$ departing from state $r_3$ in $WT/\mathcal{A}_H$, because in such a case the transaction data must be protected through a highly secure mechanism. In other words, by reversing the computation the low-level user can become aware of the fact that the transaction data are feeding the training set or not.

In the literature, there are several reverse debuggers working in this way like, e.g., UndoDB [13], a Linux-based interactive time-travel debugger that can handle multiple threads and their backward execution. For instance, it is integrated within the DBMS SAP HANA [1] in order to reduce time-to-resolution of software failures. In our example, by virtue of the observations conducted above, if the system is executed backward just after performing $l_{sso}$, a low-level user can
decide whether a high-level action had occurred before or not, thus revealing a
covert channel. Such a covert channel is completely concealed during the forward
execution of the system and is detected only when the system is executed back-
ward. More in general, this may happen when the reverse debugger is activated
by virtue of some unexpected event (e.g., segmentation faults, stack overflow
errors, memory corruption) caused intentionally or not, and by virtue of which
some undesired information flow emerges towards the low-level users.

7 Conclusions

Our study of branching-bisimilarity-based noninterference properties has estab-
lished a connection with reversible computing in the sense that those properties,
which we have investigated in a standard process calculus, are directly applica-
ble to reversible systems. To the best of our knowledge, this is the first attempt
of defining noninterference properties relying on branching bisimilarity and of
reasoning about covert channels in reversible systems.

Firstly, we have rephrased in the setting of branching bisimilarity the classical
taxonomy of nondeterministic noninterference properties based on weak bisimi-
larity. This generates an extended taxonomy that is conservative with respect to
the classical one and emphasizes the strictness of certain inclusions as well as the
incomparability of certain properties. In addition, we have studied preservation
and compositionality features of the new noninterference properties.

Secondly, we have shown that potential covert channels arising in reversible
systems cannot be revealed by employing weak bisimulation semantics. Indeed,
the higher discriminating power of branching bisimilarity is necessary to capture
information flows emerging whenever backward computations are admitted. The
correspondence discovered in [11] between branching bisimilarity and weak back-
and-forth bisimilarity confirms the adequacy of our approach.

As for future work, we are planning to further extend the noninterference
taxonomy to include more expressive properties taking into account quantita-
tive aspects of processes [4,25]. Moreover, unlike the corresponding results for
weak-bisimilarity-based noninterference properties, whose proofs rely on the use
of an up-to technique for weak bisimilarity [40], in Theorems 3 and 4 we have
proceeded by induction on the depth of the tree-like LTS underlying the consid-
ered process term, because the up-to techniques for branching bisimilarity [20,14]
seem to be too restrictive with respect to the conditions required by the non-
interference checks. Thus, we would like to study whether there exist suitable
relaxations of the latter techniques so as to be able to reformulate the proofs of
Theorems 3 and 4 accordingly, which would open the way to including recursion
in the language.

**Acknowledgment.** This research has been supported by the PRIN project *NiRvAna - Noninterference and Reversibility Analysis in Private Blockchains*.
References

1. UndoDB case studies. https://undo.io/resources/type/case-studies/. Accessed Mar 2023

2. Aldini, A.: Classification of security properties in a Linda-like process algebra. Sci. Comput. Program. **63**(1), 16–38 (2006)

3. Aldini, A., Bernardo, M.: Component-oriented verification of noninterference. J. Syst. Architect. **57**(3), 282–293 (2011)

4. Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, London (2010). https://doi.org/10.1007/978-1-84800-223-4

5. Bai, Y., Fan, M., Li, Y., Xie, C.: Privacy risk assessment of training data in machine learning. In: Proceedings of the 34th IEEE International Conference on Communications (ICC 2022), p. 1015. IEEE-CS Press (2022)

6. Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. **17**(6), 525–532 (1973)

7. Boonkrong, S.: Authentication and Access Control. Apress, Berkeley (2020)

8. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM **31**, 560–599 (1984)

9. Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19

10. Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 398–412. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452.31

11. De Nicola, R., Montanari, U., Vaandrager, F.: Back and forth bisimulations. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 152–165. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039058

12. de Vries, E., Koutavas, V., Hennessy, M.: Communicating transactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 569–583. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_39

13. Engblom, J.: A review of reverse debugging. In: Proceedings of the 4th System, Software, SoC and Silicon Debug Conference (S4D 2012), pp. 1–6. IEEE-CS Press (2012)

14. Erkens, R., Rot, J., Luttik, B.: Up-to techniques for branching bisimilarity. In: Chatzigeorgiou, A., et al. (eds.) SOFSEM 2020. LNCS, vol. 12011, pp. 285–297. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-38919-2_24

15. Focardi, R., Gorrieri, R.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45608-2_6

16. Focardi, R., Piazza, C., Rossi, S.: Proofs methods for bisimulation based information flow security. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 16–31. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47813-2_2

17. Focardi, R., Rossi, S.: Information flow security in dynamic contexts. J. Comput. Secur. **14**(1), 65–110 (2006)

18. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_26

19. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: a unifying framework for weakening information-flow. ACM Trans. Privacy Secur. **21**(2) (2018)
20. Glabbeek, R.J.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Sokołowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 473–484. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57182-5_39

21. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43, 555–600 (1996)

22. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the 2nd IEEE Symposium on Security and Privacy (SSP 1982), pp. 11–20. IEEE-CS Press (1982)

23. Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0032063

24. Hedin, D., Sabelfeld, A.: A perspective on information-flow control. In: Software Safety and Security - Tools for Analysis and Verification, vol. 33, pp. 319–347 (2012)

25. Hillston, J., et al.: Persistent stochastic non-interference. Fund. Inform. 181(1), 1–35 (2021)

26. Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: An $O(m \log n)$ algorithm for branching bisimilarity on labelled transition systems. In: TACAS 2020. LNCS, vol. 12079, pp. 3–20. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_1

27. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)

28. Landauer, R.: Irreversibility and heat generated in the computing process. IBM J. Res. Dev. 5, 183–191 (1961)

29. Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 370–390. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_21

30. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_16

31. Laursen, J.S., Ellekilde, L.P., Schultz, U.P.: Modelling reversible execution of robotic assembly. Robotica 36, 625–654 (2018)

32. Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jao-dia, S. (eds.) Encyclopedia of Cryptography and Security, pp. 605–607. Springer, Boston (2011). https://doi.org/10.1007/978-1-4419-5906-5_874

33. Martinelli, F.: Analysis of security protocols as open systems. Theoret. Comput. Sci. 290(1), 1057–1106 (2003)

34. Milner, R.: Communication and Concurrency. Prentice Hall, Hoboken (1989)

35. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309

36. Perumalla, K.S., Park, A.J.: Reverse computation for rollback-based fault tolerance in large parallel systems - evaluating the potential gains and systems effects. Clust. Comput. 17, 303–313 (2014)

37. Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebraic Program. 73, 70–96 (2007)
38. Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 218–232. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36315-3_18

39. Michele Pinna, G.: Reversing steps in membrane systems computations. In: Gheorghe, M., Rozenberg, G., Salomaa, A., Zandron, C. (eds.) CMC 2017. LNCS, vol. 10725, pp. 245–261. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73359-3_16

40. Sangiorgi, D., Milner, R.: The problem of “weak bisimulation up to”. In: Cleave-land, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32–46. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084781

41. Schordan, M., Oppelstrup, T., Jefferson, D.R., Barnes, P.D., Jr.: Generation of reversible C++ code for optimistic parallel discrete event simulation. N. Gener. Comput. **36**, 257–280 (2018)

42. Siljak, H., Psara, K., Philippou, A.: Distributed antenna selection for massive MIMO using reversing Petri nets. IEEE Wirel. Commun. Lett. **8**, 1427–1430 (2019)

43. Vassor, M., Stefani, J.-B.: Checkpoint/rollback vs causally-consistent reversibility. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 286–303. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99498-7_20

44. Zheng, L., Myers, A.C.: Dynamic security labels and noninterference (extended abstract). In: Dimitrakos, T., Martinelli, F. (eds.) Formal Aspects in Security and Trust. IIFIP, vol. 173, pp. 27–40. Springer, Boston, MA (2005). https://doi.org/10.1007/0-387-24098-5_3