Slot Games for Detecting Timing Leaks of Programs
Aleksandar S. Dimovski
Faculty of Information-Communication Tech., FON University, Skopje, 1000, MKD
aleksandar.dimovski@fon.edu.mk

In this paper we describe a method for verifying secure information flow of programs, where apart
from direct and indirect flows a secret information can be leaked through covert timing channels. That
is, no two computations of a program that differ only on high-security inputs can be distinguished by
low-security outputs and timing differences. We attack this problem by using slot-game semantics
for a quantitative analysis of programs. We show how slot-games model can be used for performing
a precise security analysis of programs, that takes into account both extensional and intensional
properties of programs. The practicality of this approach for automated verification is also shown.

1

Introduction

Secure information flow analysis is a technique which performs a static analysis of a program with the
goal of proving that it will not leak any sensitive (secret) information improperly. If the program passes
the test, then we say that it is secure and can be run safely. There are several ways in which secret
information can be leaked to an external observer. The most common are direct and indirect leakages,
which are described by the so-called non-interference property [13, 18]. We say that a program satisfies
the non-interference property if its high-security (secret) inputs do not affect its low-security (public)
outputs, which can be seen by external observers.
However, a program can also leak information through its timing behaviour, where an external observer can measure its total running time. Such timing leaks are difficult to detect and prevent, because
they can exploit low-level implementation details. To detect timing leaks, we need to ensure that the total
running time of a program do not depend on its high-security inputs.
In this paper we describe a game semantics based approach for performing a precise security analysis. We have already shown in [8] how game semantics can be applied for verifying the non-interference
property. Now we use slot-game semantics to check for timing leaks of closed and open programs. We
focus here only on detecting covert timing channels, since the non-interference property can be verified
similarly as in [8]. Slot-game semantics was developed in [11] for a quantitative analysis of Algollike programs. It is suitable for verifying the above security properties, since it takes into account both
extensional (what the program computes) and intensional (how the program computes) properties of programs. It represents a kind of denotational semantics induced by the theory of operational improvement
of Sands [19]. Improvement is a refinement of the standard theory of operational approximation, where
we say that one program is an improvement of another if its execution is more efficient in any program
context. We will measure efficiency of a program as the sum of costs associated with basic operations
it can perform. It has been shown that slot-game semantics is fully abstract (sound and complete) with
respect to operational improvement, so we can use it as a denotational theory of improvement to analyse
programming languages.
The advantages of game semantics (denotational) based approach for verifying security are several.
We can reason about open programs, i.e. programs with non-locally defined identifiers. Moreover, game
semantics is compositional, which enables analysis about program fragments to be combined into an
Gabriele Puppis, Tiziano Villa (Eds.): Fourth International
Symposium on Games, Automata, Logics and Formal Verification
EPTCS 119, 2013, pp. 166–179, doi:10.4204/EPTCS.119.15

c A. S. Dimovski
This work is licensed under the
Creative Commons Attribution License.

A. S. Dimovski

167

analysis of a larger program. Also the model hides the details of local-state manipulation of a program,
which results in small models with maximum level of abstraction where are represented only visible
input-output behaviours enriched with costs that measure their efficiency. All other behaviour is abstracted away, which makes this model very suitable for security analysis. Finally, the game model for
some language fragments admits finitary representation by using regular languages or CSP processes
[10, 6], and has already been applied to automatic program verification. Here we present another application of algorithmic game semantics for automatically verifying security properties of programs.
Related work. The most common approach to ensure security properties of programs is by using
security-type systems [14]. Here for every program component are defined security types, which contain
information about their types and security levels. Programs that are well-typed under these type systems
satisfy certain security properties. Type systems for enforcing non-interference of programs have been
proposed by Volpano and Smith in [20], and subsequently they have been extended to detect also covert
timing channels in [21, 2]. A drawback of this approach is its imprecision, since many secure programs
are not typable and so are rejected. A more precise analysis of programs can be achieved by using
semantics-based approaches [15].

2

Syntax and Operational Semantics

We will define a secure information flow analysis for Idealized Algol (IA), a small Algol-like language
introduced by Reynolds [16] which has been used as a metalanguage in the denotational semantics community. It is a call-by-name λ -calculus extended with imperative features and locally-scoped variables.
In order to be able to perform an automata-theoretic analysis of the language, we consider here its secondorder recursion-free fragment (IA2 for short). It contains finitary data types D: intn = {0, . . . , n − 1} and
bool = {tt, ff }, and first-order function types: T ::= B | B → T, where B ranges over base types: expressions (expD), commands (com), and variables (varD).
Syntax of the language is given by the following grammar:
M ::=x | v | skip | diverge | M op M | M; M | if M thenM else M | while M do M
| M := M |!M | newD x := v in M | mkvarD MM | λ x.M | MM
where v ranges over constants of type D.
Typing judgements are of the form Γ ⊢ M : T, where Γ is a type context consisting of a finite number
of typed free identifiers. Typing rules of the language are standard [1], but the general application rule is
broken up into the linear application and the contraction rule 1 .
Γ⊢M:B→T
∆⊢N:B
Γ, ∆ ⊢ MN : T

Γ, x1 : T, x2 : T ⊢ M : T ′
Γ, x : T ⊢ M[x/x1 , x/x2 ] : T ′

We use these two rules to have control over multiple occurrences of free identifiers in terms during
typing.
Any input/output operation in a term is done through global variables, i.e. free identifiers of type
varD. So an input is read by de-referencing a global variable, while an output is written by an assignment
to a global variable.
1

M[N/x] denotes the capture-free substitution of N for x in M.

Slot Games for Detecting Timing Leaks of Programs

