RIF: Reactive information flow labels

Abstract

Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.

Keywords

Reclassification piesewise noninterference type system RIF automaton

1. Introduction

Data is usually accompanied by restrictions about uses. Information flow control [50] has been employed to ensure those restrictions propagate from inputs to the outputs of operations. In Denning’s initial work [21] and in much that has followed – both for confidentiality and integrity – the set of restrictions assigned to the output of an operation is the union of the restrictions associated with its inputs. But by ignoring the operator and the values of inputs, that approach can be too conservative.

The most general formulation of flow-derived restrictions would assign restrictions to the output of an operation $op (x_{1}, x_{2}, \dots, x_{n})$ according to operator $op$ , its inputs $x_{1}, x_{2}, \dots, x_{n}$ , and the restrictions associated with those inputs. That output might warrant fewer restrictions, additional restrictions, or an incomparable set of restrictions than are associated with its inputs.

With an operation that computes the winner of an election, the inputs are votes and the output is the majority. Each input is secret to the principal casting that vote, whereas the output ought to be readable by any principal. So the output should be associated with fewer restrictions than the inputs.

A conference-management system matches papers to reviewers, where that matching is generated by a non-deterministic computation. The inputs – a list of reviewers and a list of submissions – can be read by the entire program committee, but conflicts of interest dictate that only a subset of the program committee learn which reviewers are assigned to any given paper. So, as with other aggregation problems [31], outputs are associated with more stringent restrictions than inputs.

Previous work on information flow control – declassification and erasure policies [16], information flow locks [10,11], typed declassification [24], expressions for declassification (for confidentiality) and endorsement (for integrity) [44,46], and capability-based mechanisms for downgrading security policies [35,49,56] – does not support arbitrary changes in restrictions linked with specific operations. Other approaches (e.g., [30,40,47,48,53]) allow such changes but only between two levels of labels (e.g., public and secret).

Reactive information flow (RIF) labels, which we introduce in §2, seek to address these limitations by allowing stronger, weaker, or incomparable restrictions to be associated with the output of an operation, as determined by the operator and the restrictions on inputs. Piecewise noninterference (PWNI) described in §4 then extends classical noninterference in a way that handles changes to restrictions that RIF labels support. Using terminology introduced by Sabelfeld and Sands [53], PWNI stipulates for programs that associate RIF labels with variables, what information undergoes changes of restrictions and where in the program code. A type system is given in §5 to support static enforcement of PWNI for certain classes of RIF labels. Examples of those classes include RIF automata in §3 and κ-labels in §6. In §7 we discuss how previous work relates to RIF labels and PWNI.

2. RIF labels

Restrictions. Restrictions are assumed to be elements of a join semilattice $⟨ R, ⊔_{R}, ⊑_{R} ⟩$ .1

¹
A partial order would suffice for the theory of RIF labels developed in this section. A join semilattice becomes useful for certain instantiations of RIF labels, as illustrated in §3 and §6.

For confidentiality, an element of R might identify which principals are allowed to read some value, either by enumerating that set of principals or by giving the name (e.g., public, secret, etc.) for such a set; for integrity, it might identify the set of principals allowed to write that value. But other kinds of restrictions also could be specified using elements in R – use-based privacy [9] is an example.

