Security Type Systems as Recursive Predicates⋆
Andrei Popescu

arXiv:1308.3472v1 [cs.CR] 15 Aug 2013

Technische Universität München
Abstract. We show how security type systems from the literature of languagebased noninterference can be represented more directly as predicates defined by
structural recursion on the programs. In this context, we show how our uniform
syntactic criteria from [7,8] cover several previous type-system soundness results.

1 Security type systems
As in Example 2 from [7, 8], we assume that atomic statements and tests are built by
means of expressions applied to variables taken from a set var, ranged over by x, y, z.
Thus, exp, ranged over by e, is the set of arithmetic expressions (e.g., x + 1, x ∗ y + 5).
Then atomic commands atm ∈ atom are assignment statements x := e and tests tst ∈ test
are Boolean expressions built from exp (e.g., x > 0, x + 1 = y + z). For any expression
e and test tst, Vars e and Vars tst denote their sets of variables.
States are assignments of integers to variables, i.e., the set state is var → int. Variables are classified as either low (lo) or high (hi) by a fixed security level function
sec : var → {lo, hi}. We let L be the lattice {lo, hi}, where lo < hi.1 We shall use the standard infima and suprema notations for L. Then ∼ is defined as follows: s ∼ t ≡ ∀x ∈
var. sec x = lo =⇒ s x = t x.
We shall look into type systems from the literature, ::, assigning security levels l ∈
{lo, hi}, or pairs of security levels, to expressions and commands. All have in common
the following:
Typing of expressions:
e :: lo if ∀x ∈ Vars e. sec x = lo

e :: hi always

Typing of tests (similar):
tst :: lo if ∀x ∈ Vars tst. sec x = lo

tst :: hi always

The various type systems shall differ in the typing of commands.
But first let us look more closely at their aforementioned common part. We note
that, if an expression or a test has type l and l ≤ k, then it also has type k. In other
words, the following covariant subtyping rules for tests and expressions hold:
⋆
1

This work was supported by the DFG project Ni 491/13–2, part of the DFG priority program
Reliably Secure Software Systems (RS3).
One can also consider the more general case of multilevel security, via an unspecified lattice of
security levels L—however, this brings neither much additional difficulty, nor much additional
insight, so here focus on this 2-level lattice.

tst :: l l ≤ k
(SUBTYPE-TST)
tst :: k

e :: l l ≤ k
(SUBTYPE-EXP)
e :: k

Thus, the typing of an expression or test is uniquely determined by its minimal type,
defined as follows:
minTp e =

_

{sec x. x ∈ Vars e}

minTp tst

=

_

{sec x. x ∈ Vars tst}

The minimal typing operators can of course recover the original typing relation ::
as follows:
Lemma 1. The following hold:
(1) e :: l iff minTp e ≤ l.
(2) tst :: l iff minTp tst ≤ l.
1.1 Volpano-Smith possibilistic noninterference
In [11, §4], the typing of commands (which we denote by ::1 ) is defined inductively as
follows:
sec x = l e :: l
(ASSIGN)
(x := e) ::1 l
tst ::1 l c1 ::1 l c2 ::1 l
(IF)
(If tst c1 c2 ) ::1 l
c1 ::1 l c2 ::1 l
(PAR)
(Par c1 c2 ) ::1 l

c1 ::1 l c2 ::1 l
(COMPOSE)
(Seq c1 c2 ) ::1 l
tst ::1 lo c ::1 l
(WHILE)
(While tst c) ::1 lo
c ::1 l k ≤ l
(SUBTYPE)
c ::1 k

We think of c ::1 l as saying:
– There is no downwards flow in c.
– l is a lower bound on the level of the variables that the execution of c writes to.
(This intuition is accurately reflected by Lemma 2 below.)
Actually, [11] does not explicitly consider a rule like (PAR), and in fact uses parallel composition only at the top level. However, it does require that the thread pool
(which can be viewed as consisting of a number of parallel compositions) has welltyped threads, which is the same as typing the pool to the minimum of the types of its
threads—this is precisely what (PAR) does. (Also, in [11], the rule (WHILE) has the
assumption c ::1 lo rather that c ::1 l—this alternative is of course equivalent, thanks to
(SUBTYPE).)
Due to the subtyping rule, here we have a phenomenon dual to the one for expressions and tests: if a command has type l and k ≤ l, then it also has type k—thus, the
typing of a command, if any, is uniquely determined by its maximal type. The difference
from expressions and tests is that such a type may not exist, making it necessary to keep
a “safety" predicate during the computation of the maximal type. For example, consider
the computation of the minimal type of If tst c1 c2 according to the (IF) rule: Assume l0
is the minimal type of tst and l1 , l2 are the maximal types of c1 and c2 , respectively. The
rule (IF) requires the three types involved in the hypothesis to be equal, and therefore