168
Γ ⊢ n1 op n2 , s −→kop n, s, where n = n1 opn2
Γ ⊢ skip; skip, s −→kseq skip, s′
Γ ⊢ if tt then M1 elseM2 , s −→kif M1 , s
Γ ⊢ if ff then M1 elseM2 , s −→kif M2 , s
Γ ⊢ x := v′ , s ⊗ (x 7→ v) −→kasg skip, s ⊗ (x 7→ v′ )
Γ ⊢!x, s ⊗ (x 7→ v) −→kder v, s ⊗ (x 7→ v)
Γ ⊢ (λ x.M)M ′ , s −→kapp M[M ′ /x], s
Γ ⊢ newD x := v in skip, s −→knew skip, s

Table 1: Basic Reduction Rules
The operational semantics is defined in terms of a small-step evaluation relation using a notion of an
evaluation context [9]. A small-step evaluation (reduction) relation is of the form:
Γ ⊢ M, s −→ M ′ , s′
where Γ is a so-called var-context which contains only identifiers of type varD; s, s′ are Γ-states which
assign data values to the variables in Γ; and M, M ′ are terms. The set of all Γ-states will be denoted by
St(Γ).
Evaluation contexts are contexts 2 containing a single hole which is used to identify the next sub-term
to be evaluated (reduced). They are defined inductively by the following grammar:
E ::= [−] | EM | E; M | skip; E | E op M | v op E | if E then M else M | M := E | E := v |!E
The operational semantics is defined in two stages. First, a set of basic reduction rules are defined
in Table 1. We assign different (non-negative) costs to each reduction rule, in order to denote how much
computational time is needed for a reduction to complete. They are only descriptions of time and we can
give them different interpretations describing how much real time they denote. Such an interpretation
can be arbitrarily complex. So the semantics is parameterized on the interpretation of costs. Notice that
we write s ⊗ (x 7→ v) to denote a {Γ, x}-state which properly extends s by mapping x to the value v.
We also have reduction rules for iteration, local variables, and mkvarD construct, which do not incur
additional costs.
Γ ⊢ while b do M, s −→ if b then (M; while b do M) else skip, s
Γ, y ⊢ M[y/x], s ⊗ (y 7→ v) −→ M ′ , s′ ⊗ (y 7→ v′ )
Γ ⊢ newD x := v in M, s −→ newD x := v′ in M ′ [x/y], s′
Γ ⊢ (mkvar D M1 M2 ) := v, s −→ M1 v, s
Γ ⊢!(mkvarD M1 M2 ), s −→ M2 , s
Next, the in-context reduction rules for arbitrary terms are defined as:
Γ ⊢ M, s −→n M ′ , s′
Γ ⊢ E[M], s −→n E[M ′ ], s′
The small-step evaluation relation is deterministic, since arbitrary term can be uniquely partitioned into
an evaluation context and a sub-term, which is next to be reduced.
We define the reflexive and transitive closure of the small-step reduction relation as follows:
2 A context C[−] is a term with (several occurrences of) a hole in it, such that if Γ ⊢ M : T is a term of the same type as the
hole then C[M] is a well-typed closed term of type com, i.e. ⊢ C[M] : com.

A. S. Dimovski

169
′

Γ ⊢ M, s −→n M ′ , s′
Γ ⊢ M, s n M ′ , s′
Γ ⊢ M ′ , s′ n M ′′ , s′′
′
n
′
′
Γ ⊢ M, s
M ,s
Γ ⊢ M, s n+n M ′′ , s′′
Now a theory of operational improvement is defined [19]. Let Γ ⊢ M : com be a term, where Γ is a
var-context. We say that M terminates in n steps at state s, written M, s ⇓n , if Γ ⊢ M, s n skip, s′ for
some state s′ . If M is a closed term and M, 0/ ⇓n , then we write M ⇓n . If M ⇓n and n ≤ n′ , we write
′
M ⇓≤n . We say that a term Γ ⊢ M : T may be improved by Γ ⊢ N : T, denoted by Γ ⊢ M & N, if and only
if for all contexts C[−], if C[M] ⇓n then C[N] ⇓≤n . If two terms improve each other they are considered
improvment-equivalent, denoted by Γ ⊢ M ≈ N.
Let Γ, ∆ ⊢ M : T be a term where Γ is a var-context and ∆ is an arbitrary context. Such terms are
called split terms, and we denote them as Γ | ∆ ⊢ M : T. If ∆ is empty, then these terms are called semiclosed. The semi-closed terms have only some global variables, and the operational semantics is defined
only for them. We say that a semi-closed term h : varD | − ⊢ M : com does not have timing leaks if the
initial value of the high-security variable h does not influence the number of reduction steps of M. More
formally, we have:
Definition 1. A semi-closed term h : varD | − ⊢ M : com has no timing leaks if
∀ s1 , s2 ∈ St({h}). s1 (h) 6= s2 (h) ∧
h : varD ⊢ M, s1
⇒ n1 = n2

n1

skip, s1 ′ ∧ h : varD ⊢ M, s2

n2

skip, s2 ′

(1)

Definition 2. We say that a split term h : varD | ∆ ⊢ M : com does not have timing leaks, where ∆ =
x1 : T1 , . . . , xk : Tk , if for all closed terms ⊢ N1 : T1 , . . . , ⊢ Nk : Tk , we have that the term h : varD | − ⊢
M[N1 /x1 , . . . , Nk /xk ] : com does not have timing leaks.
The formula (1) can be replaced by an equivalent formula, where instead of two evaluations of the
same term we can consider only one evaluation of the sequential composition of the given term with
another its copy [3]. So sequential composition enables us to place these two evaluations one after the
other. Let h : varD ⊢ M : com be a term, we define M ′ to be α -equivalent to M[h′ /h] where all bound vari′
ables are suitable renamed. The following can be shown: h ⊢ M, s1 n skip, s1 ′ ∧ h′ ⊢ M ′ , s2 n skip, s2 ′
′
iff h, h′ ⊢ M; M ′ , s1 ⊗ s2 n+n skip; skip, s1 ′ ⊗ s2 ′ . In this way, we provide an alternative definition to
formula (1) as follows. We say that a semi-closed term h | − ⊢ M : T has no timing leaks if
∀ s1 ∈ St({h}), s2 ∈ St({h′ }).