Relation $r ⊑_{R} r^{'}$ is satisfied if compliance with restrictions $r^{'} \in R$ implies compliance with restrictions $r \in R$ , so $r^{'}$ is at least as strong as r or, equivalently, r is at least as weak as $r^{'}$ . When elements of R denote sets of principals, then for confidentiality we would define $r ⊔_{R} r^{'}$ to be $r \cap r^{'}$ and define $r ⊑_{R} r^{'}$ to hold if and only if $r \supseteq r^{'}$ holds – if $r^{'}$ allows a principal to read then so does r, but r might also allow other principals to read, too. And, for integrity, we would define $r ⊔_{R} r^{'}$ to be $r \cup r^{'}$ and define $r ⊑_{R} r^{'}$ to hold if and only if $r \subseteq r^{'}$ holds.

Reclassifiers and RIF labels. A reclassifier abstracts how an operation changes the restrictions for an argument.2

The term reclassify is taken from Denning’s thesis [21] where it is used to describe an operation that changes the restrictions imposed on objects.

To associate reclassifiers with operations, we extend a language that defines ordinary expressions: variables and terms

op (E_{1}, \dots, E_{n})

, where

op

is an operator and each

E_{i}

is an ordinary expression. For ordinary expressions

E_{1}, \dots, E_{n}

\begin{matrix} (1) & {[op (E_{1}, \dots, E_{n})]}_{f_{1}, f_{2}, \dots, f_{n}} \end{matrix}

defines a reclassifying expression. It specifies that reclassifier

f_{i}

identifies how the restrictions associated with the value of ordinary expression

E_{i}

should be changed for constructing the restrictions associated with the value produced by

op (E_{1}, \dots, E_{n})

. Notation

{[op (E_{1}, \dots, E_{n})]}_{f_{}}

is used as a shorthand for

{[op (E_{1}, \dots, E_{n})]}_{f_{}, f_{}, \dots, f_{}}

, and we sometimes abbreviate

{[op (E_{1}, \dots, E_{n})]}_{f_{1}, f_{2}, \dots, f_{n}}

{[op (E_{1}, \dots, E_{n})]}_{\bar{f}}

or simply

{[E]}_{\bar{f}}

if the elided specifics are irrelevant. By convention, the identity reclassifier ϵ causes no changes to restrictions.

When reclassifying expressions are used to compute values, then sequences of reclassifiers offer abstract descriptions for the series of operations that have been applied to values as program execution proceeds. Such a sequence of reclassifiers then provides a basis for determining the set of restrictions associated with a computed value. For example, consider the following program. $\begin{matrix} (2) & w_{1} : = {[div (x_{1}, x_{2})]}_{f_{}}; y_{2} : = {[\mod (w_{1}, w_{2})]}_{{f_{}}^{'}}; z_{3} : = {[add (y_{1}, y_{2}, y_{3})]}_{{f_{}}^{″}} \end{matrix}$ Here, restrictions on the value stored in $z_{3}$ are derived from:

the restrictions on the value stored in $x_{1}$ and in $x_{2}$ , changed according to sequence $f_{} {f_{}}^{'} {f_{}}^{″}$ because each of these values flows to $w_{1}$ through $f_{}$ , then $w_{1}$ flows to $y_{2}$ through ${f_{}}^{'}$ , and finally $y_{2}$ flows to $z_{3}$ through ${f_{}}^{″}$ .

the restrictions on the value stored in $w_{2}$ , changed according to sequence ${f_{}}^{'} {f_{}}^{″}$ , and

the restrictions on the values stored in $y_{1}$ and $y_{3}$ , changed according to ${f_{}}^{″}$ .

A RIF label λ specifies a set of restrictions for an associated value v as well as for values derived by executing operations on v. Formally, a RIF label maps sequences of reclassifiers to elements of underlying join semilattice $⟨ R, ⊔_{R}, ⊑_{R} ⟩$ of restrictions. This mapping is specified for a set Λ of RIF labels by giving a set $F$ of reclassifiers along with two functions $R_{}$ and $T_{}$ .

$R_{}$ maps $λ \in Λ$ to the restriction $r \in R$ that λ currently imposes: $\begin{matrix} (3) & R_{} : Λ \to R \end{matrix}$

$T_{}$ maps $λ \in Λ$ and each reclassifier $f_{} \in F$ to a RIF label that should be associated with the value produced by an operation $f_{}$ abstracts: $\begin{matrix} (4) & T_{} : Λ \times F \to Λ \end{matrix}$

As an example, the restrictions associated with the value of a reclassifying expression (1) will incorporate restrictions

R_{} (T_{} (λ_{i}, f_{i}))

derived from RIF label

λ_{i}

being associated with the value of expression

E_{i}

. Note that RIF labels λ and

λ^{'}

might have

R_{} (λ) = R_{} (λ^{'})

and

R_{} (T_{} (λ, f_{})) \neq R_{} (T_{} (λ^{'}, f_{}))

– which makes having indirection between λ and

R_{} (λ)

useful.

$T_{}$ is extended to a finite sequence3

As is conventional, $F^{*}$ denotes the set of finite sequences of elements in $F$ .

F \in F^{*}

of reclassifiers in the usual way, with identity reclassifier ϵ considered an element of every set

F

of reclassifiers.

\begin{array}{l} (5) & T_{} (λ, ϵ) ≜ λ \\ (6) & T_{} (λ, F f_{}) ≜ T_{} (T_{} (λ, F), f_{}) \end{array}

Classes of RIF labels. A class of RIF labels can serve as the basis for a join semilattice $⟨ Λ, ⊔_{Λ}, ⊑_{Λ} ⟩$ , where the cardinality of Λ can be infinite. The join operator $⊔_{Λ}$ is used for combining RIF labels; the restrictiveness relation $⊑_{Λ}$ specifies whether one RIF label is at least as restrictive as another. We posit that Λ includes elements ⊥ and ⊤ such that for all $λ \in Λ$ : $⊥ ⊑_{Λ} λ$ and $λ ⊑_{Λ} ⊤$ hold.

Since, by definition, $λ ⊑_{Λ} λ ⊔_{Λ} λ^{'}$ and $λ^{'} ⊑_{Λ} λ ⊔_{Λ} λ^{'}$ hold in a join semilattice, a combination of RIF labels is at least as restrictive as any of its constituents. For the examples of RIF labels in this paper, $⊔_{Λ}$ and $⊔_{R}$ are related in a way that ensures restrictions imposed by $λ ⊔_{Λ} λ^{'}$ are the same as the combined restrictions imposed by individual RIF labels λ and $λ^{'}$ .4

⁴

Reasonable examples of RIF labels do exist where (7) does not hold.

\begin{matrix} (7) & R_{} (λ ⊔_{Λ} λ^{'}) = R_{} (λ) ⊔_{R} R_{} (λ^{'}) \end{matrix}

The definition of restrictiveness relation $⊑_{Λ}$ depends on partial order $⊑_{R}$ for set R of restrictions, $R_{}$ , and $T_{}$ : $\begin{matrix} (8) & λ ⊑_{Λ} λ^{'} ≜ (\forall F \in F^{*} : R_{} (T_{} (λ, F)) ⊑_{R} R_{} (T_{} (λ^{'}, F))) \end{matrix}$ This definition ensures that if $λ ⊑_{Λ} λ^{'}$ holds, then

current restrictions $R_{} (λ^{'})$ specified by $λ^{'}$ are at least as strong as what λ imposes because, by definition, $ϵ \in F$ and thus $ϵ \in F^{*}$ , $R_{} (T_{} (λ, ϵ)) = R_{} (λ)$ and $R_{} (T_{} (λ^{'}, ϵ)) = R_{} (λ^{'})$ hold, so (8) implies that $R_{} (λ) ⊑_{R} R_{} (λ^{'})$ , and

restrictions that $λ^{'}$ imposes for any derived value are at least as strong as what λ imposes – if v flows to w then there is a sequence $F \in F^{*}$ that v flows through, and (8) requires that $R_{} (T_{} (λ, F)) ⊑_{R} R_{} (T_{} (λ^{'}, F))$ hold.

The quantification over all sequences

F \in F^{*}

in (8) means that this definition for

λ ⊑_{Λ} λ^{'}

is conservative, since it imposes conditions for sequences

F

of reclassifiers that never arise in a program execution.

Fig. 1.

Terminology for reclassifications.

Definition (RIF Class).

A class of RIF labels is formed as follows: $\begin{matrix} ⟨ ⟨ R, ⊔_{R}, ⊑_{R} ⟩, ⟨ Λ, ⊔_{Λ}, ⊑_{Λ} ⟩, F, R_{}, T_{} ⟩ \end{matrix}$

The definition of a RIF class is silent about the existence of algorithms for computing $⊔_{Λ}$ or for deciding $⊑_{Λ}$ . We say that a RIF class is checkable if and only if:

There exists an algorithm for computing $λ ⊔_{Λ} λ^{'}$ for all $λ, λ^{'} \in Λ$ .

There exists a sound, if not complete, test for determining whether $λ ⊑_{Λ} λ^{'}$ holds for all $λ, λ^{'} \in Λ$ .

The type system we give in §5 is decidable if its RIF labels are from a checkable class.

Reclassifications. A reclassifier $f_{}$ triggers a reclassification in a RIF label λ, if $T_{} (λ, f_{}) \neq λ$ holds. In the literature, reclassification is categorized based on the restrictions that new and old labels impose – specifically, whether $R_{} (T_{} (λ, f_{}))$ is weaker than $R_{} (λ)$ . Figure 1 defines specialized terminology for this categorization, where $R_{} (λ)$ gives a set of principals that must be trusted not to divulge the value (for confidentiality) or not to have corrupted the value (for integrity). So, according to Fig. 1, reclassifier $f_{}$ triggers a declassification if the principals trusted not to divulge the value by the new label (i.e., $T_{} (λ, f_{})$ ) are a superset of those trusted by the old label (i.e., λ); if they are a subset, then $f_{}$ triggers a classification. Also, reclassifier $f_{}$ triggers an endorsement when the principals trusted not to have corrupted the value by the new label (i.e., $T_{} (λ, f_{})$ ) are a subset of those trusted by the old label (i.e., λ); if they are a superset, then $f_{}$ triggers a deprecation.

The approach in this paper, however, involves a finer-grained categorization of reclassifications. That categorization is based on how a new RIF label $T_{} (λ, f_{})$ is related to the old RIF label λ: When $T (λ, f_{}) ⊏_{Λ} λ$ holds then we say that $f_{}$ triggers a downgrade; when $T (λ, f_{}) ⋢_{Λ} λ$ holds then we say that $f_{}$ triggers an upgrade. And the reclassifying expressions that appear in a program in conjunction with the RIF labels that tag variables in these expressions, specify what information is being reclassified and where in the program. In particular, given a reclassifying expression ${[E]}_{\bar{f}}$ at a particular program point, if the RIF label of $E$ is different from the RIF label of ${[E]}_{\bar{f}}$ , then $\bar{f}$ triggers a reclassification: The what dimension of this reclassification is the current value of $E$ , and the where dimension is that particular program point (i.e., code locality is employed).

The RIF label for ordinary and reclassifying expressions are deduced as usual from the RIF labels of the variables that appear in those expressions. Starting from a fixed mapping Γ that associates a RIF label $Γ (x) \in Λ$ with each variable x, define: $\begin{array}{l} (9) & Γ (op (E_{1}, \dots, E_{n})) ≜ Γ (E_{1}) ⊔_{Λ} \dots ⊔_{Λ} Γ (E_{n}) \\ (10) & Γ ({[op (E_{1}, \dots, E_{n})]}_{f_{1}, \dots, f_{n}}) ≜ T_{} (Γ (E_{1}), f_{1}) ⊔_{Λ} \dots ⊔_{Λ} T_{} (Γ (E_{n}), f_{n}) \end{array}$ Thus, the RIF label associated with a reclassifying expression combines RIF labels obtained after the indicated transitions have been performed.

We give a concrete example of reclassification using program (2) and assuming that the following restrictiveness relation holds: $\begin{matrix} Γ ({[\mod (w_{1}, w_{2})]}_{{f_{}}^{'}}) ⊏_{Λ} Γ (\mod (w_{1}, w_{2})) \end{matrix}$ So reclassifier ${f_{}}^{'}$ triggers a downgrade. For the what dimension, the value to be downgraded is the result of applying $\mod$ to the values stored in $w_{1}$ and $w_{2}$ at program point “ $y_{2} : = {[\mod (w_{1}, w_{2})]}_{{f_{}}^{'}}$ ; $z_{3} : = {[add (y_{1}, y_{2}, y_{3})]}_{{f_{}}^{″}}$ ” – as opposed to the values stored in $w_{1}$ and $w_{2}$ at initialization. For the where dimension: the value of $\mod (w_{1}, w_{2})$ is downgraded at that program point – not earlier. A formal characterization for the security policy satisfied by a program that employs RIF labels and reclassifying expressions is given in §4.

3. RIF automata

Finite state automata provide the basis for a checkable class of RIF labels, called RIF automata, that have broad practical utility. This class of RIF labels is supported in the JRIF5

⁵
JRIF is a variant of the Jif security-typed programming language, which extends Java with support for information flow control.

programming language [34]. We built JRIF to gain practical experience with using RIF automata for specifying security policies and to understand the compiler modifications needed when a programming language that supports ordinary security label types is converted to use RIF automata. The privacy automata used in the Avanance language [9] for specifying use-based privacy are also instances of RIF automata.

Formalization of RIF automata. A finite state automaton can serve as a RIF label $λ_{α}$ by: (i) having the set of reclassifiers be the automaton’s input alphabet, and (ii) associating restrictions with each automaton state. Restrictions imposed by $λ_{α}$ are those associated with the automaton’s current state. Reclassifiers change the automaton’s current state. Thus they cause a (potentially) different set of restrictions to be imposed.

A set $Λ_{RA}$ comprising RIF automata is defined relative to some join semilattice of restrictions $⟨ R, ⊔_{R}, ⊑_{R} ⟩$ . Each RIF automaton $λ_{α} \in Λ_{RA}$ is described by a 5-tuple $\begin{matrix} (11) & λ_{α} ≜ ⟨ Q_{α}, F, δ_{α}, q_{α}, ρ_{α} ⟩ \end{matrix}$ where: $\begin{array}{l} Q_{α} is a finite set of automaton states \\ F is the finite set of reclassifiers \\ δ_{α} : Q_{α} \times F \to Q_{α} is a (deterministic) next-state transition function^{6} \\ q_{α} \in Q_{α} is the current state of the RIF automaton \\ ρ_{α} : Q_{α} \to R gives the restrictions associated with each automaton state \end{array}$

⁶

Closure $δ_{α}^{*} : Q_{α} \times F^{*} \to Q_{α}$ is obtained from $δ_{α}$ in the usual way: $δ_{α}^{*} (q, ϵ) ≜ q$ and $δ_{α}^{*} (q, F f) ≜ δ_{α} (δ_{α}^{*} (q, F), f)$ .

We require transition function $δ_{α}$ to be total, so any sequence of reclassifiers from $F$ causes a sequence of transitions. And for $F \in F^{*}$ we write $λ_{α} (F)$ to denote the automaton that results when $λ_{α}$ performs the transitions indicated by a sequence $F$ of reclassifiers. Automaton $λ_{α} (F)$ thus replaces current state $q_{α}$ of $λ_{α}$ with $δ_{α}^{*} (q_{α}, F)$ ; we define $λ_{α} (F)$ formally by: $\begin{array}{l} λ_{α} (F) ≜ λ_{α} [q_{α} \mapsto δ_{α}^{*} (q_{α}, F)] \\ where for q_{i} \in Q_{α} : λ_{α} [q_{α} \mapsto q_{i}] ≜ ⟨ Q_{α}, F, δ_{α}, q_{i}, ρ_{α} ⟩ \end{array}$

$R_{RA}$ and $T_{RA}$ are defined as expected. $\begin{array}{l} R_{RA} (λ_{α}) ≜ ρ_{α} (q_{α}) T_{RA} (λ_{α}, f) ≜ λ_{α} (f) \end{array}$ Instantiating definition (8) of $⊑_{Λ}$ using these definitions gets: $\begin{matrix} (12) & λ_{α} ⊑_{RA} λ_{α^{'}} ≜ (\forall F \in F^{*} : ρ_{α} (δ_{α}^{*} (q_{α}, F)) ⊑_{R} ρ_{α^{'}} (δ_{α^{'}}^{*} (q_{α^{'}}, F))) \end{matrix}$

A computable test for deciding $λ_{α} ⊑_{RA} λ_{α^{'}}$ is now given. It is based on constructing a restrictiveness product automaton $λ_{α} \otimes λ_{α^{'}}$ that is the product of RIF automata $λ_{α}$ and $λ_{α^{'}}$ but with unreachable automaton states eliminated. $\begin{array}{l} (13) & \begin{matrix} λ_{α} \otimes λ_{α^{'}} ≜ ⟨ Q_{α \otimes α^{'}}, F, δ_{α \otimes α^{'}}, ⟨ q_{α}, q_{α^{'}} ⟩, ρ_{α \otimes α^{'}} ⟩ \\ where Q_{α \otimes α^{'}} \subseteq Q_{α} \times Q_{α^{'}} \\ δ_{α \otimes α^{'}} (⟨ q_{}, q_{}^{'} ⟩, f) ≜ ⟨ δ_{α} (q_{}, f), δ_{α^{'}} (q_{}^{'}, f) ⟩ \\ ρ_{α \otimes α^{'}} (⟨ q_{,} q_{}^{'} ⟩) ≜ ⟨ ρ_{α} (q_{}), ρ_{α^{'}} (q_{}^{'}) ⟩ \\ (\forall q \in Q_{α \otimes α^{'}} : (\exists F_{q} \in F^{*} : δ_{α \otimes α^{'}}^{*} (⟨ q_{α}, q_{α^{'}} ⟩, F_{q}) = q)) \end{matrix} \end{array}$ Restrictiveness product automata are not RIF automata because the signature for $ρ_{α \otimes α^{'}}$ in $λ_{α} \otimes λ_{α^{'}}$ is $\begin{matrix} ρ_{α \otimes α^{'}} : Q_{α \otimes α^{'}} \to R \times R, \end{matrix}$ whereas a RIF automaton would have to associate a single element of R (rather than a pair of elements) with each automaton state.

Condition (13), which stipulates that all states in $Q_{α \otimes α^{'}}$ are reachable, is straightforward to check with a linear-time depth-first search of the state-transition graph for $δ_{α \otimes α^{'}}$ . And condition (13) implies that for any predicate $P (⟨ q, q^{'} ⟩)$ on states $⟨ q, q^{'} ⟩ \in Q_{α \otimes α^{'}}$ $\begin{matrix} (14) & (\forall ⟨ q, q^{'} ⟩ \in Q_{α \otimes α^{'}} : P (⟨ q, q^{'} ⟩)) = (\forall F \in F^{*} : P (δ_{α \otimes α^{'}}^{*} (⟨ q_{α}, q_{α^{'}} ⟩, F))) \end{matrix}$ holds. Therefore a decision procedure for $λ_{α} ⊑_{RA} λ_{α^{'}}$ need only check a predicate on the pair of restrictions associated with each state $⟨ q, q^{'} ⟩ \in Q_{α \otimes α^{'}}$ – namely that $r ⊑_{R} r^{'}$ holds if $ρ_{α \otimes α^{'}} (⟨ q, q^{'} ⟩) = ⟨ r, r^{'} ⟩$ . $\begin{array}{l} (15) & λ_{α} ⊑_{RA} λ_{α^{'}} = (\forall ⟨ q, q^{'} ⟩ \in Q_{α \otimes α^{'}} : ρ_{α} (q) ⊑_{R} ρ_{α^{'}} (q^{'})) \end{array}$ To prove that (15) is equivalent to definition (12) of $λ_{α} ⊑_{RA} λ_{α^{'}}$ , observe that $\begin{array}{l} (\forall ⟨ q, q^{'} ⟩ \in Q_{α \otimes α^{'}} : ρ_{α} (q) ⊑_{R} ρ_{α^{'}} (q^{'})) \\ = due to (14), with P (⟨ q, q^{'} ⟩) ≜ ρ_{α} (q) ⊑_{R} ρ_{α^{'}} (q^{'}) \\ (\forall F \in F^{*} : ρ_{α} (δ_{α}^{*} (q_{α}, F)) ⊑_{R} ρ_{α^{'}} (δ_{α^{'}}^{*} (q_{α^{'}}, F))) \end{array}$

The properties of $⊔_{RA}$ for RIF automata are satisfied by using a form of product construction that does yield a RIF automaton. $\begin{array}{l} λ_{α} ⊔_{RA} λ_{α^{'}} ≜ ⟨ Q_{α ⊔ α^{'}}, F, δ_{α ⊔ α^{'}}, ⟨ q_{α}, q_{α^{'}} ⟩, ρ_{α ⊔ α^{'}} ⟩ \\ where Q_{α ⊔ α^{'}} = Q_{α} \times Q_{α^{'}} \\ δ_{α ⊔ α^{'}} (⟨ q_{}, q_{}^{'} ⟩, f) ≜ ⟨ δ_{α} (q_{}, f), δ_{α^{'}} (q_{}^{'}, f) ⟩ \\ ρ_{α ⊔ α^{'}} (⟨ q_{}, q_{}^{'} ⟩) ≜ ρ_{α} (q_{}) ⊔_{R} ρ_{α^{'}} (q_{}^{'}) \end{array}$ Note that (7) relating $⊔_{R}$ and $⊔_{RA}$ is satisfied by this definition.

Finally, we prove in the Appendix A that $⟨ Λ_{RA,}, ⊑_{RA}, ⊔_{RA} ⟩$ is a join semilattice.

Fig. 2.

RIF automaton $λ_{voter (A)}$ for secret ballots.

Examples of RIF automata. A security policy we might associate with the ballot that each participant A casts in an election is: (i) only A may read the ballot’s value and (ii) anyone may read the majority value derived from all of the ballots cast. We formalize this security policy as a RIF automaton $λ_{voter (A)}$ , where $Prins$ is the set of principals eligible to learn the election outcome, the join semilattice of underlying restrictions is $⟨ 2^{Prins}, \cap, \supseteq ⟩$ , and set $F$ of reclassifiers includes $tally$ , which will be associated with calculating the election outcome.

Figure 2 gives a graphic depiction7

⁷

A conventional graphical representation for finite-state automata is used. Circles denote states of the automaton. Arrows between states are labeled with lists of reclassifiers, any of which can trigger the allowed transitions. We will write * to abbreviate the list of all reclassifiers and $\neg ℓ$ to denote a list of all reclassifiers not contained in list ℓ. The label inside each state q indicates associated restrictions $ρ_{α} (q)$ , and the grey-filled state indicates the current automaton state.

λ_{voter (A)}

; the formal definition is:

\begin{array}{l} λ_{voter (A)} ≜ ⟨ {q_{1}, q_{2}}, F, δ_{voter}, q_{1}, ρ_{voter (A)} ⟩ \\ where \\ δ_{voter} (q, f) ≜ \{\begin{matrix} q_{2} & if q = q_{1} \land f = tally \\ q & otherwise \end{matrix} \\ ρ_{voter (A)} (q) ≜ \{\begin{matrix} {A} & if q = q_{1} \\ Prins & if q = q_{2} \end{matrix} \end{array}

Restriction

ρ_{voter (A)}

defines which principals can read the value being labeled by

λ_{voter (A)}

the value may be read only by A if $λ_{voter (A)}$ is in state $q_{1}$ , because $ρ_{voter (A)} (q_{1}) = {A}$ , and

any value derived by using a $tally$ operation may be read by any principal, because the current state transitions to $q_{2}$ and $ρ_{voter (A)} (q_{2}) = Prins$ hold.

Thus, according to the terminology of Fig. 1,

tally

causes declassification.

A programmer would use reclassifying expression ${[maj (v_{A}, v_{B}, \dots, v_{Z})]}_{tally}$ to assert that computing the majority of votes in $v_{A}, v_{B}, \dots, v_{Z}$ implements the intended effect of a $tally$ operation. That derived value can be stored in a variable whose RIF label imposes no restriction on readers. Assignment $\begin{matrix} (16) & winner : = {[maj (v_{A}, v_{B}, \dots, v_{Z})]}_{tally} \end{matrix}$ has exactly that effect if the RIF automaton associated with each variable $v_{A}$ is $λ_{voter (A)}$ in state $q_{1}$ , and the RIF automaton associated with variable $winner$ is at least as restrictive as $\begin{matrix} λ_{voter (A)} (tally) ⊔_{RA} λ_{voter (B)} (tally) ⊔_{RA} \dots ⊔_{RA} λ_{voter (Z)} (tally) \end{matrix}$ which happens to be equivalent to $λ_{voter (x)} [q_{1} \mapsto q_{2}]$ for any $x \in {A, \dots, Z}$ .

Fig. 3.

RIF automaton of document excerpting.

A second example sketches RIF automata that enforce integrity policies for a document management system.8

⁸

This example is inspired by TruDocs [54].

Given is a set of original documents; these are trusted by all principals for all purposes. Operation

ext (D, parms)

derives a new document by excerpting from document D according to

parms

. Because “creative” excerpting can be used to generate a document that has different meaning from the original, cautious principals should hesitate to use such derived documents for certain purposes. Using the terminology of Fig. 1, excerpting causes deprecation.

One RIF automaton $λ_{D}$ for supporting such a policy might employ a join semilattice of underlying restrictions $⟨ {all, limited}, ⊔_{R}, ⊑_{R} ⟩$ , where $limited ⊑_{R} all$ holds; these restrictions indicate whether a document is trusted for all purposes or for limited purposes. $λ_{D}$ would employ a set $F_{Docs}$ of reclassifiers that includes $ext$ , which will correspond to excerpting operations. And $λ_{D}$ would have two automaton states, where: $\begin{matrix} ρ_{Docs} (q) ≜ \{\begin{matrix} all & if q = q_{1} \\ limited & if q = q_{2} \end{matrix} \end{matrix}$ Figure 3 gives a graphic depiction for a RIF automaton $λ_{D}$ associated with an original document D; the formal definition of $λ_{D}$ is: $\begin{array}{l} λ_{D} ≜ ⟨ {q_{1}, q_{2}}, F_{Docs}, δ_{Docs}, q_{1}, ρ_{Docs} ⟩ \\ where \\ δ_{Docs} (q, f) ≜ \{\begin{matrix} q_{2} & if q = q_{1} \land f = ext \\ q & otherwise \end{matrix} \end{array}$ RIF automaton $λ_{D} [q_{1} \mapsto q_{2}]$ would be associated with any document produced by excerpting from D.

Some applications might require a more refined basis for deciding whether a document should be trusted for a specific purpose. One obvious basis for making such trust assessments is the set of principals participating in the document’s derivation. A RIF automaton can specify such policies. There would be an automaton state $q_{S}$ for each set S of principals corresponding to a subset of $Prins$ . And restrictions being associated with an automaton state $q_{S}$ would depend on members of S. So the join semilattice of underlying restrictions is $⟨ 2^{Prins}, \cup, \subseteq ⟩$ . Transitions are facilitated by having a set $F_{Doc}$ of reclassifiers contain an element ${ext}_{p}$ for each principal p that invokes an excerpting operation. Here is the formal definition of an automaton $λ_{D}$ that is associated with a document D that some principal $W \in Prins$ has written: $\begin{array}{l} λ_{D} ≜ ⟨ Q_{Prins}, F_{Doc}, δ_{Doc}, q_{{W}}, ρ_{Doc} ⟩ \\ where \\ Q_{Prins} ≜ {q_{S} | S \in 2^{Prins}} \\ δ_{Doc} (q_{S}, {exc}_{p}) ≜ q_{S \cup {p}} \\ ρ_{Doc} (q_{S}) ≜ S \end{array}$

4. A security policy for RIF labels

Our security policy for programs that use RIF labels is obtained by extending termination-insensitive noninterference (TINI) [52]. TINI applies to programs comprising deterministic commands, so execution of a command $C_{1}$ that is started in a memory $M_{1}$ and terminates in a memory $M_{N}$ can be described by giving a finite trace $\begin{matrix} (17) & ⟨ C_{1}, M_{1} ⟩ \to ⟨ C_{2}, M_{2} ⟩ \to \dots \to ⟨ ∙, M_{N} ⟩ \end{matrix}$ where each state $⟨ C_{i}, M_{i} ⟩$ gives a command $C_{i}$ and a memory $M_{i}$ . We write ∙ in the final state of a trace to signify further execution is not possible, but ∙ is not considered a command. Thus the trace for a terminating command $C$ includes at least two states: one state having command $C$ followed by one having ∙.

Memories are represented by functions that map variables x appearing in any command to values $M (x)$ . These functions are then extended as usual for mapping ordinary expressions and reclassifying expressions. $\begin{array}{l} M (op (E_{1}, \dots, E_{n})) ≜ op (M (E_{1}), \dots, M (E_{n})) \\ M ({[E]}_{f_{1}, f_{2}, \dots, f_{n}}) ≜ M (E) \end{array}$

An operational semantics for command execution can be given by a partial function Υ, where $Υ (C, M)$ returns the finite trace corresponding to an execution of $C$ that terminates when started in memory $M$ , and $Υ (C, M)$ is undefined if that execution does not terminate.

4.1. Observations as a threat model

A mapping Γ, which associates variables with RIF labels, induces equivalence classes of memories that agree on the values in variables allowed to flow to $λ \in Λ$ : $\begin{matrix} M =_{λ} M^{'} ≜ dom (M) = dom (M^{'}) \land (\forall x \in dom (M) : Γ (x) ⊑_{Λ} λ \Rightarrow M (x) = M^{'} (x)) \end{matrix}$ where $dom (M)$ is the domain of a memory $M$ .

Our threat model is intended for analyzing systems in which principals are co-resident and able to detect changes (subject to restrictions defined by RIF labels) being made to shared memory or other resources. We formalize this threat model relative to λ by constructing an observation $\begin{matrix} M_{i + 1} ⊖_{λ} M_{i} ≜ {⟨ x, M_{i + 1} (x) ⟩ | M_{i} (x) \neq M_{i + 1} (x) \land Γ (x) ⊑_{Λ} λ} \end{matrix}$ for each transition $⟨ C_{i}, M_{i} ⟩ \to ⟨ C_{i + 1}, M_{i + 1} ⟩$ that occurs. So observation $M_{i + 1} ⊖_{λ} M_{i}$ gives the new value for each variable that was (i) changed by the transition and (ii) has a RIF label at most λ. It is easy to show: $\begin{array}{l} M =_{λ} M^{'} \Rightarrow (M^{'} ⊖_{λ} M = \emptyset) \\ λ ⊑_{Λ} λ^{'} \Rightarrow (M^{'} ⊖_{λ} M) \subseteq (M^{'} ⊖_{λ^{'}} M) \end{array}$

For a RIF label λ, program execution described by a trace τ results in a sequence9

⁹
A formal definition of $τ |_{λ}$ is thus given by the following, where ⇁ is used to delimit observations in the resulting sequence. $\begin{matrix} τ |_{λ} ≜ \{\begin{matrix} ϵ & if τ = ϵ or τ = ⟨ C, M ⟩ \\ ϵ & if τ = ⟨ C, M ⟩ \to ⟨ C^{'}, M^{'} ⟩ \land M^{'} ⊖_{λ} M = \emptyset \\ M^{'} ⊖_{λ} M & if τ = ⟨ C, M ⟩ \to ⟨ C^{'}, M^{'} ⟩ \land M^{'} ⊖_{λ} M \neq \emptyset \\ (⟨ C^{'}, M^{'} ⟩ \to τ^{'}) |_{λ} & if τ = ⟨ C, M ⟩ \to ⟨ C^{'}, M^{'} ⟩ \to τ^{'} \land M^{'} ⊖_{λ} M = \emptyset \\ M^{'} ⊖_{λ} M ⇁ (⟨ C^{'}, M^{'} ⟩ \to τ^{'}) |_{λ} & if τ = ⟨ C, M ⟩ \to ⟨ C^{'}, M^{'} ⟩ \to τ^{'} \land M^{'} ⊖_{λ} M \neq \emptyset \end{matrix} \end{matrix}$

τ |_{λ}

of non-empty observations that are derived from the successive transitions in τ, and it induces an equivalence relation on traces

\begin{matrix} τ =_{λ} τ^{'} ≜ τ |_{λ} = τ^{'} |_{λ} . \end{matrix}

Sequences $τ |_{λ}$ of observations are the basis for our threat model. Each principal p is assigned a set $R_{} (p)$ of restrictions. The threat model stipulates that a principal p sees changes to any variable x satisfying $R_{} (Γ (x)) ⊑_{R} R_{} (p)$ . Thus, principal p sees those sequences $τ |_{λ}$ of observations where $R_{} (λ) ⊑_{R} R_{} (p)$ holds.

4.2. Piecewise noninterference

In the absence of reclassifications, an illicit λ-flow is witnessed when executing a command in states having different values of a variable with RIF label $λ^{'}$ satisfying $λ^{'} ⋢_{Λ} λ$ results in differences in updates to any variable with RIF label λ or less restrictive. TINI prohibits illicit λ-flows for any join semilattice. To formalize an extension to TINI for accommodating reclassification under our threat model, we require some notation. For τ a non-empty finite trace or subtrace, $\begin{matrix} ⟨ C_{1}, M_{1} ⟩ \to ⟨ C_{2}, M_{2} ⟩ \to \dots \to ⟨ C_{N}, M_{N} ⟩ \end{matrix}$ and indices i and j satisfying $1 ⩽ i ⩽ j ⩽ N$ , define $\begin{matrix} τ [i . .] ≜ ⟨ C_{i}, M_{i} ⟩ \to \dots \to ⟨ C_{N}, M_{N} ⟩ & τ [i] . C ≜ C_{i} \\ τ [i . . j] ≜ ⟨ C_{i}, M_{i} ⟩ \to \dots \to ⟨ C_{j}, M_{j} ⟩ & τ [i] . M ≜ M_{i} \\ τ [i] ≜ ⟨ C_{i}, M_{i} ⟩ & | τ | ≜ N \end{matrix}$ In addition, we write $τ . C$ as an abbreviation for $τ [1] . C$ and write $τ . M$ for $τ [1] . M$ . It is convenient to define $τ [i . .]$ , $τ [i . . j]$ , $τ [i]$ , $τ [i] . C$ , and $τ [i] . M$ as equivalent to ϵ when $1 ⩽ i ⩽ j ⩽ N$ does not hold.

We start by formalizing prohibition of illicit λ-flows for commands $\hat{C}$ that do not contain reclassifying expressions. By definition, an illicit λ-flow is not present if executing $\hat{C}$ in memories $M$ and $M^{'}$ satisfying $M =_{λ} M^{'}$ does not result in different updates to a variable that has a RIF label λ or less restrictive. $\begin{matrix} (18) & (\forall λ, M, M^{'}, τ, τ^{'} : τ = Υ (\hat{C}, M) \land τ^{'} = Υ (\hat{C}, M^{'}) \Rightarrow NI (λ, τ, τ^{'})) \end{matrix}$ where $\begin{matrix} NI (λ, τ, τ^{'}) ≜ τ . M =_{λ} τ^{'} . M \Rightarrow τ =_{λ} τ^{'} . \end{matrix}$ When $NI (λ, τ, τ^{'})$ is $false$ then τ and $τ^{'}$ exhibit the illicit λ-flow.

Reclassification. Each transition $⟨ C_{i}, M_{i} ⟩ \to ⟨ C_{i + 1}, M_{i + 1} ⟩$ in a trace involves evaluating some (possibly empty) set of expressions. The operational semantics of commands determines what those expressions are and how their values are computed. We posit that the operational semantics for each command $C_{i}$ also includes a function $Δ (C_{i})$ that gives the set of reclassifying expressions that command $C_{i}$ evaluates as part of its first transition.

For example, with a simple imperative programming language and ordinary expressions $E$ and $E^{'}$ we might expect to have $\begin{array}{l} (19) & Δ (x : = E) = \emptyset \\ (20) & Δ (x : = {[E]}_{\bar{f}}) = {{[E]}_{\bar{f}}} \\ (21) & Δ (if {[E]}_{\bar{f}} then x : = {[E^{'}]}_{\bar{f}}) = {{[E]}_{\bar{f}}} \end{array}$ if we are assuming that assignments are executed as a single transition and that an if statement involves a first transition to evaluate its Boolean guard followed by other transitions for the then (or else) parts.

Handling downgrades. A reclassifying expression ${[E]}_{\bar{f}}$ is considered to perform a λ-downgrade if $Γ ({[E]}_{\bar{f}}) ⊑_{Λ} λ$ and $Γ (E) ⋢_{Λ} λ$ hold. The set of expressions that satisfy the definition of a λ-downgrade and are evaluated by $C_{i}$ to make its transition is given by: $\begin{matrix} Δ_{}^{-} (λ, C_{i}) ≜ {E | {[E]}_{\bar{f}} \in Δ (C_{i}) \land Γ ({[E]}_{\bar{f}}) ⊑_{Λ} λ \land Γ (E) ⋢_{Λ} λ} \end{matrix}$ To define our security policy for programs $\hat{C}$ independent of specific programming constructs, we posit that the language semantics includes a function10

¹⁰
The $\hat{C}$ subscript in $Δ_{\hat{C}}^{-} (λ, C_{i})$ enables this function to depend on an enclosing program $\hat{C}$ and/or the position of $C_{i}$ within $\hat{C}$ . For example, the language semantics might omit $E$ from $Δ_{\hat{C}}^{-} (λ, x : = {[E]}_{\bar{f}})$ if that assignment appears in the scope of an if having a Boolean guard $E^{'}$ , where $Γ (E^{'}) ⋢_{Λ} Γ (x)$ holds.

Δ_{\hat{C}}^{-} (λ, C_{i})

that satisfies:

\begin{matrix} (22) & Δ_{\hat{C}}^{-} (λ, C_{i}) \subseteq Δ_{}^{-} (λ, C_{i}) \end{matrix}

E \in Δ_{\hat{C}}^{-} (λ, C_{i})

holds, then

C_{i}

is the reference point11

¹¹

See [41] for a thorough study of reference points for declassification.

for the corresponding λ-downgrade

{[E]}_{\bar{f}}

. The reference point signifies where in program

\hat{C}

this λ-downgrade is performed and what information is being λ-downgraded – the evaluation of

E

at that program point

C_{i}

Notice that, by definition, assigning the value of an expression in $Δ_{\hat{C}}^{-} (λ, C_{i})$ to a variable having RIF label λ does not constitute an illicit λ-flow. So $Δ_{\hat{C}}^{-} (λ, C_{i})$ characterizes illicit λ-flows that have been eliminated by fiat. Trade-offs associated with selecting the content of $Δ_{\hat{C}}^{-} (λ, C_{i})$ are discussed at the end of this section.

A generalization of (18) suffices to accommodate λ-downgrades that occur in the first transition of a trace that results from executing command $\hat{C}$ . $NI (λ, τ, τ^{'})$ was defined above in terms of updates to any variable x satisfying $Γ (x) ⊑_{Λ} λ$ . But differences in updates to x that arise when expressions in $Δ_{\hat{C}}^{-} (λ, \hat{C})$ have different values are, by definition, not considered illicit λ-flows. Therefore, initial memory pairs $M$ and $M^{'}$ that cause expressions in $Δ_{\hat{C}}^{-} (λ, \hat{C})$ to have different values should be ignored in checking for indistinguishable observations [51]: $\begin{matrix} (23) & (\forall λ, M, M^{'}, τ, τ^{'} : τ = Υ (\hat{C}, M) \land τ^{'} = Υ (\hat{C}, M^{'}) \Rightarrow dNI (λ, τ, τ^{'})) \end{matrix}$ where $\begin{matrix} dNI (λ, τ, τ^{'}) ≜ (\forall E \in Δ_{\hat{C}}^{-} (λ, τ . C) : τ . M (E) = τ^{'} . M (E)) \Rightarrow NI (λ, τ, τ^{'}) \end{matrix}$ By construction in (23), $τ . C = \hat{C}$ and $τ^{'} . C = \hat{C}$ hold. Therefore $τ . C = τ^{'} . C$ and $\begin{matrix} (24) & Δ_{\hat{C}}^{-} (λ, τ . C) = Δ_{\hat{C}}^{-} (λ, τ^{'} . C) \end{matrix}$ hold too. Thus, ignoring downgraded expressions in the first transition of trace τ (i.e., elements of $Δ_{\hat{C}}^{-} (λ, τ . C)$ ), $dNI (λ, τ, τ^{'})$ is also ignoring downgraded expressions in the first transition of trace $τ^{'}$ (i.e., elements of $Δ_{\hat{C}}^{-} (λ, τ^{'} . C)$ ).

To handle traces that perform λ-downgrades after the first transition in $\hat{C}$ , we partition traces into consecutive subtraces starting with transitions that are λ-downgrades. These subtraces are called λ-pieces. To formalize, we introduce operators and . Subtrace is the initial λ-piece of trace τ and subtrace is the rest. Thus, and satisfy the following two properties, for traces and subtraces τ satisfying $2 ⩽ | τ |$ .

Trace τ splits at a λ-downgrade into and :

There is no λ-downgrade after the first transition within λ-piece :

Here is a schematic representation of

and

Notice that by repeatedly isolating the first λ-piece of the remainder, a trace τ is partitioned into consecutive λ-pieces.

Two λ-pieces and are witnesses of an illicit λ-flow if executing the same command in memories $M$ and $M^{'}$ that satisfy $M =_{λ} M^{'}$ and agree on values of expressions that have already been λ-downgraded, leads to having (i) different commands in their last states, and/or (ii) different updates to a variable x where $Γ (x) ⊑_{Λ} λ$ holds. This is because (i) implies that the next λ-downgrades that are reached by these two λ-pieces are not found at the same program point. So, the reference point of these λ-downgrades is being compromised since it depends on information that is not allowed to flow to λ. When (ii) occurs, updates to x have been compromised because they are influenced by information that is not allowed to flow to λ. In sum, (i) and (ii) expose compromises of what is allowed to flow to λ and where in the program.

In this paper, we avoid these compromises to (i) and (ii) by rejecting certain pairs of λ-pieces and :

By iterating through successive corresponding λ-pieces in two traces τ and $τ^{'}$ , the following formula uses the approach embodied by (27) to identify λ-pieces that evidence an illicit λ-flow and thus provides the formal guarantee associated with downgrades.

Definition (

dpNI

Notice, if traces τ and $τ^{'}$ each are a single λ-piece (i.e., and for all λ) then $dpNI (λ, τ, τ^{'})$ is equivalent to (27), since in the consequent of (28) would be $dpNI (λ, ϵ, ϵ)$ , which trivially holds.

A characterization similar to (23) now handles downgrades that appear anywhere in traces that result from executing a command $C$ . $\begin{matrix} (29) & (\forall λ, M, M^{'}, τ, τ^{'} : τ = Υ (C, M) \land τ^{'} = Υ (C, M^{'}) \Rightarrow dpNI (λ, τ, τ^{'})) \end{matrix}$

Downgrade examples. Some example programs illustrate nuances of (29). These programs use RIF labels $Λ_{LH} ≜ {L, H}$ with $L ⊏_{Λ} H$ and reclassifiers $F ≜ {↓, ↑}$ satisfying $T_{} (H, ↓) ≜ L$ and $T_{} (L, ↑) ≜ H$ . Assume that $Γ (low) = Γ (lo w^{'}) = L$ and $Γ (high) = Γ (hig h^{'}) = H$ .

The first example program assigns in $C_{3}$ a value with RIF label $H$ to a variable with RIF label $L$ without use of a reclassifying expression and, thus, would seem to exhibit an illicit $L$ -flow. $\begin{matrix} (30) & \begin{matrix} C_{1} : & low : = {[op (high)]}_{↓}; \\ C_{2} : & {low}^{'} : = {[op (hig h^{'})]}_{↓}; \\ C_{3} : & low : = op (high) + 1 \end{matrix} \end{matrix}$ Traces for program (30) comprise two $L$ -pieces.12

¹²
Each trace is also a single $H$ -piece. For that case, $dpNI (H, τ, τ^{'})$ holds because $τ . M =_{H} τ^{'} . M$ is equivalent to $τ . M = τ^{'} . M$ . The same applies to example programs (31) and (32) to come.

One

L

-piece starts with command

C_{1}

, and the other

L

-piece starts with command

C_{2}

(and includes

C_{3}

), due to the following.

\begin{array}{l} Δ_{(30)}^{-} (L, C_{1}) = {op (high)} Δ_{(30)}^{-} (L, C_{2}) = {op (hig h^{'})} Δ_{(30)}^{-} (L, C_{3}) = \emptyset . \end{array}

Checking, we find (29) is satisfied despite our earlier premonition about

C_{3}

. A close look shows why the flow to

low

in assignment

C_{3}

actually ought to be allowed, as characterization (29) does:

C_{3}

is assigning an

L

-downgraded value, since the value of

op (high)

in the right hand side of

C_{3}

was an

L

-downgraded value in

C_{1}

and has not been changed since and constant 1 imposes no additional restrictions.

Program (30) highlights a difference in how downgrades are treated by PWNI as compared with proposals using memory-reset (e.g., [13]). Under PWNI, a downgraded value remains so for the remainder of the trace; with memory-reset, a downgraded value remains so only until the next reclassification operation. So, program (30) would be considered to exhibit a leak according to the memory-reset approach. Gradual release [3], which does not rely on memory-reset, deems program (30) secure, like PWNI does.

A second example program changes in $C_{2}$ the value in $high$ after the $L$ -downgrade in $C_{1}$ . $\begin{matrix} (31) & \begin{matrix} C_{1} : & low : = {[op (high)]}_{↓}; \\ C_{2} : & high : = hig h^{'}; \\ C_{3} : & low : = op (high) + 1 \end{matrix} \end{matrix}$ Traces for (31) comprise a single $L$ -piece that starts with command $C_{1}$ because: $\begin{array}{l} Δ_{(31)}^{-} (L, C_{1}) = {op (high)} Δ_{(31)}^{-} (L, C_{2}) = \emptyset Δ_{(31)}^{-} (L, C_{3}) = \emptyset \end{array}$ Program (31) does not satisfy (29), because traces τ and $τ^{'}$ exist that generate observations that are not (but should be) indistinguishable. This is because there exist memories $M$ and $M^{'}$ satisfying $M =_{L} M^{'}$ and $M (hig h^{'}) \neq M^{'} (hig h^{'})$ . When alternative executions of $C_{1}$ are started in these two memories, $C_{3}$ generates different updates to $low$ . And having (29) not satisfied for this program is what we should desire – the value in $high$ when $C_{3}$ executes is not the value that was $L$ -downgraded, so in program (31) a value with RIF label $H$ that has not been $L$ -downgraded is being used to update a variable with RIF label $L$ .

We also have examined $dpNI$ with respect to downgrades for the examples used by Askarov and Sabelfeld [4] when discussing localized delimited release. Both $dpNI$ and localized delimited release yield the same judgments for these examples, although in general the two policies are incomparable.

A final program illustrates the role of conjunct in the consequent of $dpNI (λ, τ, τ^{'})$ . $\begin{matrix} (32) & \begin{matrix} C_{1} : if hig h^{'} > 0 then & C_{2} : high : = 3 \\ C_{3} : low : = {[high + 2]}_{↓} \\ else & C_{4} : high : = 4 \\ C_{5} : low : = {[high mod 2]}_{↓} \end{matrix} \end{matrix}$ Consider traces $τ = Υ (C_{1}, M)$ and $τ^{'} = Υ (C_{1}, M^{'})$ , where the following hold: $M =_{L} M^{'}$ , $M (hig h^{'} > 0) = true$ , and $M^{'} (hig h^{'} > 0) = false$ . Trace τ comprises a first $L$ -piece that starts with $C_{1}$ (and includes $C_{2}$ ), followed by a second $L$ -piece that starts with $C_{3}$ ; trace $τ^{'}$ has a first $L$ -piece that starts with $C_{1}$ (and includes $C_{4}$ ), followed by a second $L$ -piece that starts with $C_{5}$ : $\begin{array}{l} τ = \underset{L -piece}{\underset{︸}{}} ⟨ C_{1}, M ⟩ \to ⟨ C_{2}, M_{2} ⟩ \to \overset{L -piece}{\overset{︷}{⟨ C_{3}, M_{3} ⟩ \to ⟨ ∙, M_{t} ⟩}} \\ τ^{'} = \underset{L -piece}{\underset{︸}{}} ⟨ C_{1}, M^{'} ⟩ \to ⟨ C_{4}, M_{4} ⟩ \to \overset{L -piece}{\overset{︷}{⟨ C_{5}, M_{5} ⟩ \to ⟨ ∙, M_{t^{'}} ⟩}} \end{array}$

Program (32) does not satisfy (29) because both and hold, so conjunct in the consequent of $dpNI (L, τ, τ^{'})$ does not hold. And having (29) not satisfied is what we should desire, because the choice of $C_{3}$ or $C_{5}$ leaks information about the value of $hig h^{'}$ to $low$ .

Instead of command equality (i.e., ), we could have extended the bisimulation used in [4] to handle downgrades of arbitrary expressions during execution. However, with this bisimulation, we would risk accepting insecure programs. This is because this bisimulation does not seem to set intermediate reference points for the downgrades. For example, consider program (32), which is insecure. A bisimulation that supports downgrades with reference points on intermediate states would accept the program as secure. The case to consider concerns the execution steps $⟨ C_{3}, M_{3} ⟩ \to ⟨ ∙, M_{t} ⟩$ and $⟨ C_{5}, M_{5} ⟩ \to ⟨ ∙, M_{t^{'}} ⟩$ , where $M_{3} =_{L} M_{5}$ . Adapting the bisimulation definition in [4] to support downgrades with reference points on intermediate states, these two execution steps constitute a bisimulation if

$M_{3} ({[high + 2]}_{↓}) = M_{5} ({[high + 2]}_{↓})$ iff $M_{3} ({[high mod 2]}_{↓}) = M_{5} ({[high mod 2]}_{↓})$ , and

if $M_{3} ({[high + 2]}_{↓}) = M_{5} ({[high + 2]}_{↓})$ , then $M_{t} =_{L} M_{t^{'}}$ and states $⟨ ∙, M_{t} ⟩$ , $⟨ ∙, M_{t^{'}} ⟩$ are bisimilar.

Condition (i) holds because, for any such reachable memories

M_{3}

and

M_{5}

, both equalities are false. Because these equalities are false, condition (ii) is vacuously true. So these execution steps are (vacuously) bisimulations, and thus this insecure program is accepted as secure. Another form of bisimulation might fare better, but we have not found one.

Handling upgrades. A reclassifying expression ${[E]}_{\bar{f}}$ is considered to perform a λ-upgrade if $Γ (E) ⊑_{Λ} λ$ and $Γ ({[E]}_{\bar{f}}) ⋢_{Λ} λ$ hold. Characterization (29) does not detect illicit λ-flows caused by λ-upgrades. Consider, for example, a program comprising assignment $\begin{matrix} (33) & low : = {[{low}^{'}]}_{↑} \end{matrix}$ that uses RIF labels from $Λ_{LH}$ . Assuming $Γ (low) = L$ and $Γ ({low}^{'}) = L$ hold, this program satisfies (29). Yet the program exhibits an illicit $L$ -flow: differences in the initial value of an $L$ -upgraded expression ( ${[lo w^{'}]}_{↑}$ ) with RIF label $H$ result in differences in updates to a variable ( $low$ ) with RIF label $L$ where $Γ ({[{low}^{'}]}_{↑}) ⋢_{Λ} Γ (low)$ holds.

In checking for evidence of illicit λ-flows, (29) compares traces τ and $τ^{'}$ that differ in initial values of variables whose RIF labels $λ^{'}$ satisfy $λ^{'} ⋢_{Λ} λ$ . That set of comparisons covers some expressions whose RIF labels $λ^{'}$ satisfy $λ^{'} ⋢_{Λ} λ$ but it does not cover all expressions – it ignores expressions that involve λ-upgrades.

A programming language that supports RIF labels will provide syntax that allows programmers to specify λ-upgrades by using reclassifying expressions. To be independent of language constructs, we posit that the language semantics includes a function $Δ_{\hat{C}}^{+} (λ, C_{i})$ that satisfies: $\begin{matrix} (34) & Δ_{\hat{C}}^{+} (λ, C_{i}) \supseteq {E | {[E]}_{\bar{f}} \in Δ (C_{i}) \land Γ ({[E]}_{\bar{f}}) ⋢_{Λ} λ \land Γ (E) ⊑_{Λ} λ} \end{matrix}$ So $Δ_{\hat{C}}^{+} (λ, C_{i})$ contains all expressions that satisfy the definition of a λ-upgrade and are evaluated by $C_{i}$ (within $\hat{C}$ ) to make its transition.

Since (29) correctly identifies illicit λ-flows from variables x for which $Γ (x) ⋢_{Λ} λ$ holds, we transform λ-upgraded expressions to such variables as a way to identify illicit λ-flows for λ-upgraded expressions. Define translation $T (λ, \hat{C})$ to be the command that results from, in every subcommand $C_{i}$ of $\hat{C}$ , substituting an expression $next (h_{E})$ for every expression ${[E]}_{\bar{f}} \in Δ (C_{i})$ where $E \in Δ_{\hat{C}}^{+} (λ, C_{i})$ and $Γ (next (h_{E})) = Γ ({[E]}_{\bar{f}})$ hold.13

¹³

See (36) and (37) below for an example of the translation.

Here,

h_{E}

is a fresh variable that stores a list of values that

E

could assume, and successive evaluations of

next (h_{E})

return successive elements of that list. If a program

\hat{C}

exhibits an illicit λ-flow from a λ-upgraded expression

E

then, by construction,

T (λ, \hat{C})

exhibits an illicit λ-flow from

next (h_{E})

. Moreover, because

T (λ, \hat{C})

contains no λ-upgraded expressions, it exhibits no illicit λ-flows from upgraded λ-expressions per se. That means we can use (29) to check for illicit λ-flows in

\hat{C}

by checking

T (λ, \hat{C})

for illicit λ-flows. A formal definition of

T (λ, \hat{C})

can be found in the Appendix B.

The resulting characterization of piecewise noninterference (PWNI) for a program $\hat{C}$ employs $dpNI (λ, τ, τ^{'})$ – defined in (28) – by extending (29) to handle λ-flows from λ-upgraded expressions.

Definition (Piecewise Noninterference).

$\begin{matrix} (35) & \begin{matrix} PWNI (\hat{C}) \\ ≜ (\forall λ, M, M^{'}, τ, τ^{'} : τ = Υ (T (λ, \hat{C}), M) \land τ^{'} = Υ (T (λ, \hat{C}), M^{'}) \\ \Rightarrow dpNI (λ, τ, τ^{'})) \end{matrix} \end{matrix}$

The election example and the conference-management example of §1 both satisfy this definition when coded in a straightforward manner.

Upgrade examples. $PWNI (\hat{C})$ as defined in (35) considers executions of a translation in which $L$ -upgraded expressions $E$ are replaced by different fresh variables $h_{E}$ . So, equivalent expressions within an execution and in different executions of the original program may take different values in executions of the translation. Here is an illustration, where RIF labels are from $Λ_{LH}$ . $\begin{matrix} (36) & \begin{matrix} C_{1} : if {[low = low]}_{↑} then & C_{2} : low : = 1 else C_{3} : low : = 2 \end{matrix} \end{matrix}$ $PWNI (C_{1})$ creates translated program $T (λ, C_{1})$ , $\begin{matrix} (37) & \begin{matrix} C_{1} : if next (h_{low = low}) then & C_{2} : low : = 1 else C_{3} : low : = 2 \end{matrix} \end{matrix}$ where $Γ (next (h_{low = low})) = H$ holds. Boolean guard ${[low = low]}_{↑}$ in (36) is always $true$ , so execution of (36) produces no traces in which $C_{3}$ executes. In translated program (37), Boolean guard $next (h_{low = low})$ takes values $true$ and $false$ , so there are traces of (37) where $C_{3}$ executes as well as traces where $C_{2}$ executes. Thus, $PWNI (C_{1})$ is not satisfied for (37) due to the illicit $L$ -flow from upgraded expression ${[low = low]}_{↑}$ to $low$ , even though in program (36) upgraded expression ${[low = low]}_{↑}$ never actually flows to $low$ . One way to circumvent this conservatism is to restrict the set of values that a fresh variable can take. In particular, that set can be limited to containing values that the upgrading expression can take during program execution.

Assessing PWNI. Whether a program satisfies $PWNI (\hat{C})$ depends, in part, on flexibility that (22) allows in the definition of $Δ_{\hat{C}}^{-} (λ, C_{i})$ and that (34) allows in the definition of $Δ_{\hat{C}}^{+} (λ, C_{i})$ .

$Δ_{\hat{C}}^{-} (λ, C_{i})$ is constrained only by (22), so $Δ_{\hat{C}}^{-} (λ, C_{i})$ may omit expressions that cause λ-downgrades. With fewer expressions in $Δ_{\hat{C}}^{-} (λ, C_{i})$ :

There are more pairs of memories from which execution results in a pair of λ-pieces whose subtraces and must satisfy (27). So the omissions may cause $PWNI (\hat{C})$ to reject programs that do not actually exhibit illicit λ-flows.

Fewer λ-pieces need to be checked by evaluating $dpNI (λ, τ, τ^{'})$ . So the omissions may cause $PWNI (\hat{C})$ to accept more programs that do not exhibit illicit λ-flows.

$Δ_{\hat{C}}^{+} (λ, C_{i})$ is constrained only by (34), so $Δ_{\hat{C}}^{+} (λ, C_{i})$ may include expressions that do not cause λ-upgrades. The additional expressions $E$ are replaced in each $C_{i}$ by expressions involving list $h_{E}$ . That means there could be more pairs of memories (i.e., those that differ in $h_{E}$ ) from which execution results in a pair of λ-pieces whose subtraces and must satisfy (27). So the additions may cause $PWNI (\hat{C})$ to reject programs that do not exhibit illicit λ-flows.

Absent a widely accepted semantic definition for information flow in the presence of reclassifications – and none has yet appeared in the literature – examples must suffice as a starting point for any discussion of whether definitions being given for $Δ_{\hat{C}}^{-} (λ, C_{i})$ and $Δ_{\hat{C}}^{+} (λ, C_{i})$ are sensible.

The larger question is whether PWNI constitutes a reasonable approach to defining secure programs when reclassifications are possible, independent of the specific choices for $Δ_{\hat{C}}^{-} (λ, C_{i})$ and $Δ_{\hat{C}}^{+} (λ, C_{i})$ . Here, besides considering various examples, the declassification principles described in Sabelfeld and Sand [53] offer criteria for evaluation. The principles are:

Conservativity: In programs that do not involve reclassification, satisfying PWNI implies satisfying noninterference. Thus, PWNI satisfies conservativity.

Non-occlusion: PWNI satisfies non-occlusion because declassifications do not allow other secret values to be leaked. The syntactic equality on commands at the end of λ-pieces, which some might find too conservative, is here seen as ensuring PWNI satisfies non-occlusion.

Semantic Consistency: PWNI does not satisfy semantic consistency. Transformation of a declassification-free program in a semantics-preserving way might not preserve PWNI. However, we know of no policy that satisfies semantic consistency and also (i) specifies a where dimension for downgrades, (ii) has the capability to allow downgrades of expressions in the midst of the computation (rather than restricting downgrades to initial values), (iii) does not employ memory-reset (which was already shown problematic for program (30) above), and (iv) satisfies Conservativity and Non-occulusion. An interesting open research problem is to determine whether (i)–(iv) necessarily implies that semantic consistency cannot be satisfied.

Monotonicity of Release: PWNI does not satisfy monotonicity of release, because adding declassification annotations might render a secure program insecure. The example used in [4], which shows that localized delimited release does not satisfy monotonicity of release, applies to PWNI as well.

5. Static enforcement of PWNI

Type-checking allows static enforcement of $PWNI (\hat{C})$ when $\hat{C}$ is written in a programming language having a type system based on some checkable class of RIF labels. A simple imperative language provides a vehicle for demonstration.

Language and semantics. Fig. 4 gives a syntax of a simple programming language for defining commands. There, ν ranges over constants, x ranges over program variables, $E, E_{1}, E_{2}, \dots$ range over ordinary expressions, and $C_{t}, C_{e}, C_{1}, C_{2}, \dots$ range over commands. Note, allowing only reclassifying expressions (rather than ordinary expressions) in the language syntax for commands is not a limitation – due to (5), identity reclassifier ϵ is handled by every RIF label and reclassifying expression ${[E]}_{ϵ}$ has the same value and RIF label as ordinary expression $E$ .

Fig. 4.

Syntax of simple imperative language.

Fig. 5.

Operational semantics.

Figure 5 gives an operational semantics for the programming language of Fig. 4. We write $M [x \mapsto ν]$ there to denote a mapping that is identical to $M$ except $M (x) = ν$ . The rules in Fig. 5 define partial function $Υ (C, M)$ .

The final part of the semantics for this programming language is definitions for $Δ (C_{i})$ , $Δ_{\hat{C}}^{-} (λ, C_{i})$ , and $Δ_{\hat{C}}^{+} (λ, C_{i})$ . These are given in Fig. 6 through Fig. 8. In defining $Δ_{\hat{C}}^{-} (λ, C_{i})$ , we write $lhs (C_{i})$ to denote the set of target variables in assignments appearing in a command $C_{i}$ .

$Δ_{\hat{C}}^{-} (λ, C_{i})$ excludes λ-downgrades that cannot influence the value being assigned to a variable x where $Γ (x) ⊑_{Λ} λ$ holds. No illicit λ-flow is possible without such an assignment.

$Δ_{\hat{C}}^{+} (λ, C_{i})$ for $if$ and $while$ is the smallest set that satisfies (34). To exclude λ-upgrade guards because an assignment does not appear in the body of an $if$ or $while$ (as done in the definition of $Δ_{\hat{C}}^{+} (λ, C_{i})$ ) would invalidate (34) by decreasing the size of $Δ_{\hat{C}}^{+} (λ, C_{i})$ .

Fig. 6.

Definition of $Δ (C_{i})$ .

Fig. 7.

Definition of $Δ_{\hat{C}}^{-} (λ, C)$ .

Fig. 8.

Definition of $Δ_{\hat{C}}^{+} (λ, C)$ .

Fig. 9.

Typing rules for expressions.

Typing rules. Fig. 9 gives rules to associate a type with each expression. The rules for ordinary expressions are standard. $E XPR - T$ instantiates (9); $A NN E XPR - T$ is based on (10).

Figure 10 shows the familiar rules to deduce whether a command is type-correct. Judgment $Γ, λ_{κ} ⊢ C$ signifies that a command $C$ is type correct. Parameter $λ_{κ}$ in these rules is called pc-label. It is used in checking for implicit flows. A pc-label $λ_{κ}$ associates a type with the conjunction of the guards for all of the enclosing conditional commands; $λ_{κ}$ is combined with the type of the right hand side of an assignment statement.

Fig. 10.

Typing rules for commands.

The following theorem states that if a program is type correct, then this program satisfies PWNI.

Theorem 1.

If $Γ, λ_{κ} ⊢ C$ , then $PWNI (C)$ holds.

Proof.

See [33, Appendix A.1] □

It was not a coincidence that we could enforce our expressive RIF labels by adapting a type system like the one used in Volpano et al. [59]. The type system in [59] can enforce any set of labels that form a join semi-lattice, and RIF labels form a join semi-lattice. In general, any enforcement mechanism that enforces noninterference for traditional label lattices, should be easily extendable to enforce piecewise noninterference for RIF labels, since piecewise noninterference is the conjunction of noninterference for successive λ-pieces of execution.

6. κ-Labels: Illustrating leverage from type-checking RIF labels

Although RIF automata are a checkable class of RIF labels, they are not expressive enough to specify allowed flows of information in the presence of cryptographic operations. In this section we give another example of a checkable class of RIF labels: κ-labels. Programs written in terms of a type system based on κ-labels can be checked by a compiler in order to get assurance that a value v flows to $v^{'}$ only if principals authorized to read $v^{'}$ are (i) authorized to read v or (ii) unable to reverse some cryptographic operation used in generating $v^{'}$ from v. So the type system allows us to conclude that encryptions and decryptions are successfully keeping secrets. Our modelling of cryptographic operations follows the symbolic formulation of Dolev and Yao [22].14

¹⁴
Notice that we do not consider a Dovel–Yao attacker. Our threat model is the one defined in Section 4.1.

The starting point for defining allowed flows based on κ-labels is mapping $KN$ to sets of principals from variables and from cryprographic keys.

$KN (x)$ is the set of principals allowed to know the initial value of variable x.

$KN (k)$ is the set of principals allowed to know the value of cryptographic key k, which is considered a constant.

Reclassifiers for κ-labels are associated with cryptographic operations, and rewrite rules for sequences of reclassifiers characterize when cryptographic operations are inverses. Different cryptosystems and cryptographic operations give rise to different reclassifiers along with different sets of rewrite rules.

κ-Atoms. A κ-atom $κ_{i}$ for a value $v_{i}$ to which v has flowed is a pair $⟨ F_{i}, β_{i} ⟩$ , where $F_{i} \in F_{κ}^{*}$ gives the sequence of cryptographic operations involved in deriving $v_{i}$ from v, and $β_{i}$ is a set of principals authorized to read v. Let $A_{κ}$ denote the set of κ-atoms. Reclassifier $𝜃 (a_{1}, \dots, a_{n}) \in F_{κ}$ is associated with a cryptographic operation 𝜃 whose invocation has $a_{1}, \dots, a_{n}$ in its list of arguments, which may be cryptographic keys or other expressions.

A rewrite rule will have form $\begin{matrix} 𝜃 (a) 𝜃^{'} (a^{'}) ↣ ϵ \end{matrix}$ where $𝜃 (a)$ and $𝜃^{'} (a^{'})$ are reclassifiers. This rewrite rule defines $𝜃^{'} (a^{'})$ to be the complement of $𝜃 (a)$ and allows appearances of “ $𝜃 (a) 𝜃^{'} (a^{'})$ ” to be deleted in a sequence of reclassifiers. Notation ${𝜃 (a)}^{c}$ will be used to denote the complement of reclassifier $𝜃 (a)$ . Reclassifiers are not required to have complements, but if complements ${𝜃 (a)}^{c}$ and ${({𝜃 (a)}^{c})}^{c}$ both do exist then we require that ${({𝜃 (a)}^{c})}^{c} = 𝜃 (a)$ holds.

To illustrate, we formulate κ-atoms for a symmetric-key cryptosystem having two cryptographic operations – encryption and decryption. $Enc (p, k)$ produces a ciphertext from plaintext p and key k. Its reclassifiers are defined by regarding appearances of $Enc (p, k)$ to be instances of reclassifying expression $\begin{matrix} {[Enc (p, k)]}_{𝜃_{Enc}^{1} (k), 𝜃_{Enc}^{2} (p)} \end{matrix}$ which posits flows occur from p (associated with reclassifier $𝜃_{Enc}^{1} (k)$ ) and from k (associated with reclassifier $𝜃_{Enc}^{2} (p)$ ) to the value that $Enc (p, k)$ produces. $Dec (c, k)$ recovers the plaintext iff ciphertext c was previously encrypted using k. It has reclassifiers for the flows from c and from k to the value that $Dec (c, K)$ produces: $\begin{matrix} {[Dec (c, k)]}_{𝜃_{Dec}^{1} (k), 𝜃_{Dec}^{2} (c)} \end{matrix}$ And we assume $Enc$ and $Dec$ satisfy the expected properties. $\begin{array}{l} (38) & Dec (Enc (v, k), k) = v holds for all values v and keys k . \\ (39) & Dec (c, k) is the only way to recover p from c = Enc (p, k) . \\ (40) & Key k cannot be recovered from ciphertexts created using k . \end{array}$

Property (38) stipulates that the effects of $Enc (\cdot, k)$ on plaintext can be reversed by using $Dec (\cdot, k)$ ; it is that basis for rewrite rule $\begin{matrix} (41) & \forall k : 𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k) ↣ ϵ . \end{matrix}$ Property (39) further implies that $𝜃_{Dec}^{1} (k)$ is the only complement of $𝜃_{Enc}^{1} (k)$ . Thus, (39) stipulates an absence of certain rewrite rules. Finally, (40) prohibits rewrite rules that would define complements for reclassifiers associated with flows from k: $𝜃_{Enc}^{2} (\cdot)$ and $𝜃_{Dec}^{2} (\cdot)$ . This prohibition corresponds to forbidding cryptographic functions where a key used as input to that function can be recovered from the output. It also rules out cryptographic systems that admit plaintext attacks.15

¹⁵

A plaintext attack uses plaintext p and corresponding ciphertext c to recover the encryption key k satisfying $c = Enc (p, k)$ . The attack can be viewed as having a cryptographic function ${[PA (p, c)]}_{𝜃_{PA}^{1} (c), 𝜃_{PA}^{2} (p)}$ that satisfies: $\begin{matrix} PA (p, c) = k if c = Enc (p, k) \end{matrix}$ This semantics for $PA (p, c)$ would lead to rewrite rules – precluded by (40) stipulating that plaintext attacks are infeasible – for the flows from k in $Enc (p, k)$ : $\begin{array}{l} 𝜃_{Enc}^{2} (p) 𝜃_{PA}^{2} (p) ↣ ϵ \end{array}$

Reduced sequence $(| F |)$ denotes the sequence obtained by repeatedly applying some given rewrite rules to sequence $F$ of reclassifiers, until no longer possible. By definition, no reclassifier is followed by its complement in a reduced sequence. If the full set of rewrite rules defines at most one complement for each reclassifier then (i) reduced sequence $(| F |)$ is unique and (ii) the order in which rewrite rules are applied does not matter, so $(| F |)$ is associative; see [33, Appendix A.3] for proofs.

All reclassifiers in rewrite rule (41) have a single argument k; it is a key. We define set $X (𝜃 (k))$ of principals that can recover a value produced by a cryptographic operation associated with a reclassifier $𝜃 (k)$ as follows. $\begin{matrix} X (𝜃 (k)) ≜ \{\begin{matrix} \emptyset & if complement {𝜃 (k)}^{c} does not exist \\ KN (k^{'}) & if {𝜃 (k)}^{c} = 𝜃^{'} (k^{'}) \end{matrix} \end{matrix}$ Set complement $\overline{X (f)}$ thus contains those principals that cannot recover a value produced by the cryptographic operation identified by $f$ .

If a value $v^{'}$ is derived from v by performing a sequence of cryptographic operations described with sequence $F$ of reclassifiers then v can be recovered from $v^{'}$ only by those principals able to perform inverses of all operations mentioned in $(| F |)$ . So the set $\overline{X} (F)$ of principals that cannot recover a value produced using a sequence $F$ of cryptographic operations are those principals that cannot invert at least one of the operations in $F$ . We characterize that set formally as follows, writing $f \in (| F |)$ to indicate that $f$ ranges over the reclassifiers appearing in reduced sequence $(| F |)$ . $\begin{matrix} \overline{X} (F) ≜ ⋃_{f \in (| F |)} \overline{X (f)} \end{matrix}$

κ-atoms concern confidentiality for principals in a set $Prins$ . Subsets are more restrictive, so we use $⟨ 2^{Prins}, \cap, \supseteq ⟩$ as the join semilattice $⟨ R, ⊔_{R}, ⊑_{R} ⟩$ of underlying restrictions. $R_{A} (⟨ F, β ⟩)$ is defined to be the set of principals to which the value associated with $⟨ F, β ⟩$ may flow – the set of principals in β along with principals $\overline{X} (F)$ that cannot recover an input to the sequence $F$ of cryptographic operations: $\begin{array}{l} R_{A} (⟨ F, β ⟩) & ≜ β \cup \overline{X} (F) \end{array}$ And $T_{A} (⟨ F, β ⟩, f)$ specifies the flows allowed by $⟨ F, β ⟩$ when its associated value is transformed by some cryptographic operation being identified with reclassifier $f$ . $\begin{array}{l} T_{A} (⟨ F, β ⟩, f) & ≜ ⟨ F f, β ⟩ \end{array}$

For example, an initial value v that can flow to principals in $β_{v}$ would be associated with κ-atom $⟨ ϵ, β_{v} ⟩$ . And κ-atom $T_{A} (⟨ F, β ⟩, f)$ associated with a transformed value potentially changes the set of principals where that transformed value might flow.16

¹⁶

The new set of principals is a superset when $(| F f |)$ extends $(| F |)$ and $\overline{X (f)} ⊈ \overline{X} (F)$ holds. It is a subset when $(| F f |)$ is a proper prefix of $(| F |)$ , $\overline{X (f)} ⊈ \overline{X} (F f)$ and $\overline{X (f^{c})} ⊈ \overline{X} (F f)$ hold. (If $(| F f |)$ is a proper prefix of $(| F |)$ then $f$ is the complement of the final reclassifier in $(| F |)$ , so $(| F f |)$ contains neither the final reclassifier in $(| F |)$ nor the $f$ being added.)

The definition of restrictiveness relation $⊑_{A}$ on κ-atoms is obtained by substituting $R_{A}$ and $T_{A}$ for $R_{}$ and $T_{}$ in $⊑_{Λ}$ definition (8). Notice that for all $F \in F_{κ}^{*}$ $\begin{matrix} ⟨ F, β ⟩ = ⟨ (| F |), β ⟩ \end{matrix}$ and, therefore, an implementation of κ-atoms need only store reduced sequences.

A computable test to decide $⊑_{A}$ for κ-atoms can be obtained by extending complement sequences from Dolev–Yao [22], as follows. For any finite sequence $F$ of reclassifiers, define maximal complement sequence $F^{c}$ to be the sequence of reclassifiers that minimizes the length of $(| F F^{c} |)$ . $F^{c}$ can be computed by taking the complement of each element in $F$ , starting at the end. $\begin{matrix} F^{c} ≜ \{\begin{matrix} ϵ & if F = ϵ \\ f^{c} {F_{1}}^{c} & if F = F_{1} f and f^{c} exists \\ ϵ & otherwise \end{matrix} \end{matrix}$ A test for $⊑_{A}$ is then given by: $\begin{matrix} (42) & ⟨ F_{1}, β_{1} ⟩ ⊑_{A} ⟨ F_{2}, β_{2} ⟩ = R_{A} (⟨ F_{1} {F_{1}}^{c}, β_{1} ⟩) \supseteq R_{A} (⟨ F_{2} {F_{1}}^{c}, β_{2} ⟩) \end{matrix}$ Soundness and completeness proofs for this test are given in [33, Appendix A.3].

κ-Labels. A κ-label $K$ is a finite set of κ-atoms. If we adopt the following definitions for $R_{L} (K)$ , and $T_{L} (K, f_{})$ , $\begin{array}{l} (43) & R_{L} (K) ≜ ⊔_{R} κ \in K : R_{A} (κ) \\ (44) & T_{L} (K, f_{}) ≜ {T_{A} (κ, f_{}) | κ \in K} \end{array}$ then κ-labels form a join semilattice $⟨ 2^{A_{κ}}, ⊔_{L}, ⊑_{L} ⟩$ where $⊔_{L}$ is defined by $\begin{array}{l} (45) & K ⊔_{L} K^{'} ≜ K \cup K^{'} \end{array}$ and restrictiveness relation $⊑_{L}$ is defined by substituting $R_{L}$ and $T_{L}$ into $⊑_{Λ}$ definition (8). The RIF class is then characterized by: $\begin{matrix} (46) & ⟨ ⟨ R, ⊔_{R}, ⊑_{R} ⟩, ⟨ 2^{A_{κ}}, ⊔_{L}, ⊑_{L} ⟩, F_{κ}, R_{L}, T_{L} ⟩ \end{matrix}$

Examples of κ-labels. To illustrate, we typecheck a simple command that invokes operations of the symmetric cryptosystem formalized above. Suppose x is allowed to flow to some subset $P_{x}$ of set $Prins$ of all principals, principals in $P_{x}$ are authorized to know key k, y is allowed to flow to some subset $P_{y}$ of $Prins$ , and principals in $P_{y}$ are authorized to know key $k^{'}$ : $\begin{array}{l} KN (x) = P_{x} KN (k) = P_{x} KN (y) = P_{y} KN (k^{'}) = P_{y} \end{array}$ Here is a command that combines the symmetric-key cryptographic operations discussed above. $\begin{matrix} (47) & \begin{matrix} w : = {[Enc (x, k)]}_{𝜃_{Enc}^{1} (k), 𝜃_{Enc}^{2} (x)}; \\ y : = {[Dec (w, k^{'})]}_{𝜃_{Dec}^{1} (k^{'}), 𝜃_{Dec}^{2} (w)} \end{matrix} \end{matrix}$ A first assignment encrypts x using key k and then a second assignment attempts to decrypt that ciphertext using a key $k^{'}$ .

Given the assumptions above about x and k, we posit the following type declarations for the variables named in the first assignment of (47). Notice, the type for w corresponds to a value that has been encrypted under key k. $\begin{array}{l} (48) & Γ (x) ≜ {⟨ ϵ, P_{x} ⟩} Γ (k) ≜ {⟨ ϵ, P_{x} ⟩} Γ (w) ≜ {⟨ 𝜃_{Enc}^{1} (k), P_{x} ⟩} \end{array}$ Using these types and typing rule $A NN E XPR - T$ in Fig. 9, we obtain a type for the RHS of the first assignment of (47). $\begin{matrix} T_{L} (Γ (x), 𝜃_{Enc}^{1} (k)) ⊔_{L} T_{L} (Γ (k), 𝜃_{Enc}^{2} (x)) \end{matrix}$ So, according to typing rule $A SGN - T$ in Fig. 10, that assignment is type correct provided the following holds. $\begin{array}{l} (49) & (T_{L} (Γ (x), 𝜃_{Enc}^{1} (k)) ⊔_{L} T_{L} (Γ (k), 𝜃_{Enc}^{2} (x))) ⊑_{L} Γ (w) \end{array}$ Substituting according to type declarations (48), obligation (49) for type correctness simplifies as follows: $\begin{array}{l} {⟨ 𝜃_{Enc}^{1} (k), P_{x} ⟩} \cup {⟨ 𝜃_{Enc}^{2} (x), P_{x} ⟩} ⊑_{L} {⟨ 𝜃_{Enc}^{1} (k), P_{x} ⟩} \\ = {⟨ 𝜃_{Enc}^{1} (k), P_{x} ⟩, ⟨ 𝜃_{Enc}^{2} (x), P_{x} ⟩} ⊑_{L} {⟨ 𝜃_{Enc}^{1} (k), P_{x} ⟩} \\ = (\forall F : R_{L} ({⟨ 𝜃_{Enc}^{1} (k) F, P_{x} ⟩, ⟨ 𝜃_{Enc}^{2} (x) F, P_{x} ⟩}) ⊑_{R} R_{L} ({⟨ 𝜃_{Enc}^{1} (k) F, P_{x} ⟩})) \\ = (\forall F : R_{A} (⟨ 𝜃_{Enc}^{1} (k) F, P_{x} ⟩) ⊔_{R} R_{A} (⟨ 𝜃_{Enc}^{2} (x) F, P_{x} ⟩) ⊑_{R} R_{A} (⟨ 𝜃_{Enc}^{1} (k) F, P_{x} ⟩)) \\ = (\forall F : (P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F)) \cap (P_{x} \cup \overline{X} (𝜃_{Enc}^{2} (x) F) \supseteq P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F)) \\ = (\forall F : (P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F)) \cap (P_{x} \cup Prins) \supseteq P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F)) \\ = (\forall F : (P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F) \supseteq P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) F)) \end{array}$ The final formula is trivially equivalent to $true$ .

Analogous reasoning establishes that the second assignment is type correct provided the following holds. $\begin{matrix} (50) & (T_{L} (Γ (w), 𝜃_{Dec}^{1} (k^{'})) ⊔_{L} T_{L} (Γ (k^{'}), 𝜃_{Dec}^{2} (w))) ⊑_{L} Γ (y) \end{matrix}$ The validity of (50) depends on whether $k = k^{'}$ holds and on the choice of $P_{y}$ and $P_{k^{'}}$ in the following proposed types for $Γ (y)$ and $Γ (k^{'})$ : $\begin{array}{l} Γ (y) ≜ {⟨ ϵ, P_{y} ⟩} Γ (k^{'}) ≜ {⟨ ϵ, P_{k^{'}} ⟩} \end{array}$

Case $k = k^{'}$ : From $Γ (k^{'}) = Γ (k)$ , we conclude from $Γ (k)$ and $Γ (k^{'})$ that $P_{k^{'}} = P_{x}$ holds. Expanding (50) gets $\begin{array}{l} (\forall F : (P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k) F)) \cap (P_{x} \cup \overline{X} (𝜃_{Dec}^{2} (w) F)) \supseteq (P_{y} \cup \overline{X} (F))) \\ = due to (40), \overline{X} (𝜃_{Dec}^{2} (w) F) = Prins \\ (\forall F : P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k) F) \supseteq (P_{y} \cup \overline{X} (F))) \\ = since \overline{X} (𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k) F) simplifies to \overline{X} (F) \\ (\forall F : P_{x} \cup \overline{X} (F) \supseteq (P_{y} \cup \overline{X} (F))) \end{array}$ This final formula is valid provided $P_{x} \supseteq P_{y}$ holds. So we have established that if $k = k^{'}$ holds then the assignment is type correct provided $P_{x} \supseteq P_{y}$ holds. This conclusion should not be surprising, since if $P_{x} ⊉ P_{y}$ holds then once w has been decrypted, the value of x (which would now be stored in y) could flow to principals not in $P_{x}$ (because they are in $P_{y} - P_{x}$ ).

Case $k \neq k^{'}$ : Expanding (50) yields:: $\begin{matrix} (\forall F : (P_{x} \cup \overline{X} (𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k^{'}) F)) \cap (P_{k^{'}} \cup \overline{X} (𝜃_{Dec}^{2} (w) F)) \supseteq (P_{y} \cup \overline{X} (F))) \end{matrix}$ This formula is valid for all values of $P_{x}$ and $P_{y}$ since, by definition of $\overline{X} (\cdot)$ , $\begin{matrix} \overline{X} (𝜃_{Enc}^{1} (k) 𝜃_{Dec}^{1} (k^{'}) F) = Prins and \overline{X} (𝜃_{Dec}^{2} (w) F) = Prins \end{matrix}$ because complements ${𝜃_{Dec}^{1} (k^{'})}^{c}$ and ${𝜃_{Dec}^{2} (w)}^{c}$ do not exist. Thus, we conclude the assignment is type correct when $k \neq k^{'}$ , for any choices of $P_{y}$ and $P_{k^{'}}$ . Again, this outcome should not be surprising. With no way to recover x from the value stored in y by the second assignment (since we have assumed that cryptographic operation $Dec (w, k^{'})$ has no inverse), the second assignment cannot cause a flow violation.

Type-correctness guarantee for κ-labels. The connection between type correctness and flows proved for this example command is an instance of a more-general guarantee about type correctness. To formalize this guarantee, note that any value a principal $p$ could read must be tagged with a κ-label $K_{L}$ satisfying $K_{L} ⊑_{L} K_{p}$ , where $\begin{matrix} K_{p} ≜ {⟨ F, β ⟩ \in A_{κ} | p \in R_{A} (⟨ F, β ⟩)} . \end{matrix}$ We consider a κ-label $K$ to be $p$ -low iff $K ⊑_{L} K_{p}$ holds and to be $p$ -high iff $K ⋢_{L} K_{p}$ holds. Thus the type-correctness guarantee provided by (any) κ-labels can be formulated as limiting what $p$ can learn from values that flow from $p$ -high to $p$ -low – in particular, type correctness ensures that $p$ cannot recover a $p$ -high value from $p$ -low values.

To show why this guarantee persists when using the κ-labels we defined above for the symmetric-key cryptosystem, consider a command $C$ that is type correct. Theorem 1 implies $PWNI (C)$ will hold and, therefore, if a value flows from $p$ -high to $p$ -low, then it does so through some operation that performs a $K_{p}$ -downgrade. Since cryptographic operations $Enc (\cdot, \cdot)$ and $Dec (\cdot, \cdot)$ are the sole reclassifying expressions for our κ-labels, we conclude that all $K_{p}$ -downgrades are caused by these operations. Without loss of generality, let such an operation be described by $\begin{matrix} (51) & {[𝜃 (E, k)]}_{𝜃^{1} (k), 𝜃^{2} (E)} \end{matrix}$ which has a flow from $E$ (associated with reclassifier $𝜃^{1} (k)$ ) and a flow from k (associated with reclassifier $𝜃^{2} (E)$ ) to the value that $𝜃 (E, k)$ produces.

By definition, for (51) to exhibit a $K_{p}$ -downgrade then $\begin{matrix} Γ ({[𝜃 (E, k)]}_{𝜃^{1} (k), 𝜃^{2} (E)}) ⊑_{L} K_{p} \land Γ (𝜃 (E, k)) ⋢_{L} K_{p} \end{matrix}$ must hold. From the first conjunct we get: $\begin{matrix} (52) & p \in R_{L} (Γ ({[𝜃 (E, k)]}_{𝜃^{1} (k), 𝜃^{2} (E)})) \end{matrix}$ To validate the type-correctness guarantee, it suffices to prove that $p$ cannot recover either $E$ or k from $𝜃 (E, k)$ or, equivalently that the following hold. $\begin{array}{l} p \in \overline{X (𝜃^{1} (k))} p \in \overline{X (𝜃^{2} (E))} \end{array}$

Establishing $p \in \overline{X (𝜃^{1} (k))}$ . $\begin{array}{l} p \in R_{L} (Γ ({[𝜃 (E, k)]}_{𝜃^{1} (k), 𝜃^{2} (E)}) \\ = A NN E XPR - T \\ p \in R_{L} (T_{L} (Γ (E), 𝜃^{1} (k)) ⊔_{L} T_{L} (Γ (k), 𝜃^{2} (E))) \\ = definition of R_{L} where ⊔_{R} is \cap \\ p \in R_{L} (T_{L} (Γ (E), 𝜃^{1} (k))) \cap R_{L} (T_{L} (Γ (k), 𝜃^{2} (E))) \\ = {(𝜃^{2} (E))}^{c} not defined so R_{L} (T_{L} (Γ (k), 𝜃^{2} (E))) = Prins \\ p \in R_{L} (T_{L} (Γ (E), 𝜃^{1} (k))) \\ = let Γ (E) = {⟨ F_{1}, β_{1} ⟩, \dots, ⟨ F_{n}, β_{n} ⟩} \\ p \in (R_{A} (⟨ F_{1} 𝜃^{1} (k), β_{1} ⟩) ⊔_{R} \dots ⊔_{R} R_{A} (⟨ F_{n} 𝜃^{1} (k), β_{n} ⟩)) \\ = definition of R_{A}; ⊔_{R} is \cap \\ p \in ((β_{1} \cup \overline{X} (F_{1} 𝜃^{1} (k))) \cap \dots \cap (β_{n} \cup \overline{X} (F_{n} 𝜃^{1} (k))) \\ = Γ (𝜃 (E, k)) ⋢_{L} K_{p} \Rightarrow p \notin ((β_{1} \cup \overline{X} (F_{1})) \cap \dots \cap (β_{n} \cup \overline{X} (F_{n}))) \\ p \in \overline{X (𝜃^{1} (k))} \end{array}$

Establishing $p \in \overline{X (𝜃^{2} (E))}$ . According to (40), $𝜃^{2} (E)$ has no complement. Thus, by definition, $\overline{X (𝜃^{2} (E))} = Prins$ .

7. Related work

RIF labels specify restrictions that depend on the history of applied operations. And a static type system can ensure that programs using RIF labels will satisfy PWNI, which extends noninterference [27] to accommodate reclassification. Our work thus extends an approach initiated by Volpano et al. [59] – a type system based on Denning’s lattice model [19–21] that enforces noninterference.

We are not the first to explore types that depend on a history of applied operations. Strom and Yemini [57] propose types that incorporate typestate to summarize the history of operations previously applied to an object and to govern the set of operations that may next be invoked. But Hartson and Hsiao [29] seem to be the first to use history in access control. Contemporary uses of history for defining authorization include stack inspection [61] and history-based access control [1].

7.1. Reclassification: Specification and enforcement

State based reclassification. A good deal of prior work ties reclassification to changes in state predicates. Chong et al. [16] is closest to RIF labels. There, information flow policies for confidentiality are defined in terms of state predicates that specify when a value may be reclassified. A static type system enforces these declassification and erasure policies. And when a reclassification occurs in the approach of Chong et al. [16], the value and all derived values are reclassified – in contrast, with RIF labels, reclassifications apply only to the single value.

With ClickRelease, Micinski et al. [43] extend the approach in Chong et al. [16] by allowing a more-expressive language for the formulas that specify when values may be declassified. In particular, ClickRelease uses temporal logic formulas over events, in contrast to the state predicates used by Chong et al. [16]

Paralocks [12] formulates a security policy as $Σ \Rightarrow α$ , where Σ is a set of state predicates and α is a principal. A value associated with such a policy is allowed to flow to α only if all predicates in Σ are true. Changes to state predicates in Σ alter the allowed flows. Paralocks policies are enforced using a static type system.

A policy in Thoth [24] and its successor system SHAI [23] specifies confidentiality and integrity restrictions for data containers called conduits. The policies comprise two layers. The access control layer specifies which principals may read and update the associated conduit and under what conditions. The declassification layer specifies conditions under which policies for data derived from the associated conduit can change. The conditions employed by a Thoth policy are predicates on conduits’ state, which include both data and metadata (including a type) of conduits. Thoth uses dynamic analysis for enforcement, SHAI uses static analysis too.

Jeeves [6] employs faceted values [5] to specify declassification between two levels of confidentiality (i.e., public and secret). A faceted value is a pair comprising a real and a dummy value, guarded by a state predicate. If that state predicate (which itself can be a faceted value) holds, then the real, possibly secret, value is allowed to flow to low outputs. Otherwise, the dummy value flows to low outputs.

All of this prior work thus ties reclassification to changes in state predicates. In contrast, RIF labels tie reclassification to expression evaluation. A comparison of RIF labels with reclassification based on state predicates thus depends first on what state predicates are available and second on whether those state predicates could be incorporated into RIF transition function $T_{}$ .

Operation based reclassification. Explicit expressions for declassification (for confidentiality) and endorsement (for integrity) have been proposed [44,46]. However, the approach can be unsatisfying because output restrictions are not connected to input restrictions or to the operation that transforms inputs to outputs. For example, [44,46] allow an arbitrary label to be assigned to the result of evaluating any expression – type-casting has the same flavor.

RIF labels tie reclassification to expression evaluation, but it is not the first work to connect restrictions on outputs to an operation. With FJifP [30], a principal declares trusted methods to declassify input values.17

¹⁷
Trusted methods are similar to trusted subjects, first introduced by Bell and LaPadula [8] to handle declassification.

A FJifP trusted method always performs the same declassification of an input whereas, depending on the RIF label associated with an input value, a specific reclassifier in a reclassifying expression could trigger different changes to the restrictions. So reclassifying expressions (in conjunction with RIF labels) are more expressive than trusted methods.

Rocha et al. [47] propose policy graphs to specify declassification of information from secret to public (as compared to RIF labels, which handle arbitrary reclassification); similar techniques to those presented in [47] are later employed by Hammer et al. [28] and Johnson et al. [32]. In a policy graph, nodes represent variables and edges represent operation identifiers (similar to our reclassifiers). The tail node of an edge is an input of the corresponding operation, and the head node of that edge is an output of that operation. Some of the nodes in a policy graph are defined final. Values in variables of non-final nodes are considered secret, whereas values in variables that correspond to final nodes are declassified and considered public. Data and control-flow analysis is used to check whether some given program satisfies a specific policy graph. Subsequently, Rocha et al. [48] introduce a specification language for defining policies that might also depend on how many times a function is applied to a given value. This specification language seems more expressive than Rocha et al. [47], although the properties being enforced have not been formally characterized. We believe restrictions defined using any of these policy graphs could be described using a set of RIF automata.

Li and Zdancewic [39] suggest that downgrades between two security levels be specified as lambda terms. Apply one of these lambda terms to a value and the result, by definition, is given a downgraded label. (A type system is given to enforce these policies.) This approach to characterizing downgrades is attractive because it is independent from the program code. Enforcement, however, involves a conservative approach to deciding equivalence of functions because that problem is undecidable in general. Also, the approach is not well suited for handling reclassifications based on how a value has been derived, whereas RIF labels do handle that.

7.2. Extending noninterference for reclassification

Declassification violates classical noninterference [27], which has prompted researchers to develop alternatives. One example is conditional noninterference [26,27]. It proscribes secret information flows to public information, unless a given predicate is satisfied by (i) the sequence of operations involved in this flow and (ii) the principals invoking those operations. For declassification, conditional noninterference is more expressive than PWNI, because PWNI ignores identities of the principals that invoke operations. PWNI, however, handles reclassification in full generality (i.e., arbitrary lattices of labels and declassification as well as classification), in contrast to conditional noninterference. which only deals with declassification in a 2-level lattice.

Gradual release (GR) [3] dictates that declassification of expressions, encrypted exceptions, and released cryptographic keys are the only execution points where an attacker’s knowledge about initial secret values may increase. Other work (delimited release [51] and relaxed noninterference [39]) specifies what expressions of secret values in the initial state could be declassified, with no restriction about where in the program such expressions are declassified.

PWNI supports declassifications of arbitrary expressions on any secret within the program. For this reason, the program below, which is arguably secure, is accepted by PWNI, but rejected by delimited release [51] (and its extensions, such as localized delimited release [4]): $\begin{matrix} (53) & h : = avg (h_{1}, h_{2}, h_{3}); l : = declassify (h) \end{matrix}$ Delimited release (and its extensions) rejects the above program for the same reason it rejects the following program: $\begin{matrix} (54) & h^{'} : = h; l : = declassify (h^{'}) \end{matrix}$ And the reason is to prevent laundering attacks – the declassification of $h^{'}$ inadvertently causing the declassification of h.

PWNI and RIF labels prevent laundering attacks by construction. If a variable is allowed to be declassified (e.g., $h^{'}$ in (54)), then this variable will be tagged with a RIF label that specifies declassification; if a variable is not allowed to be declassified (e.g., h in (54)), then this variable will be tagged with a RIF label that does not specify declassification. So, in (54), the RIF label of $h^{'}$ will not be as restrictive as the RIF label of h, and thus, PWNI will be violated by assignment $h^{'} : = h$ and the entire program will be rightfully rejected. On the other hand, PWNI rightfully accepts program (53), when all variables $h_{1}$ , $h_{2}$ , $h_{3}$ , h are tagged with a RIF label that specifies such a declassification.

The flexibility that PWNI offers to be able to handle declassifications of any secret expression in the program (and ultimately accept (53)) is a useful advantage. This is because usually the value that we desire to be ultimately declassified is the result of consecutive computations (i.e., an arbitrary expression in the program) – not the result of one clean expression on initial secrets. Those cases can be handled by PWNI, but not by delimited release (and its extensions).

The cost of the flexibility that PWNI offers comes from formally specifying what is being declassified and where in the program (similar targets to localized delimited release). Specifying what is being declassified in terms of initial secrets is in general undecidable when declassifying an arbitrary expression in the program. Consequently we choose to specify what is being declassified with respect to secrets that exist at the program point (i.e., command) where declassification is triggered. So, we set the reference point of the declassification to be the program point where this declassification is triggered. One way to select a program point as a reference point is to demand λ-pieces end and start at that same program point (just as the beginning of a program is regarded as a reference point for noninterference, demanding all executions to start from there). For this reason PWNI requires exact code equality at the ends of λ-pieces. And with exact code equality, the where dimension of the declassification is identified, too, because the program point at which an expression is declassified becomes explicit.

With conditional gradual release [7], as with our approach, any expression in a program may be declassified. However, conditional gradual release allows declassifications to depend on secret guards, causing a declassification to disclose more information than might have been intended. (PWNI does not suffer from this defect, because of the way λ-pieces are defined.)

Non-disclosure policy [42] is a variation of noninterference for handling local declassification constructs. These declassification constructs augment allowed flows during execution of some code M, restoring the previously allowed flows once execution leaves M. To satisfy the non-disclosure policy, noninterference must hold for flow relations that are allowed at every execution step. This policy, then, embodies a different design choice from PWNI about the scope of a declassification – with PWNI the declassification persists to the end of the execution, whereas with the non-disclosure policy it ends when the declassification construct has completed. The same design choice is adopted in [13] for handling flow-locks [11].

Other alternatives to noninterference associate declassification with special commands, such as match queries18

¹⁸
A match query checks whether two objects are equal. For example, a match query is use to check whether a certain string is the password of a given user.

[60], one-way functions [58], or various other cryptographic operations. With computational noninterference (CNI) [36], disclosure of secret values is permitted only when those values are encrypted; CNI is enforced by type systems introduced in Laud et al. [38] for passive and Fournet et al. [25] for active adversaries. Smith et al. [55] propose a variant of noninterference that handles both encryption and decryption, and it is enforced using a type system.

κ-labels demonstrate how RIF labels can handle cryptographic operations by treating these operations as special and translating them into reclassifying expressions. The literature on type checking of cryptographic operations has explored two general approaches [17]: computational and symbolic. κ-labels embrace the symbolic approach, using an analysis approach derived from Dolev–Yao [22]. Cryptographically masked flows [2] also employs a symbolic analysis, and it too is enforced by type systems. Laud [37] shows that type correctness according to [2], together with some additional conditions, imply CNI, thereby establishing a connection between cryptographically masked flows (which is based on symbolic analysis) and CNI (which is based on computational analysis). Cortier et al. [17] generalizes this connection by showing that programs secure according to a symbolic analysis are also secure according to a computational analysis.

Semantic properties have been proposed to handle erasure, too. Del Tedesco et al. [18] use knowledge semantics to express a hierarchy of erasure policies. These erasure policies are categorized based on (i) whether they specify erasure of all or part of the information, and (ii) whether erasure depends on program state (either high or low). Erasure is a form of classification, and thus, can be specified by RIF labels. However, with the RIF labels in this paper, erasure only affects a value being derived and cannot be formulated to depend on program state.

Noninterference and its variations (including PWNI) characterize allowed flows of information; they do not handle required flows. Chong [15] gives a semantic definition for required information release policies and presents a static type system to enforce these policies. A required information release policy specifies what information should be released and how this information can be learned by the authorized observers. The semantics is based on algorithmic knowledge.

7.3. Views of the reclassification landscape

The survey by Sabelfeld et al. [53] introduces a four-dimension categorization for declassification policies (though the categorization seems applicable reclassification, too): what information is declassified, who declassifies information, where in the system information is declassified, and when information can be declassified. RIF labels and our reclassifying expressions specify what, where, and when, but not who. The what is the value produced by the expression; where is the position of the reclassifying expression in the program text; when is determined by the program’s control flow.

Nothing prevents the semantics of our reclassifiers from incorporating information about who is evaluating a given reclassifying expression. The decentralized label model (DLM) [44,45] is an obvious starting point for such an extension. According to DLM, a value may be declassified only if the declassification command is executed on behalf of the value’s owner or on behalf of a principal that acts-for that owner. To adopt this approach, we would add an additional input argument to $T$ – the identity of the principal undertaking the reclassification. The semantics of $T$ would then be extended so that a reclassifier triggers a transition only for certain principals.

Broberg et al. [14] offers an orthogonal view for information flow policies and declassification. It is based on a three-level hierarchy of control. Level 0 control is a set of possible flow relations between information sources (e.g., input variables) and sinks (e.g., output channels). A flow relation indicates that information from the source is allowed to flow to the sink. Level 1 controls select which flow relations are allowed. Level 2 controls constitute a meta policy for controlling the way in which the current flow relations (Level 1 controls) may be changed. RIF label function $T$ incorporates aspects of Level 1 and Level 2 controls.

Footnotes

Acknowledgments

We appreciate the comments we received on early discussions of this work from Eleanor Birrell, Michael Clarkson, Josée Desharnais, Michael George, José Meseguer, Brad Martin, Andrew Myers, David Naumann, Karn Seth, Geoffrey Smith, and Nadia Tawbi. Steve Chong and Deepak Garg, in addition, provided detailed and very helpful feedback on an earlier draft of this paper. Diligence by the reviewers and the editor is also appreciated, and a better paper resulted.

This work was supported in part by AFOSR grants F9550-16-0250, F9550-19-1-0264, and NSF grant 1642120. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of these organizations or the U.S. Government.

⟨ Λ RA,,⊑ RA,⊔ RA ⟩ is a join semilattice

To prove that $⟨ Λ_{RA,}, ⊑_{RA}, ⊔_{RA} ⟩$ is a join semilattice requires showing (i) $λ_{α} ⊑_{RA} λ_{α} ⊔_{RA} λ_{α^{'}}$ , (ii) $λ_{α^{'}} ⊑_{RA} λ_{α} ⊔_{RA} λ_{α^{'}}$ , and (iii) that $λ_{α} ⊔_{RA} λ_{α^{'}}$ is the least upper bound.

To prove (i), it suffices to use decision procedure (15) for $⊑_{RA}$ , and prove: $\begin{matrix} (55) & (\forall ⟨ q, ⟨ q, q^{″} ⟩ ⟩ \in Q_{α \otimes (α ⊔ α^{'})} : ρ_{α} (q) ⊑_{R} ρ_{α ⊔ α^{'}} (⟨ q, q^{″} ⟩)), \end{matrix}$ because reachability condition (13) for $λ_{α} \otimes (λ_{α} ⊔_{RA} λ_{α ⊔ α^{'}})$ implies that if $\begin{matrix} ⟨ q, ⟨ q^{'}, q^{″} ⟩ ⟩ \in Q_{α \otimes (α ⊔ α^{'})} \end{matrix}$ holds then $q = q^{'}$ . Completing the proof of (55) is just a matter of expanding the definition of $ρ_{α ⊔ α^{'}} (⟨ q, q^{″} ⟩)$ .

The proof of (ii) is similar.

The proof of (iii) involves showing that $λ_{α} ⊔_{RA} λ_{α^{'}}$ is the least RIF label satisfying $\begin{array}{l} λ_{α} ⊑_{RA} λ_{α} ⊔_{RA} λ_{α^{'}} \\ λ_{α^{'}} ⊑_{RA} λ_{α} ⊔_{RA} λ_{α^{'}} \end{array}$ Our proof by contradiction derives $false$ from the assumption that a RIF label $λ_{α^{″}}$ satisfying $λ_{α} ⊑_{RA} λ_{α^{″}}$ , $λ_{α^{'}} ⊑_{RA} λ_{α^{″}}$ , and $λ_{α^{″}} ⊏_{RA} λ_{α} ⊔_{RA} λ_{α^{'}}$ exists.

From $λ_{α} ⊑_{RA} λ_{α^{″}}$ we have $R_{RA} (T_{RA} (λ_{α}, F)) ⊑_{R} R_{RA} (T_{RA} (λ_{α^{″}}, F))$ for any $F$ ; from $λ_{α^{'}} ⊑_{RA} λ_{α^{″}}$ we have $R_{RA} (T_{RA} (λ_{α^{'}}, F)) ⊑_{R} R_{RA} (T_{RA} (λ_{α^{″}}, F))$ for any $F$ . Since $⟨ R, ⊔_{R}, ⊑_{R} ⟩$ defines a lattice, we conclude $\begin{matrix} (56) & R_{RA} (T_{RA} (λ_{α}, F)) ⊔_{R} R_{RA} (T_{RA} (λ_{α^{'}}, F)) ⊑_{R} R_{RA} (T_{RA} (λ_{α^{″}}, F)) . \end{matrix}$ From assumption $λ_{α^{″}} ⊏_{RA} λ_{α} ⊔_{RA} λ_{α^{'}}$ we conclude (i) $λ_{α^{″}} ⊑_{RA} λ_{α} ⊔_{RA} λ_{α^{'}}$ and (ii) $λ_{α^{″}} \neq λ_{α} ⊔_{RA} λ_{α^{'}}$ . But (56) conjoined with (i) contradicts (ii).

Definition of T ( λ,C )

$T (λ, C)$ is defined based on a deterministic generator G of fresh variables, which store lists of values. Specifically, $G . init$ sets G to its initial state, and $G . fresh ({[E]}_{\bar{f}})$ returns the next fresh variable $h_{E}$ . Each variable $h_{E}$ stores a list of values with the same type as $E$ , and it is tagged with a RIF label that satisfies $Γ (h_{E}) = Γ ({[E]}_{\bar{f}})$ .

$T (λ, C)$ substitutes each upgrading expression ${[E]}_{\bar{f}}$ in $C$ with expression $next (h_{E})$ . So, we extend the evaluation and the RIF labels for expressions $E$ to accommodate this new expression $next (h_{E})$ . In particular, we define successive $M (next (h_{E}))$ evaluations to return successive elements of the list stored in $h_{E}$ . And define $Γ (next (h_{E}))$ to be $Γ (h_{E})$ .

We now give the formal definition for $T (λ, C)$ , which employs auxiliary procedures T and S. $\begin{array}{l} T (λ, C) ≜ T (λ, C, G . init) \\ T (λ, x : = {[E]}_{\bar{f}}, G) ≜ x : = S (λ, {[E]}_{\bar{f}}, G) \\ \begin{matrix} T (λ, if {[E]}_{\bar{f}} then C_{t} else C_{e}, G) ≜ & if S (λ, {[E]}_{\bar{f}}, G) then T (λ, C_{t}, G) \\ else T (λ, C_{e}, G) \end{matrix} \\ T (λ, while {[E]}_{\bar{f}} do C_{w}, G) ≜ while S (λ, {[E]}_{\bar{f}}, G) do T (λ, C_{w}, G) \\ T (λ, C_{1}; C_{2}, G) ≜ T (λ, C_{1}, G); T (λ, C_{2}, G) \\ S (λ, {[E]}_{\bar{f}}, G) ≜ \{\begin{matrix} {[next (G . fresh ({[E]}_{\bar{f}}))]}_{ϵ}, & if Γ (E) ⊑ λ \land Γ ({[E]}_{\bar{f}}) ⋢ λ \\ {[E]}_{\bar{f}}, & otherwise \end{matrix} \end{array}$

There is a reason why upgrading expressions are substituted by variables that store lists of values instead of variables that store ordinary (scalar) values: upgrading expressions in $while$ commands. When a $while$ command involves an upgrading expression, then this expression might yield as many upgraded values as the number of iterations of that command. All these values should be protected against leaking to certain principals. So, we substitute them with arbitrarily chosen values (which are elements of these lists) and ensure that they do not influence observations of these principals.

Notice that $T (λ, C)$ is deterministic, by construction. This means that for the same command $C$ , the translated command $T (λ, C)$ is always the same. So, comparing traces $τ = Υ (T (λ, \hat{C}), M)$ and $τ^{'} = Υ (T (λ, \hat{C}), M^{'})$ in PWNI definition (35) is meaningful, because these traces correspond to the exact same translated command.

References

Abadi and

Fournet, Access control based on execution history, in: Proceedings of the 10th Annual Network and Distributed System Security Symposium, 2003, pp. 107–121.

Askarov,

Hedin and

Sabelfeld, Cryptographically-masked flows, Theor. Comput. Sci. 402(2–3) (2008), 82–101. doi:10.1016/j.tcs.2008.04.028.

Askarov and

Sabelfeld, Gradual release: Unifying declassification, encryption and key release policies, in: Proceedings of the IEEE Symposium on Security and Privacy, 2007, pp. 207–221. doi:10.1109/SP.2007.22.

Askarov and

Sabelfeld, Localized delimited release: Combining the what and where dimensions of information release, in: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS’07, ACM, New York, NY, USA, 2007, pp. 53–60. doi:10.1145/1255329.1255339.

T.H.

Austin and

Flanagan, Multiple facets for dynamic information flow, in: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’12, ACM, New York, NY, USA, 2012, pp. 165–178. doi:10.1145/2103656.2103677.

T.H.

Austin,

Yang,

Flanagan and

Solar-Lezama, Faceted execution of policy-agnostic programs, in: Proceedings of the 8th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS’13, ACM, New York, NY, USA, 2013, pp. 15–26.

Banerjee,

D.A.

Naumann and

Rosenberg, Expressive declassification policies and modular static enforcement, in: Proceedings of the IEEE Symposium on Security and Privacy, 2008, pp. 339–353. doi:10.1109/SP.2008.20.

Bell and

La Padula, Secure computer systems: Unified exposition and MULTICS interpretation, Technical Report ESD-TR-75306, Bedford, MA, 1976.

Birrell and

F.B.

Schneider, A reactive approach to use-based privacy, Technical Report 54843, Cornell University, Computing and Information Science, November 2017.

10.

Broberg,

Delft and

Sands, Paragon for practical programming with information-flow control, in: Proceedings of the 11th Asian Symposium on Programming Languages and Systems, Vol. 8301, Springer-Verlag New York, Inc., New York, NY, USA, 2013, pp. 217–232. doi:10.1007/978-3-319-03542-0_16.

11.

Broberg and

Sands, Flow locks: Towards a core calculus for dynamic flow policies, in: Proceedings of the 15th European Conference on Programming Languages and Systems, ESOP’06, Springer-Verlag, Berlin, Heidelberg, 2006, pp. 180–196. doi:10.1007/11693024_13.

12.

Broberg and

Sands, Paralocks: Role-based information flow control and beyond, in: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’10, ACM, New York, NY, USA, 2010, pp. 431–444. doi:10.1145/1706299.1706349.

13.

Broberg and

Sands, Flow locks: Towards a core calculus for dynamic flow policies, Technical report, Chalmers University of Technology and Göteborgs University, May 2006.

14.

Broberg,

van Delft and

Sands, The anatomy and facets of dynamic policies, in: Proceedings of the 28th IEEE Computer Security Foundations Symposium, 2015, pp. 122–136. doi:10.1109/CSF.2015.16.

15.

Chong, Required information release, in: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, IEEE Press, Piscataway, NJ, USA, 2010, pp. 215–227.

16.

Chong and

A.C.

Myers, End-to-end enforcement of erasure and declassification, in: Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008, pp. 98–111. doi:10.1109/CSF.2008.12.

17.

Cortier,

Kremer and

Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, J. Autom. Reason. 46(3–4) (2011), 225–259. doi:10.1007/s10817-010-9187-9.

18.

Del Tedesco,

Hunt and

Sands, A semantic hierarchy for erasure policies, in: Proceedings of the 7th International Conference on Information Systems Security, ICISS’11, Springer-Verlag, Berlin, Heidelberg, 2011, pp. 352–369.

19.

D.E.

Denning, A lattice model of secure information flow, Commun. ACM 19(5) (1976), 236–243. doi:10.1145/360051.360056.

20.

D.E.

Denning and

P.J.

Denning, Certification of programs for secure information flow, Commun. ACM 20(7) (1977), 504–513. doi:10.1145/359636.359712.

21.

D.E.R.

Denning, Secure information flow in computer systems., PhD thesis, Purdue University, West Lafayette, IN, USA, 1975.

22.

Dolev and

A.C.

Yao, On the security of public key protocols, Information Theory, IEEE Transactions on 29(2) (1983), 198–208. doi:10.1109/TIT.1983.1056650.

23.

Elnikety,

Garg and

Druschel, SHAI: Enforcing data-specific policies with near-zero runtime overhead, Technical report, Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany, January 2018.

24.

Elnikety,

Mehta,

Vahldiek-Oberwagner,

Garg and

Druschel, Thoth: Comprehensive policy compliance in data retrieval systems, in: Proceedings of the 25th USENIX Conference on Security Symposium, SEC’16, USENIX Association, 2016, pp. 637–654.

25.

Fournet and

Rezk, Cryptographically sound implementations for typed information-flow security, in: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08, ACM, New York, NY, USA, 2008, pp. 323–335. doi:10.1145/1328438.1328478.

26.

J.A.

Goguen and

Mesegue, Unwinding and inference control, in: Proceedings of the IEEE Symposium on Security and Privacy, 1984, pp. 75–87.

27.

J.A.

Goguen and

Meseguer, Security policies and security models, in: Proceedings of the IEEE Symposium on Security and Privacy, 1982, pp. 11–20.

28.

Hammer and

Snelting, Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, International Journal of Information Security 8(6) (2009), 399–422. doi:10.1007/s10207-009-0086-1.

29.

H.R.

Hartson and

D.K.

Hsiao, Full protection specifications in the semantic model for database protection languages, in: Proceedings of the 1976 Annual Conference, ACM’76, ACM, New York, NY, USA, 1976, pp. 90–95. doi:10.1145/800191.805538.

30.

Hicks,

King,

McDaniel and

Hicks, Trusted declassification: High-level policy for a security-typed language, in: Proceedings of the Workshop on Programming Languages and Analysis for Security, PLAS’06, ACM, New York, NY, USA, 2006, pp. 65–74. doi:10.1145/1134744.1134757.

31.

T.H.

Hinke, Inference aggregation detection in database management systems, in: Proceedings. 1988 IEEE Symposium on Security and Privacy, 1988, pp. 96–106. doi:10.1109/SECPRI.1988.8101.

32.

Johnson,

Waye,

Moore and

Chong, Exploring and enforcing security guarantees via program dependence graphs, in: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’15, ACM, New York, NY, USA, 2015, pp. 291–302. doi:10.1145/2737924.2737957.

33.

Kozyri, Enhancing expressiveness of information flow labels: Reclassification and permissiveness, PhD thesis, Cornell University, Ithaca, New York, USA, 2018, https://search.proquest.com/docview/2167492985?accountid=10267.

34.

Kozyri,

Arden,

A.C.

Myers and

F.B.

Schneider, JRIF: Reactive information flow control for Java, Technical report, Cornell Univarsity, February 2016.

35.

Krohn,

Yip,

Brodsky,

Cliffer,

M.F.

Kaashoek,

Kohler and

Morris, Information flow control for standard OS abstractions, in: Proceedings of the 21st ACM SIGOPS Symposium on Operating Systems Principles, SOSP’07, ACM, New York, NY, USA, 2007, pp. 321–334. doi:10.1145/1294261.1294293.

36.

Laud, Semantics and program analysis of computationally secure information flow, in: Proceedings of the 10th European Symposium on Programming Languages and Systems, ESOP’01, Springer-Verlag, London, UK, 2001, pp. 77–91, http://dl.acm.org/citation.cfm?id=645395.651928 . doi:10.1007/3-540-45309-1_6.

37.

Laud, On the computational soundness of cryptographically masked flows, in: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08, ACM, New York, NY, USA, 2008, pp. 337–348. doi:10.1145/1328438.1328479.

38.

Laud and

Vene, A type system for computationally secure information flow, in: Proceedings of the 15th International Conference on Fundamentals of Computation Theory, FCT’05, Springer-Verlag, Berlin, Heidelberg, 2005, pp. 365–377. doi:10.1007/11537311_32.

39.

Li and

Zdancewic, Downgrading policies and relaxed noninterference, in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’05, ACM, New York, NY, USA, 2005, pp. 158–170. doi:10.1145/1040305.1040319.

40.

Li and

Zdancewic, Practical information-flow control in web-based information systems, in: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, CSFW’05, IEEE Computer Society, Washington, DC, USA, 2005, pp. 2–15. doi:10.1109/CSFW.2005.23.

41.

Lux and

Mantel, Declassification with explicit reference points, in: Computer Security – ESORICS 2009,

Backes and

Ning, eds, Springer Berlin Heidelberg, Berlin, Heidelberg, 2009, pp. 69–85. doi:10.1007/978-3-642-04444-1_5.

42.

A.A.

Matos and

Boudol, On declassification and the non-disclosure policy, in: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW’05), 2005, pp. 226–240. doi:10.1109/CSFW.2005.21.

43.

Micinski,

Fetter-Degges,

Jeon,

J.S.

Foster and

M.R.

Clarkson, Checking interaction-based declassification policies for Android using symbolic execution, in: Proceedings of the European Symposium on Research in Computer Security, ESORICS 2015, Springer International Publishing, Cham, 2015, pp. 520–538.

44.

A.C.

Myers, JFlow: Practical mostly-static information flow control, in: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’99, ACM, New York, NY, USA, 1999, pp. 228–241. doi:10.1145/292540.292561.

45.

A.C.

Myers and

Liskov, A decentralized model for information flow control, in: Proceedings of the 16th ACM Symposium on Operating Systems Principles, SOSP’97, ACM, New York, NY, USA, 1997, pp. 129–142. doi:10.1145/268998.266669.

46.

A.C.

Myers,

Zheng,

Zdancewic,

Chong and

Nystrom, Jif 3.0: Java information flow, Software release, http://www.cs.cornell.edu/jif, July 2006.

47.

B.P.S.

Rocha,

Bandhakavi,

den Hartog,

W.H.

Winsborough and

Etalle, Towards static flow-based declassification for legacy and untrusted programs, in: Proceedings of the IEEE Symposium on Security and Privacy, 2010, pp. 93–108. doi:10.1109/SP.2010.14.

48.

B.P.S.

Rocha,

Conti,

Etalle and

Crispo, Hybrid static-runtime information flow and declassification enforcement, Information Forensics and Security, IEEE Transactions on 8(8) (2013), 1294–1305. doi:10.1109/TIFS.2013.2267798.

49.

Roy,

D.E.

Porter,

M.D.

Bond,

K.S.

McKinley and

Witchel, Laminar: Practical fine-grained decentralized information flow control, in: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’09, ACM, New York, NY, USA, 2009, pp. 63–74. doi:10.1145/1542476.1542484.

50.

Sabelfeld and

A.C.

Myers, Language-based information-flow security, Selected Areas in Communications, IEEE Journal on 21(1) (2003), 5–19. doi:10.1109/JSAC.2002.806121.

51.

Sabelfeld and

A.C.

Myers, A model for delimited information release, in: Proceedings of the International Symposium on Software Security (ISSS’03), LNCS, Vol. 3233, Springer-Verlag, 2004, pp. 174–191.

52.

Sabelfeld and

Sands, A per model of secure information flow in sequential programs, in: Proceedings of the 8th European Symposium on Programming Languages and Systems, ESOP’99, Springer-Verlag, Berlin, Heidelberg, 1999, pp. 40–58. doi:10.1007/3-540-49099-X_4.

53.

Sabelfeld and

Sands, Declassification: Dimensions and principles, J. Comput. Secur. 17(5) (2009), 517–548, http://dl.acm.org/citation.cfm?id=1662658.1662659 . doi:10.3233/JCS-2009-0352.

54.

F.B.

Schneider,

Walsh and

E.G.

Sirer, Nexus Authorization Logic (NAL): Design rationale and applications, ACM Trans. Inf. Syst. Secur. 14(1) (2011), 8:1–8:28. doi:10.1145/1952982.1952990.

55.

Smith and

Alpízar, Secure information flow with random assignment and encryption, in: Proceedings of the 4th ACM Workshop on Formal Methods in Security, FMSE’06, ACM, New York, NY, USA, 2006, pp. 33–44. doi:10.1145/1180337.1180341.

56.

Stefan,

Russo,

J.C.

Mitchell and

Mazières, Flexible dynamic information flow control in Haskell, in: Proceedings of the 4th ACM Symposium on Haskell, Haskell’11, ACM, New York, NY, USA, 2011, pp. 95–106. doi:10.1145/2034675.2034688.

57.

R.E.

Strom and

Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Trans. Softw. Eng. 12(1) (1986), 157–171. doi:10.1109/TSE.1986.6312929.

58.

Volpano, Secure introduction of one-way functions, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000, pp. 246–254. doi:10.1109/CSFW.2000.856941.

59.

Volpano,

Irvine and

Smith, A sound type system for secure flow analysis, J. Comput. Secur. 4(2–3) (1996), 167–187, http://dl.acm.org/citation.cfm?id=353629.353648 . doi:10.3233/JCS-1996-42-304.

60.

Volpano and

Smith, Verifying secrets and relative secrecy, in: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’00, ACM, New York, NY, USA, 2000, pp. 268–276. doi:10.1145/325694.325729.

61.

D.S.

Wallach,

J.A.

Roskind and

E.W.

Felten, Flexible, extensible Java security using digital signatures, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 38 (1996), 59–74. doi:10.1090/dimacs/038/07.

RIF: Reactive information flow labels

Abstract

Keywords

1. Introduction

2. RIF labels

1 A partial order would suffice for the theory of RIF labels developed in this section. A join semilattice becomes useful for certain instantiations of RIF labels, as illustrated in §3 and §6.

3. RIF automata

5 JRIF is a variant of the Jif security-typed programming language, which extends Java with support for information flow control.

4.1. Observations as a threat model

12 Each trace is also a single H -piece. For that case, dpNI ( H , τ , τ ′ ) holds because τ . M = H τ ′ . M is equivalent to τ . M = τ ′ . M . The same applies to example programs (31) and (32) to come.

5. Static enforcement of PWNI

14 Notice that we do not consider a Dovel–Yao attacker. Our threat model is the one defined in Section 4.1.

7.1. Reclassification: Specification and enforcement

17 Trusted methods are similar to trusted subjects, first introduced by Bell and LaPadula [8] to handle declassification.

18 A match query checks whether two objects are equal. For example, a match query is use to check whether a certain string is the password of a given user.

Footnotes

Acknowledgments

⟨ Λ RA,,⊑ RA,⊔ RA ⟩ is a join semilattice

Definition of T ( λ,C )

References

¹
A partial order would suffice for the theory of RIF labels developed in this section. A join semilattice becomes useful for certain instantiations of RIF labels, as illustrated in §3 and §6.

⁵
JRIF is a variant of the Jif security-typed programming language, which extends Java with support for information flow control.

¹²
Each trace is also a single $H$ -piece. For that case, $dpNI (H, τ, τ^{'})$ holds because $τ . M =_{H} τ^{'} . M$ is equivalent to $τ . M = τ^{'} . M$ . The same applies to example programs (31) and (32) to come.

¹⁴
Notice that we do not consider a Dovel–Yao attacker. Our threat model is the one defined in Section 4.1.

¹⁷
Trusted methods are similar to trusted subjects, first introduced by Bell and LaPadula [8] to handle declassification.

¹⁸
A match query checks whether two objects are equal. For example, a match query is use to check whether a certain string is the password of a given user.