we need to upcast l0 and downcast l1 and l2 so that we obtain a common type l—thus,
we need l0 ≤ l ≤ l1 ∧ l2 . Moreover, l has to be as high as possible. Such an l of course
only exists if l0 ≤ l1 ∧ l2 , and in this case the maximal l is l1 ∧ l2 . In summary, the rule
(IF) tells us the following:
– If tst c1 c2 is safe (i.e., type checks) iff c1 and c2 are safe and l0 ≤ l ≤ l1 ∧ l2 .
– If safe, the maximal type of If tst c1 c2 is l1 ∧ l2 .
Applying this reasoning to all the rules for ::1 , we obtain the function maxTp1 :
com → L and the predicate safe1 : com → bool defined recursively on the structure of
commands:2
Definition 1. – safe1 (x := e) = (minTp e ≤ sec x)
– maxTp1 (x := e) = sec x
– safe1 (Seq c1 c2 ) = (safe1 c1 ∧ safe1 c2 )
– maxTp1 (Seq c1 c2 ) = (maxTp1 c1 ∧ maxTp1 c2 )
– safe1 (If tst c1 c2 ) = (safe1 c1 ∧ safe1 c2 ∧ (minTp tst ≤ (maxTp1 c1 ∧ maxTp1 c2 )))
– maxTp1 (If tst c1 c2 ) = (maxTp1 c1 ∧ maxTp1 c2 )
– safe1 (While tst c) = (safe1 c ∧ (minTp tst = lo))
– maxTp1 (While tst c) = lo
– safe1 (Par c1 c2 ) = (safe1 c1 ∧ safe1 c2 )
– maxTp1 (Par c1 c2 ) = (maxTp1 c1 ∧ maxTp1 c2 )
Lemma 2. The following are equivalent:
(1) c ::1 l
(2) safe1 c and l ≤ maxTp1 c.
Proof idea: (1) implies (2): By easy induction on the definition of ::1 .
(2) implies (1): By easy structural induction on c.

⊓
⊔