s1 (h) 6= s2 (h′ ) ∧
h, h′ ⊢ M; M ′ , s1 ⊗ s2
⇒ n1 = n2

n1

skip; M ′ , s1 ′ ⊗ s2

n2

skip; skip, s1 ′ ⊗ s2 ′
(2)

3

Algorithmic Slot-Game Semantics

We now show how slot-game semantics for IA2 can be represented algorithmically by regular-languages.
In this approach, types are interpreted as games, which have two participants: the Player representing
the term, and the Opponent representing its context. A game (arena) is defined by means of a set of
moves, each being either a question move or an answer move. Each move represents an observable
action that a term of a given type can perform. Apart from moves, another kind of action, called token
(slot), is used to take account of quantitative aspects of terms. It represents a payment that a participant
needs to pay in order to use a resource such as time. A computation is interpreted as a play-withcosts, which is given as a sequence of moves and token-actions played by two participants in turns.

Slot Games for Detecting Timing Leaks of Programs

170

We will work here with complete plays-with-costs which represent the observable effects along with
incurred costs of a completed computation. Then a term is modelled by a strategy-with-costs, which
is a set of complete plays-with-costs. In the regular-language representation of game semantics [10],
types (arenas) are expressed as alphabets of moves, computations (plays-with-costs) as words, and terms
(strategies-with-costs) as regular-languages over alphabets.
Each type T is interpreted by an alphabet of moves A[[T]] , which can be partitioned into two subsets
of questions Q[[T]] and answers A[[T]] . For expressions, we have: Q[[expD]] = {q} and A[[expD]] = D, i.e. there
are a question move q to ask for the value of the expression and values from D are possible answers.
For commands, we have: Q[[com]] = {run} and A[[com]] = {done}, i.e. there are a question move run
to initiate a command and an answer move done to signal successful termination of a command. For
variables, we have: Q[[varD]] = {read, write(a) | a ∈ D} and A[[varD]] = D ∪ {ok}, i.e. there are moves
for writing to the variable, write(a), acknowledged by the move ok, and for reading from the variable,
we have a question move read, and an answer to it can be any value from D. For function types, we
i +A
have A[[B1 →...→Bk →B]] = ∑1≤i≤k A[[B
[[B]] , where + means a disjoint union of alphabets. We will use
i ]]
1
k
superscript tags to keep record from which type of the disjoint union each move comes from. We denote
the token-action by $ . A sequence of n token-actions $ will be written as n .
For any (β -normal) term we define a regular language specified by an extended regular expression R.
Apart from the standard operations for generating regular expressions, we will use some more specific
operations. We define composition of regular expressions R defined over alphabet A 1 + B 2 + { $ } and
S over B 2 + C 3 + { $ } as follows:


R 9oB2 S = {w s/a2 · b2 | w ∈ S, a2 · s · b2 ∈ R}
where R is a set of words of the form a2 · s · b2 , such that a2 , b2 ∈ B 2 and s contains only letters from A 1
and { $ }. Notice that the composition is defined over A 1 + C 3 + { $ }, and all letters of B 2 are hidden.
The shuffle operation R ⊲⊳ S generates the set of all possible interleavings from words of R and S, and
the restriction operation R |A ′ (R defined over A and A ′ ⊆ A ) removes from words of R all letters from
A ′.
If w, w′ are words, m is a move, and R is a regular expression, define m · w a w′ = m · w′ · w, and
R a w′ = {w a w′ | w ∈ R}. Given a word with costs w defined over A + { $ }, we define the underlying
word of w as w† = w |{ $ } , and the cost of w as w |A = n , which we denote as | w |= n.
The regular expression for Γ ⊢ M : T is denoted [[Γ ⊢ M : T]] and is defined over the alphabet A[[Γ⊢T]] =
∑x:T ′ ∈Γ A[[Tx ′ ]] + A[[T]] + { $ }. Every word in [[Γ ⊢ M : T]] corresponds to a complete play-with-costs in
the strategy-with-costs for Γ ⊢ M : T.
Free identifiers x ∈ Γ are interpreted by the copy-cat regular expressions, which contain all possible
computations that terms of that type can have. Thus they provide the most general closure of an open
term.
x,k
x
1
k
[[Γ, x : Bx,1
1 → . . . Bk → B ⊢ x : B1 → . . . Bk → B]] =
i
x
∑ q · q · ∑ ( ∑ qx,i
1 · q1 ·
q∈Q[[B]]

1≤i≤k q1 ∈Q[[Bi ]]

∑

∗
ai1 · ax,i
1 ) ·

a1 ∈A[[Bi ]]

∑

ax · a

a∈A[[B]]

When a first-order non-local function is called, it may evaluate any of its arguments, zero or more times,
and then it can return any value from its result type as an answer. For example, the term [[Γ, x : expDx ⊢
x : expD]] is modelled by the regular expression: q · qx · ∑n∈D nx · n.
The linear application is defined as:
[[Γ, ∆ ⊢ M N : T]] = [[∆ ⊢ N : B1 ]] o9A 1 [[Γ ⊢ M : B1 → T]]
[[B]]

A. S. Dimovski

171

Since we work with terms in β -normal form, function application can occur only when the function term
is a free identifier. In this case, the interpretation is the same as above except that we add the cost kapp
corresponding to function application. Notice that kapp denotes certain number of $ units that are needed
for a function application to take place. The contraction [[Γ, x : T x ⊢ M[x/x1 , x/x2 ] : T ′ ]] is obtained from
[[Γ, x1 : T x1 , x2 : T x2 ⊢ M : T ′ ]], such that the moves associated with x1 and x2 are de-tagged so that they
represent actions associated with x.
To represent local variables, we first need to define a (storage) ‘cell’ regular expression cellv which
imposes the good variable behaviour on the local variable. So cellv responds to each write(n) with ok,
and plays the most recently written value in response to read, or if no value has been written yet then
answers the read with the initial value v. Then we have:
∗
cellv = (read · v)∗ · ∑ write(n) · ok · (read · n)∗
n∈D

x
[[Γ, x : varD ⊢ M]] ◦ cellxv = [[Γ, x : varD ⊢ M]] ∩ (cellxv ⊲⊳ (A[[Γ⊢B]] + $ )∗ ) |A[[varD]]
x
[[Γ ⊢ newD x := v in M]] = [[Γ, x : varD ⊢ M]] ◦ cellv a kvar
Note that all actions associated with x are hidden away in the model of new, since x is a local variable
and so not visible outside of the term.
Language constants and constructs are interpreted as follows:
[[v : expD]] = {q · v} [[skip : com]] = {run · done} [[diverge : com]] = 0/
[[op : expD1 × expD2 → expD′ ]] = q · kop · q1 · ∑m∈D m1 · q2 · ∑n∈D n2 ·(m op n)
[[; : com1 → com2 → com]] = run · run1 · done1 · kseq · run2 · done2 · done
[[if : expbool1 → com2 → com3 → com]] = run · kif · q1 · tt1 · run2 · done2 · done +
run · kif · q1 · ff 1 · run3 · done3 · done
[[while : expbool1 → com2 → com]] = run · (kif · q1 · tt1 · run2 · done2 )∗ · kif · q1 · ff 1 · done
[[:=: varD1 → expD2 → com]] = ∑n∈D run · kasg · q2 · n2 · write(n)1 · ok1 · done
[[! : varD1 → expD]] = ∑n∈D q · kder · read1 · n1 · n
Although it is not important at what position in a word costs are placed, for simplicity we decide to attach
them just after the initial move. The only exception is the rule for sequential composition (; ), where the
cost is placed between two arguments. The reason will be explained later on.
We now show how slot-games model relates to the operational semantics. First, we need to show
how to represent the state explicitly in the model. A Γ-state s is interpreted as follows:
k
1
[[s : varDx11 × . . . × varDxkk ]] = cellxs(x
⊲⊳ . . . ⊲⊳ cellxs(x
1)
k)

xk
x1
, and words in [[s]] are
The regular expression [[s]] is defined over the alphabet A[[varD
+ . . . + A[[varD
1 ]]
k ]]
such that projections onto xi -component are the same as those of suitable initialized cells(xi ) strategies.
Note that [[s]] is a regular expression without costs. The interpretation of Γ ⊢ M : com at state s is:

[[Γ ⊢ M]] ◦ [[s]] = [[Γ ⊢ M]] ∩ ([[s]] ⊲⊳ (A[[com]] + $ )∗ ) |A[[Γ]]

which is defined over the alphabet A[[com]] + { $ }. The interpretation [[Γ ⊢ M]] ◦ [[s]] can be studied
more closely by considering words in which moves from A[[Γ]] are not hidden. Such words are called
interaction sequences. For any interaction sequence run · t · done ⊲⊳ n from [[Γ ⊢ M]] ◦ [[s]], where t
is an even-length word over A[[Γ]] , we say that it leaves the state s′ if the last write moves in each xi component are such that xi is set to the value s′ (xi ). For example, let s = (x 7→ 1, y 7→ 2), then the

Slot Games for Detecting Timing Leaks of Programs

172

following interaction: run · write(5)y · oky · readx · 1x · done leaves the state s′ = (x 7→ 1, y 7→ 5). Any twomove word of the form: runxi · nxi or write(n)xi · okxi will be referred to as atomic state operation of A[[Γ]] .
The following results are proved in [11] for the full ICA (IA plus parallel composition and semaphores),
but they also hold for the restricted fragment of it.
Proposition 1. If Γ ⊢ M : {com, expD} and Γ ⊢ M, s −→n M ′ , s′ , then for each interaction sequence i · t
from [[Γ ⊢ M ′ ]] ◦ [[s′ ]] (i is an initial move) there exists an interaction i · ta · t a n ∈ [[Γ ⊢ M]] ◦ [[s]] such
that ta is an empty word or an atomic state operation of A[[Γ]] which leaves the state s′ .
Proposition 2. If Γ ⊢ M, s

n

M ′ , s′ then [[Γ ⊢ M ′ ]] ◦ [[s′ ]] ⊲⊳ n ⊆ [[Γ ⊢ M]] ◦ [[s]].

Theorem 1 (Consistency). If M, s ⇓n then ∃ w ∈ [[Γ ⊢ M]] ◦ [[s]] such that | w |= n and w† = run · done .
Theorem 2 (Computational Adequacy). If ∃ w ∈ [[Γ ⊢ M]] ◦ [[s]] such that | w |= n and w† = run · done,
then M, s ⇓n .
w†

We say that a regular expression R is improved by S, denoted as R & S, if ∀ w ∈ R, ∃ t ∈ S, such that
= t† and | w |≥| t |.

Theorem 3 (Full Abstraction). Γ ⊢ M & N iff [[Γ ⊢ M]] & [[Γ ⊢ N]].
This shows that the two theories of improvement based on operational and game semantics are identical.

4

Detecting Timing Leaks