Now, let us write:
– low e, for the sentence minTp e = lo
– low tst, for the sentence minTp tst = lo
– fhigh c (read “c finite and high"), for the sentence maxTp1 c = hi
(Thus, low : exp → bool, low : test → bool and fhigh : com → bool.)
Then, immediately from the definitions of minTp and maxTp1 (taking advantage of
the fact that L = {hi, lo}) we have the following:
– low e = (∀x ∈ Vars e. sec x = lo)
– low tst = (∀x ∈ Vars tst. sec x = lo)
– safe1 (x := e) = ((sec x = hi) ∨ low e)
– fhigh (x := e) = (sec x = hi)
– safe1 (Seq c1 c2 ) = (safe1 c1 ∧ safe1 c2 )
2

Notice the overloaded, but consistent usage of the infimum operator ∧ in both the lattice L =
{lo, hi} and the lattice of truth values bool (the latter simply meaning the logical “and").

– fhigh (Seq c1 c2 ) = (
fhigh c1 ∧ fhigh c2 )
safe1 c1 ∧ safe1 c2 ,
if low tst
– safe1 (If tst c1 c2 ) =
safe1 c1 ∧ safe c2 ∧ fhigh c1 ∧ fhigh c2 , otherwise
– fhigh (If tst c1 c2 ) = (fhigh c1 ∧ fhigh c2 )
– safe1 (While tst c) = (low tst ∧ safe1 c)
– fhigh (While tst c) = False
– safe1 (Par c1 c2 ) = (safe1 c1 ∧ safe1 c2 )
– low (Par c1 c2 ) = (low c1 ∧ low c2 )
Notice that the above clauses characterize the prediactes safe1 : com → bool and
fhigh : com → bool uniquely, i.e., could act as their definitions (recursively on the structure of commands). Since the predicate safe1 is stronger than fhigh (as its clauses are
strictly stronger), we can remove safe1 c1 ∧ safe c2 from the “otherwise" case of the If
clause for safe1 , obtaining:
– safe1 (If tst c1 c2 ) =



safe1 c1 ∧ safe1 c2 ,
fhigh c1 ∧ fhigh c2 ,

if low tst
=
otherwise



safe1 c1 ∧ safe1 c2 ,
fhigh (If tst c1 c2 ),

if low tst
otherwise

The clauses for safe1 and fhigh are now seen to coincide with our [7, 8, §6] clauses
for ≈WT and discr ∧ mayT, respectively, with the following variation: in [7, 8, §6] we do
not commit to particular forms of tests or atomic statements, and therefore replace:
– low tst with cpt tst
– fhigh atm with pres atm (where atm is an atom, such as x := e)
– safe1 atm with cpt atm
Note that the predicates cpt and pres, as defined in [7, 8, §4], are semantic conditions
expressed in terms of state indistinguishability, while low, fhigh and safe1 are syntactic checks. than syntactic checks as here—the syntactic checks are easyly seen to be
stronger, i.e., we have low tst =⇒ cpt tst, fhigh atm =⇒ pres atm and safe1 atm =⇒ cpt atm.
The main concurrent noninterference result from [11], Corollary 5.7, states (something
slightly weaker than) the following: if c ::1 l for some l ∈ L, then c ≈WT c. In the light of
Lemma 2 and the above discussion, this result is subsumed by our Prop. 4 from [7, 8],
taking χ to be ≈WT.
For the rest of the type systems we discuss, we shall proceed with similar transformations at a higher pace.
1.2 Volpano-Smith scheduler-independent noninterference
In [11, §7], another type system is defined, ::2 , which has the same typing rules as ::1
except for the rule for If, which is weakened by requiring the typing of the test to be lo:3
tst :: lo c1 ::2 l c2 ::2 l
(IF)
(If tst c1 c2 ) ::2 l
3

The same type system (except for the (PAR) rule) is introduced in [12] for a sequential language
with the purpose of preventing leaks through the covert channels of termination and exceptions.

Definition 2. We define safe2 just like safe1 , except for the case of If, which becomes:
– safe2 (If tst c1 c2 ) = ((minTp tst = lo) ∧ safe2 c1 ∧ safe2 c2 )
Similarly to Lemma 2, we can prove:
Lemma 3. The following are equivalent:
(1) c ::2 l
(2) safe2 c and l ≤ maxTp1 c.
If,

The inferred clauses for safe2 are the same as those for safe1 , except for the one for
which becomes:
– safe2 (If tst c1 c2 ) = (low tst ∧ safe2 c1 ∧ safe2 c2 )
Then safe2 is seen to coincide with siso from [7, 8, §6].

In [11] it is proved (via Theorem 7.1) that the soundness result for ::1 also holds for ::2 .
In fact, one can see that Theorem 7.1 can be used to prove something much stronger:
if c ::2 l for some l ∈ L, then siso c. This result is subsumed by our Prop. 4 from [7, 8],
taking χ to be siso.
1.3 Boudol-Castellani termination-insensitive noninterference
As we already discussed in [7, 8], Boudol and Castellani [3, 4] work on improving the
harsh Vopano-Smith typing of While (which requires low tests), but they pay a (comparatively small) price in terms of typing sequential composition, where what the first
command reads is required to be below what the second command writes. (Essentially
the same type system is introduced independently by Smith [9, 10] for studying probabilistic noninterference in the presence of uniform scheduling. Boudol and Castellani,
as well as Smith, consider parallel composition only at the top level. Barthe and Nieto [1] raise this restriction, allowing nesting Par inside other language constructs, as
we do here.)
To achieve this, they type commands c to a pair of security levels (l, l ′ ): the contravariant “write" type l (similar to the Volpano-Smith one) and an extra covariant
“read" type l ′ .
sec x = l e :: l
(ASSIGN)
(x := e) ::2 (l, l ′ )
tst :: l0

c1 ::3 (l1 , l1′ ) c2 ::3 (l2 , l2′ ) l1′ ≤ l2
(COMPOSE)
(Seq c1 c2 ) ::3 (l1 ∧ l2 , l1′ ∨ l2′ )

c1 ::3 (l, l ′ ) c2 ::3 (l, l ′ )
(If tst c1 c2 ) ::3 (l, l0 ∨ l ′ )

c1 ::3 l c2 ::3 l
(PAR)
(Par c1 c2 ) ::3 l
We think of c ::3 (l, l ′ ) as saying:
– There is no downwards flow in c.

l0 ≤ l

(IF)

tst :: l ′ c ::3 (l, l ′ ) l ′ ≤ l
(WHILE)
(While tst c) ::3 (l, l ′ )

c ::3 (l1 , l1′ ) l2 ≤ l1
c ::3 (l2 , l2′ )

l1′ ≤ l2′

(SUBTYPE)

– l is a lower bound on the level of the variables that the execution of c writes to.
– l ′ is an upper bound on the level of the variables that c reads, more precisely, that
the control flow of the execution of c depends on.
(This intuition is accurately reflected by Lemma 4 below.)
In [3, 4], the rule for While is slightly different, namely:
tst :: l0 c ::3 (l, l ′ ) l0 ∨ l ′ ≤ l
(WHILE’)
(While tst c) ::3 (l, l0 ∨ l ′ )
However, due to subtyping, it is easily seen to be equivalent to the one we listed. Indeed:
– (WHILE) is an instance of (WHILE’) taking l0 = l ′ .
– Conversely, (WHILE’) follows from (WHILE) as follows: Assume the hypotheses
of (WHILE’). By subtyping, we have tst :: l0 ∨ l ′ and c ::3 (l, l0 ∨ l ′ ), hence, by
(WHILE), we have (While tst c) ::3 (l, l0 ∨ l ′ ), as desired.
Following for ::3 the same technique as in the case of ::1 and ::2 , we define the
functions maxWtp : com → L (read “maximum writing type") and minRtp : com → L
(read “minimum reading type") and the predicate safe3 : com → bool:
Definition 3. – safe3 (x := e) = (minTp e ≤ sec x)
– maxWtp (x := e) = sec x
– minRtp (x := e) = lo
– safe3 (Seq c1 c2 ) = (safe3 c1 ∧ safe3 c2 ∧ (minRtp c1 ≤ maxWtp c2 ))
– maxWtp (Seq c1 c2 ) = (maxWtp c1 ∧ maxWtp c2 )
– minRtp (Seq c1 c2 ) = (minRtp c1 ∨ minRtp c2 )
– safe3 (If tst c1 c2 ) = (safe3 c1 ∧ safe3 c2 ∧ (minTp tst ≤ (maxWtp c1 ∧ maxWtp c2 )))
– maxWtp (If tst c1 c2 ) = (maxWtp c1 ∧ maxWtp c2 )
– minRtp (If tst c1 c2 ) = (minTp tst ∨ minRtp c1 ∨ minRtp c2 )
– safe3 (While tst c) = (safe3 c ∧ ((minTp tst ∨ minRtp c) ≤ maxWtp c))
– maxWtp (While tst c) = maxWtp c
– minRtp (While tst c) = (minTp tst ∨ minRtp c)
– safe3 (Par c1 c2 ) = (safe3 c1 ∧ safe3 c2 )
– maxWtp (Par c1 c2 ) = (maxWtp c1 ∧ maxWtp c2 )
– minRtp (Par c1 c2 ) = (minRtp c1 ∨ minRtp c2 )
Furthermore, similarly to the cases of safe1 and safe2 , we have that:
Lemma 4. The following are equivalent:
(1) c ::3 (l, l ′ )
(2) safe3 c and l ≤ maxWtp c and minRtp c ≤ l ′ .
Now, let us write:
– high c, for the sentence maxWtp c = hi
– low c, for the sentence minRtp c = lo

Then, immediately from the definitions of maxWtp and minRtp, we have the following:
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–

safe3 (x := e) = ((sec x = hi) ∨ low e)
high (x := e) = (sec x = hi)
low (x := e) = True
safe3 (Seq c1 c2 ) = (safe3 c1 ∧ safe3 c2 ∧ (low c1 ∨ high c2 ))
high (Seq c1 c2 ) = (high c1 ∧ high c2 )
low (Seq c1 c2 ) = (low c1 ∧ low c2 )
safe3 (If tst c1 c2 ) = (safe3 c1 ∧ safe3 c2 ∧ (low tst ∨ (high c1 ∧ high c2 )))
high (If tst c1 c2 ) = (high c1 ∧ high c2 )
low (If tst c1 c2 ) = (low tst ∧ low c1 ∧ low c2 )
safe3 (While tst c) = (safe3 c ∧ ((low tst ∧ low c) ∨ high c))
high (While tst c) = high c
low (While tst c) = (low tst ∧ low c)
safe3 (Par c1 c2 ) = (safe3 c1 ∧ safe3 c2 )
high (Par c1 c2 ) = (high c1 ∧ high c2 )
low (Par c1 c2 ) = (low c1 ∧ low c2 )

Then high and low are stronger than safe3 , and hence we can rewrite the Seq, If and
clauses for safe3 as follows:

While

– safe3 (Seq c1 c2 ) = 
((low c1 ∧ safe3 c2 ) ∨ (safe3 c1 ∧ highc2 ))
safe3 c1 ∧ safe3 c2 , if low tst
safe3 c1 ∧ safe3 c2 , if low tst
– safe3 (If tst c1 c2 ) =
=
high c1 ∧ high c2 ,
otherwise
high (If tst c1 c2 ), otherwise
– safe3 (While tst c) = ((low tst ∧ low c) ∨ high c) = (low (While tst c) ∨ high (While tst c))
The clauses for safe3 , high and low are now seen to coincide with our [7,8, §6] clauses
for ≈01 and discr and siso, respectively.
The main concurrent noninterference result from [3, 4] (Theorem 3.13 in [3] and Theorem 3.16 in [4]), states (something slightly weaker than) the following: if c ::3 l for
some l ∈ L, then c ≈01 c. In the light of Lemma 4 and the above discussion, this result
is subsumed by our Prop. 4 from [7, 8], taking χ to be ≈01.
1.4 Matos and Boudol’s further improvement
Mantos and Boudol [2, 5, 6] study a richer language than the one we consider here,
namely, an ML-like language. Moreover, they also consider a declassification construct. We shall ignore these extra features and focus on the restriction of their results
to our simple while language. Moreover, they parameterize their development by a set
of strongly terminating expressions (commands in our setting)—here we fix this set to
be that of commands not containing while loops.
The type system ::4 from [2,5,6] is based on a refinement of ::3 , noticing that, as far
as the reading type goes, one does not care about all variables a command reads (i.e.,
the variables that affect the control flow of its execution), but can restrict attention to
those that may affect the termination of its execution.
The typing rules of ::4 are identical to those of ::3 , except for the If rule, which
becomes:

tst :: l0


c1 ::3 (l, l ′ ) c2 ::3 (l, l ′ )
(If tst c1 c2 ) ::3 (l, k)

l0 ≤ l

(IF)

if c1 , c2 do not contain While subexpressions
l0 ∨ l ′ , otherwise
We think of c ::4 (l, l ′ ) as saying:

where k =

lo,

– There is no downwards flow in c.
– l is a lower bound on the level of the variables that the execution of c writes to.
– l ′ is an upper bound on the level of the variables that c termination-reads, i.e., that
termination of the execution of c depends on.
(In [2, 5, 6], While is not a primitive, but is derived from higher-order recursion—
however, the effect of the higher-order typing system on While is the same as that of our
::3 , as shown in [6]. Moreover, due to working in a functional language with side effects,
[2, 5, 6] record not two, but three security types: in addition to our l and l ′ (called there
the writing and termination effects, respectively), they also record l ′′ (called there the
reading effect) which represents an upper bound on the security levels of variables the
returned value of c depends on—here, this information is unnecessary, since c returns
no value.)
Definition 4. We define the function minTRtp : com → L (read “minimum terminationreading type") and the predicate safe4 : com → bool as follows: minTRtp is defined using
the same recursive clauses as minRtp, except for the clause for If, which becomes:
– 
minTRtp (If tst c1 c2 ) =
lo,
if c1 , c2 do not contain While subexpressions
minTp tst ∨ minTRtp c1 ∨ minTRtp c2 , otherwise
safe4

is defined using the same clauses as safe3 with minTRtp replacing minRtp.

Lemma 5. The following are equivalent:
(1) c ::4 (l, l ′ )
(2) safe4 c and l ≤ maxWtp c and minTRtp c ≤ l ′ .
Now, let us write:
– wlow c (read “c has low tests on top of while subexpressions"), for the sentence
minTRtp c = lo
– noWhile c, for the sentence “c contains no While subexpressions"
We obtain:
–
–
–
–
–

safe4 (x := e) = ((sec x = hi) ∨ low e)
wlow (x := e) = True
safe4 (Seq c1 c2 ) = (safe4 c1 ∧ safe4 c2 ∧ (wlow c1 ∨ high c2 ))
wlow (Seq c1 c2 ) = (wlow c1 ∧ wlow c2 )
safe4 (If tst c1 c2 ) = (safe4 c1 ∧ safe4 c2 ∧ (wlow tst ∨ (high c1 ∧ high c2 )))

–
–
–
–
–

wlow (If tst c1 c2 ) = (low tst ∧ wlow c1 ∧ wlow c2 ) ∨ (noWhile c1 ∧ noWhile c2 )
safe4 (While tst c) = (safe4 c ∧ ((low tst ∧ low c) ∨ high c))
wlow (While tst c) = (low tst ∧ wlow c)
safe4 (Par c1 c2 ) = (safe4 c1 ∧ safe4 c2 )
wlow (Par c1 c2 ) = (wlow c1 ∧ wlow c2 )

We can prove by induction on c that safe1 c = (safe4 c ∧ wlow c) Using this, we
rewrite the Seq, If and While clauses for safe4 as follows:
– safe4 (Seq c1 c2 ) = ((
safe1 c1 ∧ safe4 c2 ) ∨ (safe4 c1 ∧ high c2 ))
safe4 c1 ∧ safe4 c2 , if low tst
– safe4 (If tst c1 c2 ) =
high (If tst c1 c2 ), otherwise
– safe4 (While tst c) = (safe1 (While tst c) ∨ high (While tst c))
Then safe4 turns out to coincide with our ≈W from [7, 8, §6].
The main noninterference result from [2, 5, 6] (in [2], the soundness theorem in §5),
states the following: if c ::4 l for some l ∈ L, then c ≈W c. In the light of Lemma 4 and
the above discussion, this result is subsumed by our Prop. 4 from [7, 8], taking χ to be
≈W.

References
1. G. Barthe and L. P. Nieto. Formally verifying information flow type systems for concurrent
and thread systems. In FMSE, pages 13–22, 2004.
2. G. Boudol. On typing information flow. In ICTAC, pages 366–380, 2005.
3. G. Boudol and I. Castellani. Noninterference for concurrent programs. In ICALP, pages
382–395, 2001.
4. G. Boudol and I. Castellani. Noninterference for concurrent programs and thread systems.
Theoretical Computer Science, 281(1-2):109–130, 2002.
5. A. A. Matos and G. Boudol. On declassification and the non-disclosure policy. In CSFW,
pages 226–240, 2005.
6. A. A. Matos and G. Boudol. On declassification and the non-disclosure policy. Journal of
Computer Security, 17(5):549–597, 2009.
7. A. Popescu, J. Hölzl, and T. Nipkow. Proving concurrent noninterference. In CPP, pages
109–125, 2012.
8. A. Popescu, J. Hölzl, and T. Nipkow. Formal verification of concurrent noninterference.
Journal of Formalized Reasoning, 2013. Extended version of [7]. To appear.
9. G. Smith. A new type system for secure information flow. In IEEE Computer Security
Foundations Workshop, pages 115–125, 2001.
10. G. Smith. Probabilistic noninterference through weak probabilistic bisimulation. In IEEE
Computer Security Foundations Workshop, pages 3–13, 2003.
11. G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language.
In ACM Symposium on Principles of Programming Languages, pages 355–364, 1998.
12. D. M. Volpano and G. Smith. Eliminating covert flows with minimum typings. In CSFW,
pages 156–169, 1997.