In this section slot-game semantics is used to detect whether a term with a secret global variable h can
leak information about the initial value of h through its timing behaviour.
For this purpose, we define a special command skip# which similarly as skip does nothing, but its
slot-game semantics is: [[skip# ]] = {run · # · done}, where # is a new special action, called delimiter.
Since we verify security of a term by running two copies of the same term one after the other, we will
use the command skip# to specify the boundary between these two copies. In this way, we will be able
to calculate running times of the two terms separately.
Theorem 4. Let h : varD | − ⊢ M : com be a semi-closed term, and 3
R = [[k : expD ⊢ newD h := k in M; skip# ; newD h′ := k in M ′ : com]]

(3)

Any word of R is of the form w = w1 · # · w2 such that | w1 |=| w2 | iff M has no timing leaks, i.e. the fact
(2) holds.
Proof. Suppose that any word w ∈ R is of the form w = w1 · # · w2 such that | w1 |=| w2 |. Let us analyse
the regular expression R defined in (3). We have:
R = {run · kvar · qk · vk · w1 · kseq · # · kseq · kvar · qk · v′k · w2 · done |
′
run · w1 · done ∈ [[h ⊢ M]] ◦ cellhv , run · w2 · done ∈ [[h′ ⊢ M ′ ]] ◦ cellhv′ }
for arbitrary values v, v′ ∈ D. In order to ensure that one kseq unit of cost occurs before and after the
delimiter action, kseq is played between two arguments of the sequential composition as was described
′
in Section 3. Given that run · w1 · done ∈ [[h ⊢ M]] ◦ cellhv and run · w2 · done ∈ [[h′ ⊢ M ′ ]] ◦ cellhv′ for any
3 The

free identifier k in (3) is used to initialize the variables h and h′ to arbitrary values from D.

A. S. Dimovski

173

v, v′ ∈ D, by Computational Adequacy we have that M, (h 7→ v) ⇓|w1 | and M ′ , (h′ 7→ v′ ) ⇓|w2 | . Since
| w1 |=| w2 |, it follows that the fact (2) holds.
Let us consider the opposite direction. Suppose that the fact (2) holds. The term in (3) is α -equivalent
to k ⊢ newD h := k in newD h′ := k in M; skip# ; M ′ . Consider [[h, h′ ⊢ M; skip# ; M ′ ]] ◦ [[(h 7→ v) ⊗ (h′ 7→ v′ )]],
where v, v′ ∈ D. By Consistency, we have that ∃ w1 ∈ [[h, h′ ⊢ M]] ◦ [[(h 7→ v) ⊗ (h′ 7→ v′ )]] such that
| w1 |= n and w1 leaves the state (h 7→ v1 ) ⊗ (h′ 7→ v′ ), and ∃ w2 ∈ [[h, h′ ⊢ M ′ ]] ◦ [[(h 7→ v1 ) ⊗ (h′ 7→ v′ )]]
such that | w2 |= n and w2 leaves the state (h 7→ v1 ) ⊗ (h′ 7→ v′1 ). Any word w ∈ R is obtained from w1
and w2 as above (| w1 |=| w2 |), and so satisfies the requirements of the theorem.
We can detect timing leaks from a semi-closed term by verifying that all words in the model in (3)
are in the required form. To do this, we restrict our attention only to the costs of words in R.
Example 1. Consider the term:
h : var int2 ⊢ if (!h > 0) then h := !h + 1; else skip : com
The slot-game semantics of this term extended as in (3) is:
run · kvar · qk · 0k · kseq · # · kseq · kvar · qk · (0k · done + 1k · kder · k+ · done)

+1k · kseq · kder · k+ · # · kseq · kvar · qk · (0k · done + 1k · kder · k+ · done)
This model includes all possible observable interactions of the term with its environment, which contains
only the identifier k, along with the costs measuring its running time. Note that the first value for k read
from the environment is used to initialize h, while the second value for k is used to initialize h′ .
By inspecting we can see that the model contains the word:
run · kvar · qk · 0k · kseq · # · kseq · kvar · qk · 1k · kder · k+ · done
which is not of the required form. This word (play) corresponds to two computations of the given term
where initial values of h are 0 and 1 respectively, such that the cost of the second computation has
additional kder + k+ units more than the first one.
We now show how to detect timing leaks of a split (open) term h : varD | ∆ ⊢ M : com, where ∆ =
x1 : T1 , . . . , xk : Tk . To do this, we need to check timing efficiency of the following model:
[[h, h′ : varD ⊢ M[N1 /x1 , . . . , Nk /xk ]; skip# ; M ′ [N1 /x1 , . . . , Nk /xk ]]]

(4)

at state (h 7→ v, h′ 7→ v′ ), for any closed terms ⊢ N1 : T1 , . . . , ⊢ Nk : Tk , and for any values v, v′ ∈ D. As
we have shown slot-game semantics respects theory of operational improvement, so we will need to
examine whether all its complete plays-with-costs s are of the form s1 · # · s2 where | s1 |=| s2 |. However,
the model in (4) can not be represented as a regular language, so it can not be used directly for detecting
timing leaks.
Let us consider more closely the slot-game model in (4). Terms M and M ′ are run in the same context
∆, which means that each occurrence of a free identifier xi from ∆ behaves uniformly in both M and M ′ .
So any complete play-with-costs of the model in (4) will be a concatenation of complete plays-with-costs
from models for M and M ′ with additional constraints that behaviours of free identifiers from ∆ are the
same in M and M ′ . If these additional constraints are removed from the above model, then we generate
a model which is an over-approximation of it and where free identifiers from ∆ can behave freely in M
and M ′ . Thus we obtain:
[[h, h′ : varD ⊢ M[N1 /x1 , . . . , Nk /xk ]; skip# ; M ′ [N1 /x1 , . . . , Nk /xk ]]] ⊆
[[h, h′ : varD ⊢ M; skip# ; M ′ [N1 /x1 , . . . , Nk /xk ]]]

174

Slot Games for Detecting Timing Leaks of Programs

If ⊢ N1 : T1 , . . . , ⊢ Nk : Tk are arbitrary closed terms, then they are interpreted by identity (copy-cat)
strategies corresponding to their types, and so we have:
[[h, h′ : varD ⊢ M; skip# ; M ′ [N1 /x1 , . . . , Nk /xk ]]] = [[h, h′ : varD, ∆ ⊢ M; skip# ; M ′ ]]
This model is a regular language and we can use it to detect timing leaks.
Theorem 5. Let h : varD | ∆ ⊢ M : com be a split (open) term, where ∆ = x1 : T1 , . . . , xk : Tk , and
S = [[k : expD, ∆ ⊢ newD h := k in M; skip# ; newD h′ := k in M ′ : com]]

(5)

If any word of S is of the form w = w1 · # · w2 such that | w1 |=| w2 |, Then h : varD | ∆ ⊢ M has no timing
leaks.
Note that the opposite direction in the above result does not hold. That is, if there exists a word from
S which is not of the required form then it does not follow that M has timing leaks, since the found word
(play) may be spurious introduced due to over-approximation in the model in (5), and so it may be not
present in the model in (4).
Example 2. Consider the term:
h : varint2 , f : expint2 f ,1 → comf ⊢ f (!h) : com
where f is a non-local call-by-name function.
The slot-game model for this term is as follows:
run · kapp · runf · (qf ,1 · kder · readh · (0h · 0f ,1 + 1h · 1f ,1 ))∗ · donef · done
Once f is called, it may evaluate its argument, zero or more times, and then it terminates successfully.
Notice that moves tagged with f represent the actions of calling and returning from the function f , while
moves tagged with f , 1 indicate actions of the first argument of f .
If we generate the slot-game model of this term extended as in (5), we obtain a word which is not in
the required form:
run · kvar · qk · 0k · kapp · runf · qf ,1 · kder · 0f ,1 · donef · kseq · # · kseq · kvar · qk · 1k · kapp · runf · donef · done
This word corresponds to two computations of the term, where the first one calls f which evaluates its
argument once, and the second calls f which does not evaluate its argument at all. The first computation
will have the cost of kder units more that the second one. However, this is a spurious counter-example,
since f does not behave uniformly in the two computations, i.e. it calls its argument in the first but not in
the second computation.
To handle this problem, we can generate an under-approximation of the model given in (4) which can
be represented as a regular language. Let h : varD | ∆ ⊢ M be a term derived without using the contraction
rule for any identifier from ∆. Consider the following model:
[[h, h′ : varD | ∆ ⊢ M; skip# ; M ′ ]]m = [[h, h′ : varD | ∆ ⊢ M; skip# ; M ′ ]] ∩
(deltaxT11 ,m ⊲⊳ . . . ⊲⊳ deltaxTkk ,m ⊲⊳ (A[[h,h′ :varD⊢com]] + $ )∗ )

(6)

where m ≥ 0 denotes the number of times that free identifiers of function types may evaluate its arguments at most. The regular expressions deltaT,m are used to repeat zero or once an arbitrary behaviour
for terms of type T, and are defined as follows.
deltaexpD,0 = q · ∑n∈D n · (ε + q · n)
deltacom,0 = run · done · (ε + run · done)
deltavarD,0 = (read · ∑n∈D n · (ε + read · n)) + (∑n∈D write(n) · ok · (ε + write(n) · ok))

A. S. Dimovski

175

If T is a first-order function type, then deltaT,m will be a regular language only when the number of times
its arguments can be evaluated is limited. For example, we have that:
m

deltacom1 →com,m = run · ∑ (run1 · done1 )r · done · (ε + run · (run1 · done1 )r · done)
r=0

If T is a function type with k arguments, then we have to remember not only how many times arguments
are evaluated in the first call, but also the exact order in which arguments are evaluated.
Notice that we allow an arbitrary behavior of type T to be repeated zero or once in deltaT,m , since it
is possible that depending on the current value of h an occurrence of a free identifier from ∆ to be run in
M but not in M ′ , or vice versa. For example, consider the term:
h : var int2 | x, y : exp int2 ⊢ newint2 z := 0 in if (!h > 0) then z := x else z := y + 1
This term has timing leaks, and the corresponding counter-example contains only one interaction with x
occurred in a computation, and one interaction with y occurred in the other computation. This counterexample will be included in the model in (6), only if deltaT,m is defined as above.
Let h : varD | ∆ ⊢ M be an arbitrary term where identifiers from ∆ may occur more than once in
M. Let h : varD | ∆1 ⊢ M1 be derived without using the contraction for ∆1 , such that h : varD | ∆ ⊢ M
is obtained from it by applying one or more times the contraction rule for identifiers from ∆. Then
[[h, h′ : varD | ∆ ⊢ M; skip# ; M ′ ]]m is obtained by first computing [[h, h′ : varD | ∆1 ⊢ M1 ; skip# ; M1′ ]]m as
defined in (6), and then by suitable tagging all moves associated with several occurrences of the same
identifier from ∆ as described in the interpretation of contraction. We have that:
[[h, h′ : varD, ∆ ⊢ M; skip# ; M ′ ]]m ⊆ [[h, h′ : varD ⊢ M[N1 /x1 , . . . , Nk /xk ]; skip# ; M ′ [N1 /x1 , . . . , Nk /xk ]]]
for any m ≥ 0 and arbitrary closed terms ⊢ N1 : T1 , . . . , ⊢ Nk : Tk .
In the case that ∆ contains only identifiers of base types B which do not occur in any while-subterm of
M, then in the above formula the subset relation becomes the equality for m = 0. If a free identifier occurs
in a while-subterm of M, then it can be called arbitrary many times in M, and so we cannot reproduce its
behaviour in M ′ .
Theorem 6. Let h : varD | ∆ ⊢ M be a split (open) term, where ∆ = x1 : T1 , . . . , xk : Tk , and
T = [[k : expD, ∆ ⊢ newD h := k in M; skip# ; newD h′ := k in M ′ : com]]m

(7)

(i) Let ∆ contains only identifiers of base types B, which do not occur in any while-subterm of M. Any
word of T (where m = 0) is of the form w1 · # · w2 such that | w1 |=| w2 | iff M has no timing leaks.
(ii) Let ∆ be an arbitrary context. If there exists a word w = w1 · # · w2 ∈ T such that | w1 |6=| w2 |, Then
M does have timing leaks.
Note that if a counter-example witnessing a timing leakage is found, then it provides a specific context
∆, i.e. a concrete definition of identifiers from ∆, for which the given open term have timing leaks.

5

Detecting Timing-Aware Non-interference

The slot-game semantics model contains enough information to check the non-interference property of
terms along with timing leaks. The method for verifying the non-interference property is analogous to

Slot Games for Detecting Timing Leaks of Programs

176

the one described in [8], where we use the standard game semantics model. As slot-game semantics
can be considered as the standard game semantics augmented with the information about quantitative
assessment of time usage, we can use it as underlying model for detection of both non-interference
property and timing leaks, which we call timing-aware non-interference.
In what follows, we show how to verify timing-aware non-interference property for closed terms. In
the case of open terms, the method can be extended straightforwardly by following the same ideas for
handling open terms described in Section 4.
Let l : varD, h : varD′ ⊢ M : com be a term where l and h represent low- and high-security global
variables respectively. We define Γ1 = l : varD, h : varD′ , Γ′1 = l′ : varD, h′ : varD′ , and M ′ is α -equivalent
to M[l′ /l, h′ /h] where all bound variables are suitable renamed. We say that Γ1 | − ⊢ M : com satisfies
timing-aware non-interference if
∀ s1 ∈ St(Γ1 ), s2 ∈ St(Γ′1 ). s1 (l) = s2 (l′ ) ∧ s1 (h) 6= s2 (h′ ) ∧
Γ1 ⊢ M; M ′ , s1 ⊗ s2 n1 skip; M ′ , s1 ′ ⊗ s2
⇒ s′1 (l) = s′2 (l′ ) ∧ n1 = n2

n2

skip; skip, s1 ′ ⊗ s2 ′

Suppose that abort is a special free identifier of type comabort in Γ. We say that a term Γ ⊢ M is safe
4
iff Γ ⊢ M[skip/abort] ⊏
∼ M[diverge/abort] ; otherwise we say that a term is unsafe. It has been shown in
abort , which we
[5] that a term Γ ⊢ M is safe iff [[Γ ⊢ M]] does not contain any play with moves from A[[com]]
call unsafe plays. For example, [[abort : comabort ⊢ skip ; abort : com]] = run · runabort · doneabort · done,
so this term is unsafe.
By using Theorem 4 from Section 4 and the corresponding result for closed terms from [8], it is easy
to show the following result.
L = [[k : expD, k′ : expD′ , abort : com ⊢ newD l := k in newD′ h := k′ in
newD l′ := !l in newD′ h′ := k′ in
skip# ; M; skip# ; M ′ ; skip# ; if (!l 6=!l′ ) then abort : com]]

(8)

The regular expression L contains no unsafe word (plays) and all its words are of the form w = w1 · # ·
w2 · # · w3 · # · w4 such that | w2 |=| w3 | iff M satisfies the timing-aware non-interference property.
Notice that the free identifier k in (8) is used to initialize the variables l and l′ to any value from D
which is the same for both l and l′ , while k′ is used to initialize h and h′ to any values from D′ . The last
if command is used to check values of l and l′ in the final state after evaluating the term in (8). If their
values are different, then abort is run.

6

Application

We can also represent slot-game semantics model of IA2 by using the CSP process algebra. This can be
done by extending the CSP representation of standard game semantics given in [6], by attaching the costs
corresponding to each translation rule. In the same way, we have adapted the verification tool in [6] to
automatically convert an IA2 term into a CSP process [17] that represents its slot-game semantics. The
CSP process outputted by our tool is defined by a script in machine readable CSP which can be analyzed
by the FDR tool. It represents a model checker for the CSP process algebra, and in this way a range of
properties of terms can be verified by calls to it.
4⊏
∼

denotes observational approximation of terms (see [1])

A. S. Dimovski

177
$
read x[0]
run

read h

0 x[0]

1h
0h

read x[0]

done

1x[0]

0 x[0]
1x[0]

$

read x[1]

x[1]
0,1
read x[1]

$
0,1x[1]

Figure 1: Slot-game semantics for the linear search with k=2
In the input syntax of terms, we use simple type annotations to indicate what finite sets of integers will
be used to model free identifiers and local variables of type integer. An operation between values of types
intn1 and intn2 produces a value of type intmax{n1 ,n2 } . The operation is performed modulo max{n1 , n2 }.
In order to use this tool to check for timing leaks in terms, we need to encode the required property
as a CSP process (i.e. regular-language). This can be done only if we know the cost of the worst plays
(paths) in the model of a given term. We can calculate the worst-case cost of a term by generating its
model, and then by counting the number of tokens in its plays. The property we want to check will be:
∑ni=0 i · # · i , where n denotes the worst-case cost of a term.
To demonstrate practicality of this approach for automated verification, we consider the following
implementation of the linear-search algorithm.
h : varint2 , x[k] : varint2 ⊢
newint2 a[k] := 0 in
newintk+1 i := 0 in
while (i < k) do {a[i] :=!x[i]; i :=!i + 1; }
newint2 y := !h in
newbool present := ff in
while (i < k && ¬present) do {
if (compare(!a[i], !y)) then present := tt;
i :=!i + 1;
} : com
The meta variable k > 0 represents the array size. The term copies the input array x into a local array a,
and the input value of h into a local variable y. The linear-search algorithm is then used to find whether
the value stored in y is in the local array. At the moment when the value is found in the array, the term
terminates successfully. Note that arrays are introduced in the model as syntactic sugar by using existing
term formers. So an array x[k] is represented as a set of k distinct variables x[0], . . . , x[k − 1] (see [6, 10]
for details).
Suppose that we are only interested in measuring the efficiency of the term relative to the number of
compare operations. It is defined as follows compare : expint2 → expint2 → expbool, and its semantics
compares for equality the values of two arguments with cost $ :
[[compare : expint12 → expint22 → expbool]] = q · $ · q1 · (∑m6=n m1 · q2 · n2 · ff ) + (∑m=n m1 · q2 · n2 · tt)
where m, n ∈ {0, 1}. We assume that the costs of all other operations are relatively negligible (e.g.
kvar = kder = . . . = 0).

Slot Games for Detecting Timing Leaks of Programs

178

We show the model for this term with k = 2 in Fig. 1. The worst-case cost of this term is equal to
the array’s size k, which occurs when the search fails or the value of h is compared with all elements of
the array. We can perform a security analysis for this term by considering the model extended as in (7),
where m = 0. We obtain that this term has timing leaks, with a counter-example corresponding to two
computations, such that initial values of h are different, and the search succeeds in the one after only one
iteration of while and fails in the other. For example, this will happen when all values in the array x are
0’s, and the value of h is 0 in the first computation and 1 in the second one.
We can also automatically analyse in an analogous way terms where the array size k is much larger.
Also the set of data that can be stored into the global variable h and array x can be larger than {0, 1}. In
these cases we will obtain models with much bigger number of states, but they still can be automatically
analysed by calls to the FDR tool.

7

Conclusion

In this paper we have described how game semantics can be used for verifying security properties of
open sequential programs, such as timing leaks and non-interference. This approach can be extended to
terms with infinite data types, such as integers, by using some of the existing methods and tools based
on game semantics for verifying such terms. Counter-example guided abstraction refinement procedure
(ARP) [5] and symbolic representation of game semantics model [7] are two methods which can be used
for this aim. The technical apparatus introduced here applies not only to time as a resource but to any
other observable resource, such as power or heating of the processor. They can all be modeled in the
framework of slot games and checked for information leaks.
We have focussed here on analysing the IA language, but we can easily extend this approach to any
other language for which game semantics exists. Since fully abstract game semantics was also defined
for probabilistic [4], concurrent [12], and programs with exceptions [1], it will be interesting to extend
this approach to such programs.

References
[1] Abramsky, S., and McCusker, G: Game Semantics. In Proceedings of the 1997 Marktoberdorf Summer
School: Computational Logic , (1998), 1–56. Springer.
[2] Agat, J: Transforming out Timing Leaks. In: Wegman, M.N., Reps, T.W. (eds.) POPL 2000. ACM, pp.
40–53. ACM, New York (2000), doi:10.1145/325694.325702.
[3] Barthe, G., D’Argenio, P.R., Rezk, T: Secure information flow by self-composition. In: IEEE CSFW
2004. pp. 100–114. IEEE Computer Society Press, (2004), doi:10.1109/CSFW.2004.17.
[4] V. Danos and R. Harmer. Probabilistic Game Semantics. In Proceedings of LICS 2000. 204–213. IEEE
Computer Society Press, Los Alamitos (2000), doi:10.1109/LICS.2000.855770.
[5] Dimovski, A., Ghica, D. R., Lazić, R. Data-Abstraction Refinement: A Game Semantic Approach. In:
Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS vol. 3672, pp. 102–117. Springer, Heidelberg (2005),
doi:10.1007/11547662 9.
[6] Dimovski, A., Lazić, R: Compositional Software Verification Based on Game Semantics and Process
Algebras. In Int. Journal on STTT 9(1), pp. 37–51, (2007), doi:10.1007/s10009-006-0005-y.
[7] Dimovski, A: Symbolic Representation of Algorithmic Game Semantics. In: Faella, M., Murano, A. (eds.) GandALF 2012. EPTCS vol. 96, pp. 99–112. Open Publishing Association, (2012),
doi:10.4204/EPTCS.96.8.

A. S. Dimovski

179

[8] Dimovski, A: Ensuring Secure Non-interference of Programs by Game Semantics. Submitted for publication.
[9] Cartwright, R., Curien, P. L., and Felleisen, M: Fully abstract semantics for observably sequential
languages. In Information and Computation 111(2), pp. 297–401, (1994), doi:10.1006/inco.1994.1047.
[10] Ghica, D. R., McCusker, G: The Regular-Language Semantics of Second-order Idealized Algol. Theoretical Computer Science 309 (1–3), pp. 469–502, (2003), doi:10.1016/S0304-3975(03)00315-3.
[11] Ghica, D. R. Slot Games: a quantitative model of computation. In Palsberg, J., Abadi, M. (eds.) POPL
2005. ACM, pp. 85–97. ACM Press, New York (1998), doi:10.1145/1040305.1040313.
[12] Ghica, D. R., Murawski, A: Compositional Model Extraction for Higher-Order Concurrent Programs.
In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS vol. 3920, pp. 303–317. Springer, Heidelberg
(2006), doi:10.1007/11691372 20.
[13] Goguen, J., Meseguer, J: Security polices and security models. In: IEEE Symp. on Security and Privacy
1982. pp. 11–20. IEEE Computer Society Press, (1982).
[14] Heintze, N., Riecke, J.G: The SLam calculus: programming with secrecy and integrity. In:
MacQueen, D.B., Cardelli, L. (eds.) POPL 1998. ACM, pp. 365–377. ACM, New York (1998),
doi:10.1145/268946.268976.
[15] Joshi, R., and Leino, K.R.M: A semantic approach to secure information flow. In Science of Computer
Programming 37, pp. 113–138, (2000), doi:10.1016/S0167-6423(99)00024-6.
[16] Reynolds, J. C: The essence of Algol. In: O’Hearn, P.W, and Tennent, R.D. (eds), Algol-like languages.
(Birkhaüser, 1997).
[17] Roscoe, W. A: Theory and Practice of Concurrency. Prentice-Hall, 1998.
[18] Sabelfeld, A., and Myers, A.C: Language-based information-flow security. In IEEE Journal on Selected
Areas in Communications 21(1), (2003), 5–19, doi:10.1109/JSAC.2002.806121.
[19] Sands, D: Improvement Theory and its Applications. Cambridge University Press, 1998.
[20] Volpano, D., Smith, G., and Irvine, C: A sound type system for secure flow analysis. In Journal of
Computer Security 4(2/3), (1996), 167–188, doi:10.3233/JCS-1996-42-304.
[21] Volpano, D., Smith, G: Eliminating covert flows with minimum typings.
In: IEEE Computer
Security Foundations Workshop (CSFW), 1997, 156–169. IEEE Computer Society Press, (1997),
doi:10.1109/CSFW.1997.596807.

