1: \documentclass{llncs}

2: \usepackage{a4wide}

3: 

4: %---------------------------------------------------------------------

5: 

6: \usepackage{latexsym,amssymb}

7: \usepackage{graphics,graphicx}

8: \usepackage{color}

9: \usepackage[all]{xy}

10: \usepackage{tikz}

11: \usepackage{algorithm}

12: \usepackage{algpseudocode}

13: 

14: %---------------------------------------------------------------------

15: 

16: \def\A{\mathbb A}

17: \def\B{\mathbb B}

18: \def\C{\mathbb C}

19: \def\Q{\mathbb Q}

20: \def\R{\mathbb R}

21: \def\Z{\mathbb Z}

22: \def\N{\mathbb N}

23: \def\M{\mathbb M}

24: \def\I{\mathbb I}

25: \def\J{\mathbb J}

26: \def\F{\mathbb F}

27: \def\E{\mathbb E}

28: \def\T{\mathbb T}

29: \def\L{\mathbb L}

30: \def\K{\mathbb K}

31: \def\H{\mathbb H}

32: \def\X{\mathbb X}

33: \def\V{\mathbb V}

34: \def\W{\mathbb W}

35: 

36: \def\al{\alpha}         \def\be{\beta}  

37: \def\ga{\gamma}         \def\de{\delta} 

38: \def\ep{\varepsilon}    \def\ze{\zeta}

39: \def\et{\eta}           \def\th{\vartheta}

40: \def\io{\iota}          \def\ka{\kappa}

41: \def\la{\lambda}        \def\rh{\varrho}

42: \def\si{\sigma}         \def\ta{\tau}

43: \def\ph{\varphi}        \def\ch{\chi}   

44: \def\ps{\psi}           \def\om{\omega}

45: 

46: \def\GA{\Gamma}         \def\DE{\Delta} 

47: \def\TH{\Theta}         \def\LA{\Lambda} 

48: \def\SI{\Sigma}         \def\PH{\Phi}

49: \def\OM{\Omega}

50: 

51: \def\cA{\mathcal A}             \def\cB{\mathcal B}

52: \def\cC{\mathcal C}             \def\cD{\mathcal D}

53: \def\cE{\mathcal E}             \def\cF{\mathcal F}

54: \def\cG{\mathcal G}             \def\cH{\mathcal H}

55: \def\cI{\mathcal I}             \def\cJ{\mathcal J}

56: \def\cK{\mathcal K}             \def\cL{\mathcal L}

57: \def\cM{\mathcal M}             \def\cN{\mathcal N}

58: \def\cO{\mathcal O}             \def\cP{\mathcal P}

59: \def\cQ{\mathcal Q}             \def\cR{\mathcal R}

60: \def\cS{\mathcal S}             \def\cT{\mathcal T}

61: \def\cU{\mathcal U}             \def\cV{\mathcal V}

62: \def\cW{\mathcal W}             \def\cX{\mathcal X}

63: \def\cY{\mathcal Y}             \def\cZ{\mathcal Z}

64: 

65: \def\bA{\mathbf A}              \def\bB{\mathbf B}

66: \def\bC{\mathbf C}              \def\bD{\mathbf D}

67: \def\bE{\mathbf E}              \def\bF{\mathbf F}

68: \def\bG{\mathbf G}              \def\bH{\mathbf H}

69: \def\bI{\mathbf I}              \def\bJ{\mathbf J}

70: \def\bK{\mathbf K}              \def\bL{\mathbf L}

71: \def\bM{\mathbf M}              \def\bN{\mathbf N}

72: \def\bO{\mathbf O}              \def\bP{\mathbf P}

73: \def\bQ{\mathbf Q}              \def\bR{\mathbf R}

74: \def\bS{\mathbf S}              \def\bT{\mathbf T}

75: \def\bU{\mathbf U}              \def\bV{\mathbf V}

76: \def\bW{\mathbf W}              \def\bX{\mathbf X}

77: \def\bY{\mathbf Y}              \def\bZ{\mathbf Z}

78: 

79: %---------------------------------------------------------------------

80: \newcommand{\SkipIf}{{\bf skipIf}}

81: \newcommand{\SkipAsn}{{\bf skipAsn}}

82: %---------------------------------------------------------------------

83: \usepackage{ifthen}

84: \newlength{\upperlabel}\setlength{\upperlabel}{0pt}

85: \newlength{\lowerlabel}\setlength{\lowerlabel}{0pt}

86: \newlength{\translabel}\setlength{\translabel}{0pt}

87: % very simple transitions

88: \newcommand{\trans}{\longrightarrow}

89: \newcommand{\ptrans}[1]{\Ltrans{#1}{~~~~~~~}}

90: \newcommand{\Trans}{\Longrightarrow}

91: \newcommand{\pTrans}[1]{\LTrans{#1}{~~~~~~~}}

92: %\newcommand{\pTrans}[1]{\Longrightarrow_{#1}}

93: % local transitions

94: \newcommand{\LTrans}[2]{%

95: \settowidth{\upperlabel}{$#1$}%

96: \settowidth{\lowerlabel}{$#2$}%

97: \ifthenelse{\lengthtest{\upperlabel>\lowerlabel}}%

98: {\setlength{\translabel}{\upperlabel}}%

99: {\setlength{\translabel}{\lowerlabel}}%

100: \xymatrix@=\translabel{\ar@{=>}[r]^{#1}_{#2}&}}

101: \newcommand{\Ltrans}[2]{%

102: \settowidth{\upperlabel}{$#1$}%

103: \settowidth{\lowerlabel}{$#2$}%

104: \ifthenelse{\lengthtest{\upperlabel>\lowerlabel}}%

105: {\setlength{\translabel}{\upperlabel}}%

106: {\setlength{\translabel}{\lowerlabel}}%

107: \xymatrix@=\translabel{\ar[r]^{#1}_{#2}&}}

108: \newcommand{\pLtrans}[3]{%

109: \settowidth{\upperlabel}{$#1:#2$}%

110: \settowidth{\lowerlabel}{$#3$}%

111: \ifthenelse{\lengthtest{\upperlabel>\lowerlabel}}%

112: {\setlength{\translabel}{\upperlabel}}%

113: {\setlength{\translabel}{\lowerlabel}}%

114: \xymatrix@=\translabel{\ar[r]^{#1:#2}_{#3}&}}

115: % network transitions

116: \newcommand{\Ntrans}{\xymatrix{\ar@2{)->}[r]&}}

117: \newcommand{\pNtrans}[1]{

118: \settowidth{\translabel}{~$#1$~}%

119: \xymatrix@=\translabel{\ar@2{)->}[r]^{#1}&}}

120: %---------------------------------------------------------------------

121: \newcommand{\Classes}[2]{{#1}/_{#2}}

122: \newcommand{\Dists}{\mbox{\bf Dist}}

123: \newcommand{\Vars}{\mbox{\bf Var}}

124: \newcommand{\Values}{\mbox{\bf Value}}

125: \newcommand{\Confs}{\mbox{\bf Conf}}

126: %---------------------------------------------------------------------

127: \newcommand{\tick}{\surd}

128: %---------------------------------------------------------------------

129: % Include/exclude comments on outline/plan

130: \newenvironment{plan}{\begin{em}}{\end{em}}

131: %\excludecomment{plan}

132: %---------------------------------------------------------------------

133: % Important for algorithms!

134: \newcommand{\Assume}{\State {\bf Assume:\ }}

135: % special label

136: \newcommand{\noop}{e}

137: \newcommand{\ins}{\vartriangleleft}

138: \newcommand{\del}{\ntriangleleft}

139: %---------------------------------------------------------------------

140: % Multiple ranges for sums, etc.

141: \newcommand{\range}[1]{\mbox{\scriptsize\(\begin{array}{c}#1\end{array}\)}}

142: %---------------------------------------------------------------------

143: % over- and under-line

144: \newcommand{\ul}{\underline}

145: \newcommand{\ol}{\overline}

146: %---------------------------------------------------------------------

147: % Identity

148: \newcommand{\Id}{{\mathbf I\mathbf d}}

149: \newcommand{\diag}{{\mathrm d\mathrm i\mathrm a\mathrm g}}

150: \newcommand{\slim}{\mbox{\rm s-}\!\lim}

151: \newcommand{\indeg}{\mbox{\rm in-}\!\deg}

152: \newcommand{\outdeg}{\mbox{\rm out-}\!\deg}

153: %---------------------------------------------------------------------

154: \newcommand{\syndef}{\mbox{\tt::=}}

155: \newcommand{\synalt}{\;\mbox{\tt\large$|$}\;}

156: \newcommand{\sem}[1]{[\![ #1 ]\!]}

157: %\newcommand{\trans}{\longrightarrow}

158: \newcommand{\ttrans}{\Longrightarrow}

159: \newcommand{\tup}[1]{\langle #1 \rangle}

160: \newcommand{\false}{\mbox{\bf false}}

161: \newcommand{\true}{\mbox{\bf true}}

162: %---------------------------------------------------------------------

163: \newcommand{\skipS}{\mbox{\bf skip}}

164: \newcommand{\stopS}{\mbox{\bf stop}}

165: \newcommand{\getsS}[2]{\varE{#1} \gets #2}

166: \newcommand{\ifS}[3]{\mbox{\bf if}~#1~\mbox{\bf then}~#2~\mbox{\bf else}~#3}

167: \newcommand{\whileS}[2]{\mbox{\bf while}~#1~\mbox{\bf do}~#2}

168: \newcommand{\waitS}{\mbox{\bf wait}}

169: \newcommand{\SkipAsnS}{\mbox{\bf SkipAsn}}

170: \newcommand{\SkipIfS}{\mbox{\bf SkipIf}}

171: \newcommand{\choice}{~\mbox{\bf or}~}

172: \newcommand{\chooseS}[2]{\mbox{\bf choose}~#1~\mbox{\bf or}~#2}

173: \newcommand{\choosel}[3]{[\mbox{\bf choose}]^{#3}~#1~\mbox{\bf or}~#2}

174: \newcommand{\chooseL}[3]{\mbox{\bf choose}^{#1}~#2~\mbox{\bf or}~#3}

175: \newcommand{\op}{\mbox{\it op}}

176: %---------------------------------------------------------------------

177: \newcommand{\high}{\mbox{\sc H}}

178: \newcommand{\low}{\mbox{\sc L}}

179: \newcommand{\Int}{\mbox{\bf Int}}

180: \newcommand{\Bool}{\mbox{\bf Bool}}

181: %---------------------------------------------------------------------

182: 

183: \begin{document}

184: 

185: \title{

186: Quantifying Timing Leaks and Cost Optimisation

187: }

188: \author{

189: Alessandra Di Pierro\inst{1} 

190: \and 

191: Chris Hankin\inst{2}

192: \and

193: Herbert Wiklicky\inst{2}

194: }

195: %

196: \institute{

197: University of Verona,

198: Ca' Vignal 2 - Strada le Grazie 15 %\\

199: I-37134 Verona, Italy %\\

200: \email{dipierro@sci.univr.it}

201: \and

202: Imperial College London,  

203: 180 Queen's Gate %\\

204: London SW7 2AZ, UK %\\

205: \email{\{clh,herbert\}@doc.ic.ac.uk }

206: }

207: 

208: %---------------------------------------------------------------------

209: 

210: \maketitle

211: 

212: %---------------------------------------------------------------------

213: 

214: \begin{abstract}

215:   We develop a new notion of security against timing attacks where the

216:   attacker is able to simultaneously observe the execution time of a program

217:   and the probability of the values of low variables.  We then show how to

218:   measure the security of a program with respect to this notion via a

219:   computable estimate of the timing leakage and use this estimate for cost

220:   optimisation.

221: \end{abstract}

222: 

223: %---------------------------------------------------------------------

224: 

225: \section{Introduction}

226: \label{Introduction}

227: 

228: Early work on language-based security, such as Volpano and Smith's type

229: systems \cite{VolpanoSmith98b}, precluded the use of high security variables

230: to affect control flow. Specifically, the conditions in if-commands and

231: while-commands were restricted to using only low security information. If this

232: restriction is weakened, it opens up the possibility that high security data

233: may be leaked through the different timing behaviour of alternative control

234: paths.  This kind of leakage of information is said to form a {\em covert

235:   timing channel} and is a serious threat to the security of programs (cf.

236: e.g. \cite{Kocher96}).

237: 

238: We develop a new notion of security against timing attacks where the attacker

239: is able to simultaneously observe the execution time of a (probabilistic)

240: program and the probability of the values of low variables.  This notion is a

241: non-trivial extension of similar ideas for deterministic programs

242: \cite{Agat00}\ which also covers attacks based on the combined observation of

243: time and low variables.  This earlier work presents an approach which, having

244: identified a covert timing channel, provides a program transformation which

245: neutralises the channel.

246: 

247: We start by introducing a semantic model of timed probabilistic transition

248: systems.  Our approach is based on modelling programs essentially as Markov

249: Chains (MC) where the stochastic behaviour is determined by a joint

250: distribution on both the values assigned to the program's variables and the

251: time it takes the program to perform a given command.  This is very different

252: from other approaches in the area of automata theory which are also dealing

253: with both time and probability. In this area the timed automata constitute a

254: well-established model \cite{alur94}.  These automata have been extended with

255: probability and used in model-checking for the verification of probabilistic

256: timed temporal logic properties of real-time systems \cite{KNSW04}. The

257: resulting model is essentially a Markov Decision Process where rewards are

258: interpreted as time durations and is therefore quite different from our MC

259: approach. In particular, the presence of non-determinism makes it not very

260: appropriate as a base of our quantitative analysis aiming at measuring timing

261: leaks.  We next present a concrete programming language with a timed

262: probabilistic transition system as its execution model. This language is based

263: on the language studied in \cite{Agat00}\ but is extended with a probabilistic

264: choice construct -- whilst this may not play a role in user programs, it has

265: an essential role in our program transformation.  In order to determine and

266: quantify the security of systems and the effectiveness of potential

267: counter-measures against timing attacks we then discuss an approximate notion

268: of timed bisimilarity and construct an algorithm for computing a quantitative

269: estimate of the vulnerability of a system against timing attacks; this is

270: given in terms of the mismatch between the actual transition probabilities and

271: those of an ideal perfectly confined program.

272: %

273: Finally, we present a probabilistic variation of Agat's padding algorithm

274: which we use to illustrate -- via an example -- a technique for formally

275: analysing the trade-off between security costs and protection.

276: 

277: %---------------------------------------------------------------------

278: 

279: \section{The Model}

280: \label{Model}

281: 

282: We introduce a general model for the semantics of programs where time and

283: probability are explicitly introduced in order to keep track of both the

284: probabilistic evolution of the program/system state and its running time.

285:  

286: The scenario we have in mind is that of a multilevel security system and an

287: attacker who can observe the system looking at the values of its public

288: variables and the time it takes to perform a given operation or before

289: terminating, or other similar properties related to its timing behaviour.

290: 

291: In order to keep the model simple, we assume that the time to execute a

292: statement is constant and that there is no distinction between any `local' and

293: `global' clocks. In a more realistic model, one has -- of course -- to take

294: into account also that the execution speed might differ depending on which

295: other process is running on the same system and/or delays due to

296: uncontrollable events in the communication infrastructure, i.e. network.

297: 

298: Our reference model is the timed probabilistic transition system we define

299: below.  The intuitive idea is that of a probabilistic transition system

300: (similar to those defined in all generality in \cite{JonssonEtAl01}) where

301: transition probabilities are defined by a joint distribution of two random

302: variables representing the variable updates and time, respectively.

303: 

304: %---------------------------------------

305: 

306: Let us consider a finite set $X$, and let $\Dists(X)$ denote the set of all

307: {\em probability distributions} on $X$, that is the set of all functions $\pi:

308: X \rightarrow [0,1]$, such that $\sum_{x\in X} \pi(x) = 1$. We often represent

309: these functions as sets of tuples $\{\tup{x,\pi(x)}\}_{x\in X}$.

310: %

311: If the set $X$ is presented as a Cartesian product, i.e.  $X = X_1 \times

312: X_2$, then we refer to a distribution on $X$ also as a {\em joint

313:   distribution} on $X_1$ and $X_2$.  A joint distribution associates to each

314: pair $(x_1,x_2)$, with $x_1\in X_1, x_2\in X_2$ the probability

315: $\pi(x_1,x_2)$.

316: %

317: It is important to point out that, in general, it is not possible to define

318: any joint distribution on $X_1 \times X_2$ as a `product' of distributions on

319: $X_1$ and $X_2$, i.e. for a given joint distribution $\pi$ on $X = X_1 \times

320: X_2$ it is, in general, not possible to find distributions $\pi_1$ and $\pi_2$

321: on $X_1$ and $X_2$ such that for all $(x_1,x_2) \in X_1 \times X_2$ we have

322: $\pi(x_1,x_2) = \pi_1(x_1)\pi_2(x_2)$. In the special cases where a joint

323: distribution $\pi$ can be expressed in this way, as a `product', we say that

324: the distributions $\pi_1$ and $\pi_2$ are {\em independent}

325: (cf. e.g. \cite{Stirzaker99}).

326: 

327: %---------------------------------------

328: 

329: \subsection{Timed Probabilistic Transition Systems}

330: 

331: The execution model of programs which we will use in the following is that of

332: a labelled transition system; more precisely, we will consider probabilistic

333: transition systems (PTS). We will put labels on transitions as well as states;

334: the former will have ``times'' associated with them while the latter will be

335: labelled by uninterpreted entities which are intended to represent the values

336: of (low security) variables, i.e. the computational state during the execution

337: of a program. We will not specify what kind of ``time labels'' we use -- e.g.

338: whether we have a discrete or continuous time model -- we just assume that

339: time labels are taken from a finite set $\T\subseteq\R^+$ of positive real

340: numbers. The ``state labels'' will be taken from an abstract set which we

341: denote by $\L$.

342:  

343: \begin{definition}\label{tPTS}

344:   We define a {\em timed Probabilistic Transition System with labelled

345:     states}, or tPTS, as a triple $(S,\trans,\la)$, with $S$ a finite set of

346:   {\em states}, $\trans \;\subseteq S \times \T \times [0,1] \times S$ a

347:   probabilistic transition relation, and $\la: S \rightarrow \L$ a state

348:   labelling function.

349: \end{definition}

350: 

351: We denote by $s_1 \ptrans{p:t} s_2$ the fact that $(s_1,p,t,s_2) \in \trans$

352: with $s_1,s_2\in S$, $p\in[0,1]$ and $t\in\T$. In a general tPTS we can have

353: {\em non-determinism} in the sense that for two states $s_1$ $s_2$ we may have

354: $s_1 \ptrans{1:t_1} s_2$ and $s_1 \ptrans{1:t_2} s_2$, which would suggest

355: that it is possible to make a transition from $s_1$ to $s_2$ in different

356: times ($t_1$ and $t_2$) and probability $1$, i.e. certainly.

357: %

358: In order to eliminate non-determinism we will consider in this paper only

359: tPTS's which are subject to the following conditions:

360: \begin{enumerate}

361: \item for all $s \in S$ we have $\sum_{(s,p_i,t_j,s_k) \in \trans} p_i = 1$, and

362: \item for all $t \in T$ there is {\em at most one} tuple $(s_1,t,p,s_2) \in

363:   \trans$.

364: \end{enumerate}

365: 

366: The first condition means that we consider here a {\em purely probabilistic}

367: or {\em generative} execution model. The second condition allows us to

368: associate a unique probability to every transition time between two states,

369: i.e. triple $(s_1,t,s_2)$; this means that we can define a function $\pi: S

370: \times \T \times S \rightarrow [0,1]$ such that $s_1 \ptrans{p:t} s_2$ iff

371: $\pi(s_1,t,p_2) = p$. Note however, that it is still possible to have

372: differently timed transitions between states, i.e. it is possible to have

373: $(s_1,t_1,p_2,s_2) \in \trans$ and $(s_1,t_2,p_2,s_2) \in \trans$ with $t_1

374: \neq t_2$.

375: 

376: If for all $s_1,s_2 \in S$ there exists at most one $(s_1,t,p,s_2)\in \trans$,

377: we can also represent a timed Probabilistic Transition System with labelled

378: states as a quadruple $(S,\trans,\tau,\la)$ with $\tau: S \times S \rightarrow

379: [0,1] \times \T$, a timing function. Thus, to any two states $s_1$ and $s_2$

380: we associate a unique transition time $t_{s_1,s_2}$ and probability

381: $p_{s_1,s_2}$.

382: 

383: \begin{definition}

384:   Consider a tPTS $(S,\trans,\la)$ and an {\em initial

385:     state} $s_0 \in S$. An {\em execution sequence} or {\em trace} starting in

386:   $s_0$ is a sequence $(s_0,s_1,\ldots)$ such that

387:   $s_i\ptrans{p_i:t_i}s_{i+1}$, for all $i=0,1,2,\dots$.

388: \end{definition}

389: 

390: We associate, in the obvious way, to an execution sequence $\si =

391: (s_0,s_1,\ldots)$ three more sequences: (i) the transition probability

392: sequence: $(p_1,p_2,\ldots)$, (ii) a time stamp sequence: $(t_1,t_2,\ldots)$,

393: and (iii) a state label sequence: $(\la(s_o),\la(s_1),\ldots)$.

394: 

395: Even for a tPTS with a finite number of states it is possible to have infinite

396: execution sequences. It is thus, in general, necessary to consider measure

397: theoretic notions in order to define a mathematically sound model for the

398: possible behaviours of a tPTS.  However, as long as we consider only

399: terminating systems, i.e. finite traces, things are somewhat simpler. In

400: particular, in this case, probability distributions can replace measures as

401: they are equivalent.  In this paper we restrict our attention to terminating

402: traces and probability distributions. This allows us to define for every

403: finite execution sequence $\si = (s_0,s_1,\ldots)$ its {\em running time} as

404: $\tau(\si) = \sum t_i$, and its {\em execution probability} as $\pi(\si) =

405: \prod t_i$. We will also associate to every state $s_0$ its {\em execution

406:   tree}, i.e. the collection of all execution sequences starting in $s_0$.

407: 

408: %---------------------------------------

409: 

410: \subsection{Observing tPTS's}

411: 

412: In Section~\ref{pWhile}\ we will present an operational semantics of a simple

413: imperative programming language, pWhile, via a tPTS. Based on this model we

414: will then investigate the vulnerability against attackers who are able to

415: observe (i) the time, and (ii) the state labels, i.e. the low variables. In

416: this setting we will argue that the combined observation of time and low

417: variables is more powerful than the observation of time and low variables

418: separately. The following example aims to illustrate this aspect which comes

419: from the properties of joint probability distributions.

420: 

421: \begin{example}

422:   In order to illustrate the role of joint distributions in the observation of

423:   timed PTS's let us consider the following simple systems.

424:   \[

425:   \xymatrix{

426:     &&

427:     \bullet^{s_1}

428:     \ar[dll]_{\frac{1}{4}:1}

429:     \ar[dl]^{\frac{1}{4}:2}

430:     \ar[d]^{\frac{1}{4}:1}

431:     \ar[dr]^{\frac{1}{4}:2}

432:     &

433:     \\

434:     \circ_{s^1_1}

435:     &

436:     \circ_{s^1_2} 

437:     &

438:     \bullet_{s^1_3} 

439:     &

440:     \bullet_{s^1_4} 

441:     \\

442:   }

443:   \hspace{1cm}

444:   \xymatrix{

445:     &

446:     \bullet^{s_2} 

447:     \ar[dl]_{\frac{1}{4}:2}

448:     \ar[d]_{\frac{1}{4}:2}

449:     \ar[dr]_{\frac{1}{4}:1}

450:     \ar[drr]^{\frac{1}{4}:1}

451:     &&

452:     \\

453:     \bullet_{s^2_1} 

454:     &

455:     \bullet_{s^2_2} 

456:     &

457:     \circ_{s^2_3} 

458:     &

459:     \circ_{s^2_4} 

460:     \\

461:   }

462:   \]

463:   We assume that the attacker can observe the execution times and that he/she

464:   is also able to (partially) distinguish (the final) states. In our example

465:   we assume that the states depicted as $\bullet$ and $\circ$ form two classes

466:   which the attacker can identify (e.g. because $\bullet$ and $\circ$ states

467:   have the same values for low, variables). The question now is whether this

468:   information allows the attacker to distinguish the two tPTS's.

469: 

470:   If we consider the information obtained by observing the running time, we

471:   see that both systems exhibit the same time behaviour corresponding to the

472:   distribution $\{ \tup{1,\frac{1}{2}}, \{\tup{2,\frac{1}{2}} \}$ over $\T =

473:   \{1,2\}$. The same is true in the case where the information is obtained by

474:   inspecting the final states: we have the distributions $\{

475:   \tup{\bullet,\frac{1}{2}}, \{\tup{\circ,\frac{1}{2}} \}$ over

476:   $\L=\{\bullet,\circ\}$ for both systems.

477: 

478:   However, considering that the attacker can observe running time and labels

479:   simultaneously, we see that the system on the right hand side always runs

480:   for $2$ time steps iff it ends up in a $\bullet$ state and $1$ time step iff

481:   it ends up in a $\circ$ state. In the system on the left hand side there is

482:   no such {\em correlation} between running time and final state. The

483:   difference between the two systems, which allows an attacker to distinguish

484:   them, is reflected in the joint distributions over $\T \times \L$. These can

485:   be expressed in matrix form for the two systems above as:

486:   \[

487:   \begin{array}{c|cc}

488:     \chi_1(t,l) & ~~~1~~~ & ~~~2~~~    \\ \hline

489:     \bullet& \frac{1}{4} & \frac{1}{4} \\

490:     \circ  & \frac{1}{4} & \frac{1}{4} \\ 

491:   \end{array}

492:   \hspace{2cm}

493:   \begin{array}{c|cc}

494:     \chi_2(t,l) & ~~~1~~~ & ~~~2~~~ \\ \hline

495:     \bullet& 0           & \frac{1}{2} \\

496:     \circ  & \frac{1}{2} & 0           \\ 

497:   \end{array}

498:   \]

499:   Note that while $\chi_1$ is the product of two {\em independent} probability

500:   distributions on $\T$ and $\L$ it is not possible to represent $\chi_2$ in

501:   the same way.

502: \end{example}

503: 

504: %---------------------------------------------------------------------

505: 

506: \section{An Imperative Language}

507: \label{pWhile}

508: 

509: We consider a language similar to that used in \cite{Agat00}\ with the

510: addition of a probabilistic choice construct. The syntax of the language is as

511: follows:

512: \[

513: \begin{array}{lrcl}

514: \mbox{Operators:}   & \op & \syndef & 

515: + \synalt * \synalt - \synalt = \synalt != \synalt < \synalt <= \\

516: \mbox{Expressions:} & e & \syndef & 

517: v \synalt x \synalt e~\op~e \\

518: \mbox{Commands:}    & C, D & \syndef & 

519: x := e \synalt \SkipAsn ~x~e \synalt \ifS{(e)}{C}{D} \synalt \SkipIf ~e~C \\ 

520: & & & \synalt \whileS{(e)}{C} \synalt C;D \synalt \chooseL{p}{C}{D} \\

521: \mbox{Basic Values:}& v & \syndef & 

522: n \synalt \true \synalt \false

523: \end{array}

524: \]

525: The probabilistic choice is used in an essential way in the program

526: transformation presented later.

527: %

528: We also keep the language of types in \cite{Agat00}, although in a 

529: simplified form:

530: \[

531: \begin{array}{lll}

532: \mbox{Security levels} ~~~ & 

533: s ~\syndef~ \low \synalt \high & (\mbox{with } \low \leq \high 

534:                                  ~\mbox{and}~ s \leq s) \\

535: \mbox{Base types} & 

536: \overline{\tau} ~\syndef~ \Int \synalt \Bool \\

537: \mbox{Security types} & 

538: \tau~\syndef~\overline{\tau}_s

539: \end{array}

540: \]

541: and sub-typing relation:

542: \[

543: \frac{\displaystyle

544: s_1 \leq s_2}

545: {\displaystyle

546: \overline{\tau}_{s_1} \leq \overline{\tau}_{s_2}}.

547: \]

548: 

549: We will indicate by $E$ the state of a computation and denote by $E_L$ its

550: restriction to low variables, i.e. a state which is defined as $E$ for all the

551: low variables for which $E$ is defined, and is undefined otherwise.  We say

552: that two configurations $ \tup{E~|~C}$ and $\tup{E'~|~C'}$ are {\em low

553:   equivalent} if and only if $E_L=E'_L$ and we indicate this by $\tup{E~|~C}

554: =_L \tup{E'~|~C'}$.  In the following we will sometimes use for configurations

555: the shorthand notation $c, c_1, c_2, \dots, c', c'_1, \ldots$. We will also

556: denote by ${\Confs}$ the set of all configurations.

557: 

558: %---------------------------------------

559: 

560: \subsection{SOS Semantics}

561: 

562: The operational semantics of pWhile -- except for the probabilistic choice

563: construct -- follows essentially the one presented in \cite{Agat00}. 

564: For the convenience of the reader we present here  all the

565: rules which are based on the big step semantics for expressions (where

566: $\sem{op}$ represents the usual semantics of operators):

567: 

568: \[

569: \begin{array}{l@{~~~~~~~~}c@{~~~~~~~~}r}

570: E \vdash v \Downarrow v 

571: &

572: \frac{\displaystyle E(x) = v}{\displaystyle E \vdash x \Downarrow v} 

573: &

574: \frac{

575: \displaystyle E \vdash e_1 \Downarrow v_1 \hspace{0.5cm} 

576:               E \vdash e_2 \Downarrow v_2}{

577: \displaystyle E \vdash e_1 ~\op~ e_2 \Downarrow v_1 \sem{op} v_2}

578: \end{array}

579: \]

580: 

581: The small step semantics is then define as a timed PTS via the %following

582: SOS rules in Table~\ref{OpSem}.

583: 

584: %---------------------------------------------------------------------

585: \begin{table}[t]

586: \hrule

587: \[

588: \begin{array}{ll}

589: \mbox{(Assign)} & 

590: \frac{

591: \displaystyle 

592: E \vdash e \Downarrow v

593: }{

594: \displaystyle 

595: \tup{E ~|~ x:=e} \ptrans{1:t_e \cdot t_x \cdot t_{asn} \cdot \surd} E[x=v]

596: }

597: \\[5ex]

598: \mbox{(Seq)} &

599: \frac{

600: \displaystyle

601: \tup{E~|~C} \ptrans{p:ts \cdot \surd)} E'

602: }{

603: \displaystyle

604: \tup{E~|~C ; D} \ptrans{p:ts} \tup{E'~|~D}

605: }

606: \\[3ex] &

607: \frac{

608: \displaystyle

609: \tup{E~|~C} \ptrans{p:ts} \tup{E'~|~C'}

610: }{

611: \displaystyle

612: \tup{ E~|~C ; D} \ptrans{p:ts} \tup{E'~|~C' ; D}

613: }

614: \\[5ex]

615: \mbox{(If)} &

616: \frac{

617: \displaystyle

618: E \vdash e \Downarrow \true

619: }{

620: \displaystyle

621: \tup{E~|~\ifS{(e)}{C}{D}} \ptrans{1:t_e \cdot t_{br}}\tup{E~|~C}

622: }

623: \\[3ex] &

624: \frac{

625: \displaystyle

626: E \vdash e \Downarrow \false

627: }{

628: \displaystyle

629: \tup{E~|~\ifS{(e)}{C}{D}} \ptrans{1:t_e \cdot t_{br}} \tup{E~|~D}

630: }

631: \\[5ex]

632: \mbox{(SkipAsn)} &

633: \frac{

634: \displaystyle

635: E \vdash e \Downarrow v

636: }{

637: \displaystyle

638: \tup{E~|~\SkipAsn~ x~ e} \ptrans{1:t_e \cdot t_{asn} \cdot \surd} E

639: }

640: \\[5ex]

641: \mbox{(SkipIf)} &

642: \frac{

643: \displaystyle

644: E \vdash e \Downarrow v

645: }{

646: \displaystyle

647: \tup{E~|~\SkipIf~ e~ C} \ptrans{1:t_e \cdot t_{br}} \tup{E~|~C}

648: }~~~~~v \in \{\true,\false\}

649: \\[5ex]

650: \mbox{(While)} &

651: \frac{

652: \displaystyle

653: E \vdash e \Downarrow \false

654: }{

655: \displaystyle

656: \tup{E~|~\whileS{(e)}{C}} \ptrans{1:t_e \cdot t_{br} \cdot \surd} E

657: }

658: \\[3ex] &

659: \frac{

660: \displaystyle

661: E \vdash e \Downarrow \true

662: }{

663: \displaystyle

664: \tup{E~|~\whileS{(e)}{C}} \ptrans{1:t_e \cdot t_{br}} 

665:                            \tup{E~|~C ; \whileS{(e)}{C}} 

666: }

667: \\[5ex]

668: \mbox{(Choose)} &

669: \frac{

670: \displaystyle 

671: ~

672: }{

673: \displaystyle

674: \tup{E~|~\chooseL{p}{C}{D}} \ptrans{p:t_{ch}} \tup{E~|~C}

675: }

676: \\[3ex] &

677: \frac{

678: \displaystyle 

679: ~

680: }{

681: \displaystyle

682: \tup{E~|~\chooseL{p}{C}{D}} \ptrans{(1-p):t_{ch}} \tup{ E~|~D}

683: }

684: \end{array}

685: \]

686: \hrule\vspace{1em}

687: \caption{Operational Semantics}

688: \label{OpSem}

689: \end{table}

690: %---------------------------------------------------------------------

691: 

692: The time labels $t_.$ represent the time it takes to perform certain

693: operations: $t_x$ is the time to store a variable, $t_e$ is the time it takes

694: to evaluate an expression, $t_{asn}$ represents the time to perform an

695: assignment, $t_{br}$ is the time required for a branching step, and $t_{ch}$

696: is the time to perform a probabilistic choice. By $ts$ we denote any sequence

697: of time labels and with $\surd$ we indicate termination.

698: 

699: The rule (Choose) is the only new rule with respect to the original semantics

700: in \cite{Agat00}.  It states that the execution of a probabilistic choice

701: construct leads, after a time $t_{ch}$, to a state where either the command

702: $C$ or the command $D$ is executed with probability $p$ or $1-p$,

703: respectively.  This rule together with the standard transition rules for the

704: other constructs of the language define a tPTS for our pWhile language

705: according to Definition~\ref{tPTS}. In this tPTS, the state labels are given

706: by the environment, i.e. $\la(\tup{E~|~C}) = E$.

707: 

708: %---------------------------------------

709: 

710: \subsection{Abstract Semantics}

711: 

712: According to the notion of security we consider in this paper, an observer or

713: attacker can only observe the changes in low variables. Therefore, we can

714: simplify the semantics by `collapsing' the execution tree in such a way that

715: execution steps during which the value of all low variables is unchanged are

716: combined into one single step.

717: %

718: We call an execution sequence $\si$ {\em deterministic} if $\pi(\si) = 1$, and

719: we call it {\em low stable} if $\la(s_i)|_L = l$ for all $s_i\in\si$. The empty

720: path (of length zero) is by definition deterministic and low stable.

721: %

722: An execution sequence is {\em maximal deterministic/low stable} if it is not a

723: proper sub-sequence of another deterministic/low stable path.

724: 

725: \begin{definition}

726:   We define the collapsed transition relation by: 

727:   $\tup{E_1~|~C_1} \pTrans{p:T} \tup{E_2~|~C_2}$ iff

728: \begin{description}

729: %

730: \item[(i)] there exists a configuration $\tup{E_1'~|~C_1'}$ such that

731:   $\tup{E_1~|~C_1} \ptrans{p:t} \tup{E_1'~|~C_1'}$,

732: %

733: \item[(ii)] the path $\tup{E_1'~|~C_1'} \ptrans{1:t_1} \ldots \ptrans{1:t_{n-1}}

734:   \tup{E_2'~|~C_2'} \ptrans{1:t_n} \tup{E_2~|~C_2}$ is deterministic,

735: %

736: \item[(iii)] the path $\tup{E_1~|~C_1} \ptrans{p:t} \tup{E_1'~|~C_1'}

737:   \ptrans{1:t_1} \ldots \ptrans{1:t_{n-1}} \tup{E_2'~|~C_2'}$ is maximal low

738:   stable,

739: %

740: \item[(iv)] and $T = t + {\displaystyle\sum_{i=1}^n t_i}$.

741: \end{description}

742: \end{definition}

743: 

744: This is illustrated in the following example. In the depicted execution trees

745: we indicate in the nodes only the state and omit the program parts of the

746: corresponding configurations. Moreover, we use the notation $[n,m]$ for the

747: state $E$ where $h$ has value $n$ and $l$ has value $m$. 

748: \[

749:   \xymatrix@R=3mm@C=5mm{

750:   &

751:   & 

752:   [0,0] 

753:   \ar[d]^{1:t_e + t_{br}}

754:   &

755:   \\

756:   &

757:   & 

758:   [0,0] 

759:   \ar[dll]_{\frac{1}{4}:t_{ch}}

760:   \ar[dl]^{\frac{1}{4}:t_{ch}}

761:   \ar[dr]^{\frac{1}{2}:t_{ch}}

762:   &

763:   \\

764:   [0,0] \ar[d]_{1:t_{asn}}

765:   &

766:   [0,0] \ar[d]^{1:t_{asn}}

767:   & 

768:   &

769:   [0,0] \ar[d]_{1:t_{asn}}

770:   \\

771:   [0,1] \ar[d]_{1:t_{asn}}

772:   &

773:   [0,1] \ar[d]^{1:t_{asn}}

774:   & 

775:   &

776:   [0,0] 

777:   \\

778:   [0,1]

779:   &

780:   [0,1]

781:   & 

782:   &

783:   }

784: ~~~~~~~~

785:   \xymatrix@R=3mm@C=10mm{

786:   &

787:   & 

788:   [0,0] 

789:   \ar@{=>}[d]^{1:t_e + t_{br}}

790:   &

791:   \\

792:   &

793:   & 

794:   [0,0] 

795:   \ar@{=>}[dll]_{\frac{1}{4}:t_{ch} + t_{asn}}

796:   \ar@{=>}[dl]^{\frac{1}{4}:t_{ch} + t_{asn}}

797:   \ar@{=>}[dr]^{\frac{1}{2}:t_{ch} + t_{asn}}

798:   &

799:   \\

800:   [0,1] \ar@{=>}[d]_{1:t_{asn}}

801:   &

802:   [0,1] \ar@{=>}[d]^{1:t_{asn}}

803:   & 

804:   &

805:   [0,0] 

806:   \\

807:   [0,1] 

808:   &

809:   [0,1] 

810:   & 

811:   &

812:   }

813: \]

814: The collapsed execution tree on the right hand side represents in effect what

815: an attacker can actually observe during the program execution (for our

816: analysis of the situation we still record the value of $h$ although it is

817: invisible to the attacker).

818:  

819: %---------------------------------------------------------------------

820: 

821: \section{Bisimulation and Timing Leaks}

822: 

823: Observing the low variables and the running time separately is not the same as

824: observing them together; a correlation between the two random variables

825: (probability and time) has to be taken into account (cf.

826: Section~\ref{Model}).  A naive probabilistic extension of the

827: $\Gamma$-bisimulation notion introduced in \cite{Agat00} might not take this

828: into account. More precisely, this may happen if time and probability are

829: treated as two independent aspects which are observed separately in a mutual

830: exclusive way.  According to such a notion an attacker must set up two

831: different covert channels if she wants to exploit possible interference

832: through both the probabilistic and the timing behaviour of the system.

833: 

834: The notion of bisimulation we introduce here allows us to define a stronger

835: security condition: an attacker must be able to distinguish the probabilities

836: that two programs compute a given result in a given execution time. This is

837: obviously different from being able to distinguish the probability

838: distributions of the results {\em and} the running time.

839: 

840: 

841: %---------------------------------------

842: 

843: \subsection{Probabilistic Time Bisimulation}

844: \label{PTBisim}

845: 

846: Probabilistic bisimulation was first introduced in \cite{LarsenSkou91}\ and

847: refers to an equivalence on probability distributions over the states of the

848: processes. This latter equivalence is defined as a lifting of the bisimulation

849: relation on the support sets of the distributions, namely the states

850: themselves.

851: 

852: An equivalence relation $\sim\;\subseteq S \times S$ on $S$ can be lifted to a

853: relation $\sim^* \;\subseteq \Dists(S) \times \Dists(S)$ between probability

854: distributions on $S$ via (cf \cite[Thm~1]{JonssonEtAl01}):

855: \[

856: \mu \sim^* \nu ~\mbox{iff}~ \forall [s] \in \Classes{S}{\sim}: \mu([s]) =

857: \nu([s]).

858: \]

859: It follows that $\sim^*$ is also an equivalence relation

860: (\cite[Thm~3]{JonssonEtAl01}).

861: 

862: For any equivalence relation $\sim$ on the set ${\Confs}$ of configurations,

863: we define the associated {\em low equivalence} relation $\sim_L$ by $c_1

864: \sim_L c_2$ if $c_1 \sim c_2$ and $c_1 =_L c_2$.  Obviously $\sim_L$ is again

865: an equivalence relation.  We can lift a low equivalence $\sim_L$ to

866: $(\sim_L)^*$ which we simply denote by $\sim_L^*$.

867: 

868: %--------------------------------

869:  

870: \begin{definition}

871:   Given a security typing $\GA$, a probabilistic time bisimilarity $\sim$ is

872:   the largest symmetric relation on configurations such that whenever

873: %\[

874:   $c_1 \sim c_2$,

875: %\]

876:   then

877:   \[

878:   c_1 \ttrans \chi_1

879:   ~\mbox{implies that there exists }~ 

880:   \chi_2 ~\mbox{ such that }~

881:   c_2 \ttrans \chi_2

882:   ~\mbox{and}~

883:   \chi_1 \sim_L^* \chi_2.

884:   \]

885: 

886:   We say that two configurations are probabilistic time bisimilar or

887:   PT-bisimilar, $c_1 \sim c_2$, if there exists a probabilistic time

888:   bisimilarity relation in which they are related.

889: \end{definition}

890: 

891: This definition generalises the one in \cite{Agat00}\ which only applies to

892: deterministic transition systems. Note that there is a difference between

893: $\sim_L^* = (\sim_L)^*$ and $(\sim^*)_L$; in fact, only the former is able to

894: take into account the correlation between time and low variables, while the

895: latter would be a straightforward generalisation of the time bisimulation in

896: \cite{Agat00} which is unable to model such a correlation.

897: 

898: %--------------------------------

899: 

900: We now exploit the notion of bisimilarity introduced above in order to

901: introduce a security property ensuring that a system is confined against any

902: combined attacks based on both timing and probabilistic covert channels.

903: 

904: \begin{definition}

905:   A pWhile program $P$ is {\em probabilistic time secure} or PT-secure if for

906:   any set of initial states $E$ and $E'$ such that $E_L = E'_L$, we have

907:   $\tup{E,P} \sim \tup{E',P}$.

908: \end{definition}

909: 

910: %---------------------------------------------------------------------

911: 

912: \section{Computing Approximate Bisimulation}

913: 

914: The papers \cite{TCS05,CONCUR03}\ introduce an approximate version of

915: bisimulation and confinement where the approximation can be used as a measure

916: $\varepsilon$ for the information leakage of the system under analysis. The

917: quantity $\varepsilon$ is formally defined in terms of the norm of a linear

918: operator representing the partition induced by the `minimal' bisimulation on

919: the set of the states of a given system, i.e. the one minimising the

920: observational difference between the system's components. We show here how to

921: compute a non-trivial upper bound $\delta$ to $\varepsilon$ by essentially

922: exploiting the algorithmic solution proposed by Paige and Tarjan

923: \cite{PaigeTarjan87}\ for computing bisimulation equivalence. This was already

924: adapted to PTS's in \cite{JLAP06}, where it was used for constructing a

925: padding algorithm as part of a transformational approach to the timing leaks

926: problem. In this approach the computational paths of a program are transformed

927: so as to make it perfectly secure by eliminating any possible timing covert

928: channel while preserving its I/O behaviour.

929: 

930: The algorithm we present here is an instantiation of that algorithm where the

931: abstract labels are replaced by the statements in a concrete language (pWhile)

932: and their execution times. Moreover, instead of transforming the execution

933: trees, our algorithm accumulates the information about the difference between

934: their transition probabilities and uses this information to compute an upper

935: bound $\delta$ to the maximal information leakage of the given program.

936: 

937: %---------------------------------------

938: 

939: \subsection{Computing $\delta$ for PT-Bisimulation}

940: 

941: %---------------------------------------------------------------------

942: 

943: \begin{algorithm}%[b]

944: \begin{algorithmic}[1]

945:   \Procedure{QLumping}{$T_1,T_2$}

946:   \Assume $T_1$ execution tree with states $S_1$, and

947:           $T_2$ execution tree with states $S_2$

948: %

949:   \State $\delta \gets 0$

950:   \State $n \gets 0$

951:   \State $P \gets \{ S_1 \cup S_2 \}$    

952:     \Comment{(Initial) Partition}

953: %

954:   \While{$n \leq \Call{Height}{T_1 \oplus T_2}$}

955:      \State $S \gets \{ B \cap \Call{CutOff}{T_1 \oplus T_2,n}) ~|~ B \in P \}$

956:        \Comment{Splitters (below)}

957: %

958:      \While{$S \neq \emptyset$}

959:        \State choose $B\in S$, $S \gets S \setminus B$

960:          \Comment{Choose a splitter}

961:        \State $P \gets \Call{Splitting}{B,P}$

962:          \Comment{Split partition}

963:      \EndWhile

964:      \State $L_1 \gets \Call{Layer}{T1,n}$, 

965:             $L_2 \gets \Call{Layer}{T2,n}$

966:      \State $\Call{CompDelta}{L_1,L_2}$

967:      \State $n \gets n+1$

968:        \Comment{Go to next level}

969:   \EndWhile

970: %       \State \Return C

971:          \State \Return $\delta$

972:   \EndProcedure

973: \end{algorithmic}

974: \caption{Algorithm for detecting critical blocks}

975: \label{QLumping}

976: \end{algorithm}

977: 

978: %--------------------------------------------------------------------

979: 

980: \begin{algorithm}[t]

981: \begin{algorithmic}[1]

982:   \Procedure{CompDelta}{$L_1,L_2$}

983: 	\While{$L_1 \neq \emptyset$}

984: 	  \State choose $s_1 \in L_1$, $L_1 \gets L_1 \setminus s_1$

985: 	    \Comment For all $s_1\in L_1$

986: 	  \State $\beta \gets \infty$

987: 	  \State $L \gets L_2$	

988: 	  \While{$L_2 \neq \emptyset$}

989: 	    \State choose $s_2 \in L$, $L \gets L \setminus s_2$	 

990: 	      \Comment For all $s_2\in L_2$

991: 	    \State $\beta \gets \min(\beta,\|\chi(s_1)-\chi(s_2)\|_\infty)$

992: 	      \Comment Find best match

993: 	  \EndWhile

994:       \State $\delta \gets \max(\delta,\beta)$

995:     \EndWhile

996:   \EndProcedure

997: \end{algorithmic}

998: \caption{Algorithm for computing $\delta$}

999: \label{CompDelta}

1000: \end{algorithm}

1001: 

1002: %--------------------------------------------------------------------

1003: 

1004: Algorithm~\ref{CompDelta}\ describes a procedure that can be used inside an

1005: algorithm for constructing a lumping (i.e.\ a PT-bisimulation equivalence) of

1006: two tPTS's $T_1$ and $T_2$. In particular, Algorithm~\ref{QLumping}\ refers to

1007: a such a procedure which follows the algorithmic paradigm for partition

1008: refinement introduced by Paige and Tarjan in \cite{PaigeTarjan87} (see also

1009: \cite{DerisaviEtAl03,DovierEtAl04}). The Paige-Tarjan algorithm constructs a

1010: partition of a state space $\Sigma$ which is {\em stable} for a given

1011: transition relation $\rightarrow$. It is a well-known result that this

1012: partition corresponds to a bisimulation equivalence on the transition system

1013: $(\Sigma,\rightarrow)$. The refinement procedure used in the algorithm

1014: consists in {\em splitting} the blocks in a given partition $P$ by replacing

1015: each block $B\in P$ with $B\cap pre{S}$ and $B\setminus pre{S}$, where

1016: $S\subseteq \Sigma$ and $pre(X)=\{s\in \Sigma\mid s\rightarrow x\mbox{ for

1017:   some }x\in X\}$.

1018: 

1019: In order to check whether two execution trees $T_1$ and $T_2$ in our tPTS

1020: model are PT-bisimilar, in Algorithm~\ref{QLumping} we apply this refinement

1021: technique to the set of states formed by the disjoint union of the states in

1022: $T_1$ and $T_2$.  The strategy of our lumping procedure $\Call{QLumping}{T_1,

1023:   T_2}$ \ is as follows: it proceeds iteratively layer by layer starting from

1024: the leaves layer, and splits the blocks in the current partition restricted to

1025: the current layer.  The procedure $\Call{CompDelta}{L_1,L_2}$ computes for

1026: each two layers $L_1$ and $L_2$, the maximal difference

1027: $\|\chi(s_1)-\chi(s_2)\|_\infty$ between the probabilities to get from states

1028: in $T_1\cap L_1$ and $T_2\cap L_1$, respectively, into states of layer $L_2$.

1029: In the original lumping procedure this would determine a splitting of the

1030: states in layer $L_1$. This value is stored in a variable $\beta$ and compared

1031: with the current value of a variable $\delta$ which contains the maximal

1032: difference up to that iteration. When the lumping algorithm terminates (that

1033: is when we have reached the root of the union tree), one of the following

1034: situations will occur: either the roots of $T_1$ and $T_2$ belong to the same

1035: class in the constructed partition (i.e. $T_1$ and $T_2$ are PT-bisimilar) or

1036: not. In the latter case $\delta$ will contain a maximal difference in the

1037: transition probabilities of the two processes which makes them non-bisimilar.

1038: This is therefore an estimate of the information leakage of the system. Note

1039: that, by construction, $\delta$ will be zero in the first case.

1040: 

1041: The strategy for constructing the lumping described above determines the {\em

1042:   coarsest partition} of a set which is stable wrt a given relation

1043: \cite{DerisaviEtAl03,DovierEtAl04}, that is in our case the coarsest

1044: PT-bisimulation equivalence. Obviously, this does not necessarily coincide

1045: with the `minimal' one corresponding to the quantity $\varepsilon$ defined in

1046: \cite{TCS05}. Thus, $\delta$ will be in general only a safe approximation,

1047: namely an upper bound to the capacity of probabilistic timing covert channel

1048: defined by $\varepsilon$.

1049: %

1050: The following proposition is therefore a corollary of Proposition~45 in

1051: \cite{TCS05}\ stating a similar assertion for $\varepsilon$-bisimulation.

1052: 

1053: \begin{proposition}

1054:   $P$ is PT-secure iff for any pair of initial configurations $c_1,c_2$ the

1055:   corresponding execution trees $T_1$ and $T_2$ are such that

1056:   $\Call{QLumping}{T_1, T_2}$ returns $\delta =0$.

1057: \end{proposition}

1058: 

1059: %---------------------------------------

1060: 

1061: \subsection{A Weighted Version:  $\delta'$}

1062: 

1063: The actual value of $\de$ is determined by the way we compute the best match

1064: between the joint probability distributions $\chi(s_1)$ and $\chi(s_2)$ in

1065: line~8 of $\Call{CompDelta}{L_1,L_2}$. In order to compute $\de$ we use the

1066: {\em supremum norm}, $\|\cdot\|_\infty$, between two distributions, i.e. the

1067: largest absolute difference between corresponding entries in $\chi(s_1)$ and

1068: $\chi(s_2)$, respectively. In other words, we try to identify a class of

1069: states $C$ (in the layer below) and a time interval $t$ such that the

1070: probability of reaching this class in that time from $s_1$ differs maximally

1071: from the one for $s_2$.

1072: 

1073: One can argue that this is a fair approach as we treat all classes and time

1074: labels the same way. However, it might be useful to develop a measure which

1075: reflects the fact that certain times and classes are more similar than others.

1076: 

1077:  From the point of view of the attacker, such a measure would encode her/his

1078: ability in detecting similarity as given by the nature and the precision of

1079: the instruments he is actually using.  For example, suppose it is possible to

1080: reach the same class $C$ from $s_1$ and $s_2$ with different times $t_1$ and

1081: $t_2$, such that the corresponding probabilities determine $\de$ (i.e. we have

1082: the maximal difference in this case). However, we might in certain

1083: circumstances also want to express the fact that $t_1$ and $t_2$ are more or

1084: less similar, e.g. for $t_1=10$ and $t_2=10.5$ we might want a smaller $\de'$

1085: than for $t_1=1$ and $t_2=100$.  In terms of the attacker, this means that we

1086: make our estimate dependent on the actual power of the time detection

1087: instrument that he/she possesses.

1088: 

1089: In order to incorporate similarity of times and/or classes we need to modify

1090: the way we determine the best match in line~8 of $\Call{CompDelta}{L_1,L_2}$.

1091: Instead of determining the norm between $\chi(s_1)$ and $\chi(s_2)$ we can

1092: compute a weighted version as:

1093: \[

1094: \beta \gets 

1095: \min(\beta,\|\omega\cdot\chi(s_1)-\omega\cdot\chi(s_2)\|_\infty) =

1096: \min(\beta,\|\omega\cdot(\chi(s_1)-\chi\cdot(s_2))\|_\infty),

1097: \]

1098: where $\omega$ re-scales the entries in $\chi(s_1)$ and $\chi(s_2)$ so as to

1099: reflect the relative importance of certain times and/or classes. Note that

1100: ``$\cdot$'' denotes here the component-wise and not the matrix multiplication:

1101: $(\omega\cdot\chi)_{tC} = \omega_{tC}\chi_{tC}$. If, for example, an attacker

1102: is not able to detect the absolute difference between times but can only

1103: measure multiplicities expressing approximative proportions, we could re-scale

1104: the $\chi$'s via $\omega_{tC} = \log(t)$.

1105: 

1106: In the following we will use a weighted version $\de'$ which reflects the

1107: similarity of classes. The idea is to weight according to the

1108: ``replaceability'' of a class. To this purpose we associate to every class (in

1109: the layers below) a matching measure $\mu(C) = \min_{C \neq C'}\de'(C,C')$,

1110: i.e. we determine the $\de'$ between a (sub)tree with a root in the class $C$

1111: in question and all (sub)trees with roots in any of the other classes $C'$.

1112: We can take any representative of the classes $C$ and $C'$ as these are by

1113: definition bisimilar. The measure $\mu$ indicates how easy it is to replace

1114: class $C$ by another one, or how good/precise is the attacker in

1115: distinguishing successor states.  Then $\de'$ is simply the weighted version

1116: of $\de$ as described above with $\omega_{tC} = \mu(C)$. Note that there is no

1117: problem with the fact that $\de'$ is defined recursively as we always know the

1118: $\de'$ in the layers below before we compute $\de'$ in the current layer.

1119: 

1120: %---------------------------------------

1121: 

1122: \begin{example}

1123:   In order to illustrate how $\delta$ and $\delta'$ quantify the difference

1124:   between various execution trees, let us consider the following four trees.

1125:   \[

1126:   \xymatrix@R=4mm{

1127:   \bullet_1 \ar[d]_1 \\

1128:   \bullet_2 \ar[d]_1 \\

1129:   \bullet_3 \ar[d]_1 \\

1130:   \bullet_3 \\

1131:   }

1132:   ~~~~~

1133:   \xymatrix@C=5mm@R=4mm{

1134:   & 

1135:   \bullet_1 \ar[dl]_{\frac{1}{2}} \ar[dr]^{\frac{1}{2}}

1136:   & \\

1137:   \bullet_2 \ar[d]_1 

1138:   &&

1139:   \bullet_3 \ar[d]_1   

1140:   \\

1141:   \bullet_4 

1142:   &&

1143:   \bullet_5 \ar[d]_1   

1144:   \\

1145:   &&

1146:   \bullet_6  

1147:   \\

1148:   }

1149:   ~~~  

1150:   \xymatrix@C=5mm@R=4mm{

1151:   & 

1152:   \bullet_1 \ar[d]_1

1153:   & \\

1154:   & 

1155:   \bullet_2 \ar[dl]_{\frac{1}{2}} \ar[dr]^{\frac{1}{2}}

1156:   & \\

1157:   \bullet_3 

1158:   &&

1159:   \bullet_4 \ar[d]_1   

1160:   \\

1161:   &&

1162:   \bullet_5

1163:   \\

1164:   }

1165:   ~~~  

1166:   \xymatrix@C=5mm@R=4mm{

1167:   & 

1168:   \bullet_1 \ar[d]_1

1169:   & \\

1170:   & 

1171:   \bullet_2 \ar[d]_1

1172:   & \\

1173:   & 

1174:   \bullet_3 \ar[dl]_{\frac{1}{2}} \ar[dr]^{\frac{1}{2}}

1175:   & \\

1176:   \bullet_4 

1177:   &&

1178:   \bullet_5 

1179:   \\

1180:   }

1181:   \]

1182:   We abstract from the influence of different transition times and individual

1183:   state labels, i.e. we assume that $t=1$ for all transitions and that all

1184:   states are labelled with the same label.

1185:   

1186:   If we compute the $\de$ and $\de'$ values between all the pairs of systems

1187:   we get the following results:

1188:   \[

1189:   \begin{array}{c|rrrr}

1190:     \de   & \bT_1 & \bT_2 & \bT_3 & \bT_4 \\ \hline

1191:     \bT_1 & 0.000 & 0.500 & 1.000 & 0.000 \\

1192:     \bT_2 & 0.500 & 0.000 & 1.000 & 0.500 \\

1193:     \bT_3 & 1.000 & 1.000 & 0.000 & 1.000 \\

1194:     \bT_4 & 0.000 & 0.500 & 1.000 & 0.000 \\

1195:   \end{array}

1196:   ~~~~~~~

1197:   \begin{array}{c|rrrr}

1198:     \de'  & \bT_1 & \bT_2 & \bT_3 & \bT_4 \\ \hline

1199:     \bT_1 & 0.000 & 0.250 & 0.125 & 0.000 \\

1200:     \bT_2 & 0.250 & 0.000 & 0.125 & 0.250 \\

1201:     \bT_3 & 0.125 & 0.125 & 0.000 & 0.125 \\

1202:     \bT_4 & 0.000 & 0.250 & 0.125 & 0.000 \\

1203:   \end{array}

1204:   \]

1205:   From this we see that $\de$ and $\de'$ are symmetric, i.e. the difference

1206:   between two systems is symmetric; that every system is bisimilar with

1207:   itself, i.e.  $\de=0=\de'$ (as we have an empty diagonal); and that the

1208:   difference between two systems is between zero and one with values in

1209:   between very well possible.

1210: \end{example}

1211: 

1212: %---------------------------------------------------------------------

1213: 

1214: \section{Cost Analysis}

1215: 

1216: In a recent article on ``Software Bugtraps'' in {\em The Economist} the

1217: authors report on some ongoing research at NIST on ``Software Assurance

1218: Metrics and Tool Evaluation'' \cite{TheEconomist08}. They claim that ``{\em

1219:   The purpose of the research is to get away from the feeling that `all

1220:   software has bugs' and say `it will cost this much money to make software of

1221:   this kind of quality'}''.  They then conclude: ``{\em Rather than trying to

1222:   stamp out bugs altogether, in short, the future of "software that makes

1223:   software better" may lie in working out where the pesticide can be most

1224:   cost-effectively applied}''.

1225: 

1226: Our aim is to introduce ``cost factors'' in a similar way into computer

1227: security. Instead of trying to achieve perfect security we will look at the

1228: trade-off between costs of security counter measures -- such as increased

1229: average running time -- and the improvement in terms of security, which we can

1230: measure via the $\delta$ introduced above. Even in simple examples we are able

1231: to exhibit interesting effects.

1232: 

1233: %---------------------------------------

1234: 

1235: \subsection{Security Typing}

1236: 

1237: In \cite{Agat00}\ Agat introduces a program transformation to remove covert

1238: timing channels ({\em timing leaks}) from programs written in a sequential

1239: imperative programming language.  The language used is a language of security

1240: types with two security levels that is based on earlier work by Volpano and

1241: Smith \cite{VolpanoSmith98a,VolpanoSmith98b}.  Whilst Volpano and Smith

1242: restrict the condition in both while-loops and if-commands to being of the

1243: lowest security level, Agat allows the condition in an if-command to be high

1244: security providing that an external observer cannot detect which branch was

1245: taken. He shows that if a program is typeable in his system, then it is secure

1246: against timing attacks.  This result depends critically on a notion of

1247: bisimulation; an if-command with a high security condition is only typeable if

1248: the two branches are bisimilar.  Agat's notion of bisimilarity is timing aware

1249: and based on a notion of low-equivalence which ensures stepwise

1250: non-interference.  He does not give an algorithm for bisimulation checking.

1251: 

1252: If a program fails to type, Agat presents a transformation system to remove

1253: the timing leak.  The transformation pads the branches of if-commands with

1254: high security conditions with dummy commands.  The objective of the padding is

1255: that both branches end up with the same timing and thus become

1256: indistinguishable by an external observer.  The transformation utilises the

1257: concept of a {\em low-slice}: for a given command $C$, its low-slice $C_L$ has

1258: the same syntactic structure as $C$ but only has assignments to low security

1259: variables; all assignments to high security variables and branching on high

1260: security conditions are replaced by skip commands of appropriate duration.

1261: The transformation involves extending the branches in a high security

1262: if-command by adding the low-slice from the other branch.  The effect of this

1263: transformation is that the timing of the execution of both branches are the

1264: same and equal to the sum of timing of the two branches in the untransformed

1265: program.  Agat demonstrates that the transformation is semantically sound and

1266: that transformed programs are secure (correctness).

1267: 

1268: In order to extend this system to our language, we only have to add a rule for

1269: the {\bf choose} statement (essentially a straight forward extension of the

1270: rule for {\bf if}). In detail, we present the typing rules in

1271: Table~\ref{SecTypes}. Note that the rule (If$_{H}$) refers to the {\em

1272:   semantic} notion of timed bisimilarity (as introduced in

1273: Section~\ref{PTBisim}).

1274: 

1275: %---------------------------------------------------------------------

1276: \begin{table}[t]

1277: \hrule

1278: \[

1279: \begin{array}{ll}

1280: \mbox{(Assign$_{H}$)} &

1281: \frac{

1282: \displaystyle

1283: \Gamma \vdash_\leq e : \overline{\tau}_s ~~~~

1284: \Gamma \vdash_= x : \overline{\tau}_{H} ~~~~ s \leq H

1285: }{

1286: \displaystyle

1287: \Gamma \vdash x := e : \SkipAsn~x~e

1288: }

1289: \\[5ex]

1290: \mbox{(Assign$_{L}$)} &

1291: \frac{

1292: \displaystyle

1293: \Gamma \vdash_\leq e : \overline{\tau}_{L} ~~~

1294: \Gamma \vdash_= x : \overline{\tau}_{L}

1295: }{

1296: \displaystyle

1297: \Gamma \vdash x := e : x := e

1298: }

1299: \\[5ex]

1300: \mbox{(Seq)} &

1301: \frac{

1302: \displaystyle

1303: \Gamma \vdash C : C_{L} ~~~~ \Gamma \vdash D : D_{L}

1304: }{

1305: \displaystyle

1306: \Gamma C ; D : C_{L} ; D_{L}

1307: }

1308: \\[5ex]

1309: \mbox{(If$_{H}$)} &

1310: \frac{

1311: \displaystyle

1312: \Gamma \vdash_\leq e : \Bool_{H} ~~~~

1313: \Gamma \vdash C : C_{L} ~~~~ \Gamma \vdash D : D_{L}

1314: }{

1315: \displaystyle

1316: \Gamma \vdash \ifS{(e)}{C}{D} : \SkipIf~e~C_{L}

1317: } ~~~~ C_{L} \sim D_{L} 

1318: \\[5ex]

1319: \mbox{(If$_{L}$)} &

1320: \frac{

1321: \displaystyle

1322: \Gamma \vdash_\leq e : \Bool_{L} ~~~~

1323: \Gamma \vdash C : C_{L} ~~~~ \Gamma \vdash D : D_{L}

1324: }{

1325: \displaystyle

1326: \Gamma \vdash \ifS{(e)}{C}{D} : \ifS{(e)}{C_{L}}{D_{L}}

1327: }

1328: \\[5ex]

1329: \mbox{(While)} &

1330: \frac{

1331: \displaystyle

1332: \Gamma \vdash_\leq e : \Bool_{L} ~~~~ \Gamma \vdash C : C_{L}

1333: }{

1334: \displaystyle

1335: \Gamma \vdash \whileS{(e)}{C} : \whileS{(e)}{C_{L}}

1336: }

1337: \\[5ex]

1338: \mbox{(Choose)} &

1339: \frac{

1340: \displaystyle

1341: \Gamma \vdash C : C_{L} ~~~~ \Gamma \vdash D : D_{L}

1342: }{

1343: \displaystyle

1344: \Gamma \vdash \chooseL{p}{C}{D} : \chooseL{p}{C_{L}}{D_{L}}

1345: }

1346: \\[5ex]

1347: \mbox{(SkipAsn)} &

1348: \frac{

1349: \displaystyle 

1350: ~

1351: }{

1352: \displaystyle

1353: \Gamma \vdash \SkipAsn~x~e : \SkipAsn~x~e

1354: }

1355: \\[5ex]

1356: \mbox{(SkipIf)} &

1357: \frac{

1358: \displaystyle 

1359: \Gamma \vdash C : C_{L}

1360: }{

1361: \displaystyle

1362: \Gamma \vdash \SkipIf~e~C : \SkipIf~e~C_{L}

1363: }

1364: \end{array}

1365: \]

1366: \hrule\vspace{1em}

1367: \caption{Security Typing Rules}

1368: \label{SecTypes}

1369: \end{table}

1370: %---------------------------------------------------------------------

1371: 

1372: %---------------------------------------

1373: 

1374: \subsection{Probabilistic Transformation}

1375: 

1376: We consider a probabilistic variant of Agat's language.  Probabilities

1377: play an important role in the transformation.  Rather than just adding the

1378: low slice from the other branch to each branch of a high security conditional,

1379: we transform each branch to make a probabilistic choice between its

1380: padded and untransformed variant.  This allows us to trade-off the

1381: increased run-time of the padded program versus the vulnerability to attack

1382: of the untransformed program.  The transformation described is just one

1383: on a whole spectrum of probabilistic transformations -- at the other extreme

1384: we could probabilistically decide whether or not to execute each 

1385: command in the low slice.

1386: %

1387: All the formal transformation rules for probabilistic padding are the same as

1388: in \cite{Agat00}. The only exception is the rule (If$_{H}$): Here we replace

1389: -- provided certain typing conditions are fulfilled -- the branches of an {\bf

1390:   if} statement not just by the correctly ``padded'' version as in

1391: \cite{Agat00}; instead we introduce in every branch a choice such that the

1392: secure replacement will be executed only with probability $p$ while with

1393: probability $1-p$ the original code fragment will be executed.

1394: 

1395: In order to transform programs into secure versions we need to introduce an

1396: auxiliary notion, namely the notion of global effect $ge(C)$ of commands. This

1397: is used to identify (global) variables which might be changed when a command

1398: $C$ is executed. Here is its formal definition:

1399: \[

1400: \begin{array}{rcl}

1401: ge(x := e)                & = & \{x\}\\

1402: ge(C_1;C_2)               & = & ge(C_1) ~\cup~ ge(C_2)\\

1403: ge(\ifS{(e)}{C_1}{C_2})   & = & ge(C_1) ~\cup~ ge(C_2)\\

1404: ge(\whileS{(e)}{C})       & = & ge(C)\\

1405: ge(\chooseL{p}{C_1}{C_2}) & = & ge(C_1) ~\cup~ ge(C_2)\\

1406: ge(\SkipAsn~x~e)          & = & \emptyset\\

1407: ge(\SkipIf~e~C)           & = & ge(C).

1408: \end{array}

1409: \]

1410: 

1411: The judgments or transformation rules in Table~\ref{ProgTrans}\ are of the

1412: general form:

1413: \[

1414: \Gamma \vdash C \hookrightarrow D ~|~ D_{L}

1415: \]

1416: which represents the fact that with a certain (security) typing $\Gamma$ we

1417: can transform the statement $C$ into $D$ -- we also recorder as a side-product

1418: the so-called {\em low slice} $D_{L}$ of $D$. 

1419: 

1420: %---------------------------------------------------------------------

1421: \begin{table}[t]

1422: \hrule

1423: \[

1424: \begin{array}{ll}

1425: \mbox{(Assign$_{H}$)} &

1426: \frac{

1427: \displaystyle

1428: \Gamma \vdash_\leq e : \overline{\tau}_s ~~~~

1429: \Gamma \vdash_= x : \overline{\tau}_{H} ~~~~ s \leq H

1430: }{

1431: \displaystyle 

1432: \Gamma \vdash x := e \hookrightarrow x := e ~|~ \SkipAsn~x~e

1433: }

1434: \\[5ex]

1435: \mbox{(Assign$_{L}$)} &

1436: \frac{

1437: \displaystyle

1438: \Gamma \vdash_\leq e : \overline{\tau}_{L} ~~~~

1439: \Gamma \vdash_= x : \overline{\tau}_{L}

1440: }{

1441: \displaystyle 

1442: \Gamma \vdash x := e \hookrightarrow x := e ~|~ x := e

1443: }

1444: \\[5ex]

1445: \mbox{(Seq)} &

1446: \frac{\displaystyle

1447: \Gamma \vdash C_1 \hookrightarrow D_1 ~|~ D_{1L} ~~~~

1448: \Gamma \vdash C_2 \hookrightarrow D_2 ~|~ D_{2L}

1449: }{

1450: \displaystyle

1451: \Gamma \vdash C_1 ; C_2 \hookrightarrow D_1 ; D_2 ~|~ D_{1L} ; D_{2L}

1452: }

1453: \\[5ex]

1454: \mbox{(If$_{H}$)} &

1455: \frac{

1456: \displaystyle

1457: \Gamma \vdash_\leq e: \Bool_{H} ~~

1458: \Gamma \vdash C_1 \hookrightarrow D_1 ~|~ D_{1L} ~~

1459: \Gamma \vdash C_2 \hookrightarrow D_2 ~|~ D_{2L} ~~

1460: ge(D_{1L}) = \emptyset ~~ ge(D_{2L}) = \emptyset

1461: }{

1462: \displaystyle

1463: \Gamma \vdash \ifS{(e)}{C_1}{C_2} \hookrightarrow

1464: \begin{array}{l}

1465: {

1466: \displaystyle 

1467: {\bf if}~(e)~{\bf then}~(\chooseL{p}{D_1}{D_1 ; D_{2L}})~{\bf else}

1468: } 

1469: \\

1470: {

1471: \displaystyle 

1472: (\chooseL{p}{D_2}{D_{1L} ; D_2}) ~|~ \SkipIf~e~(D_{1L} ; D_{2L})

1473: }

1474: \end{array}

1475: }

1476: \\[7ex]

1477: \mbox{(If$_{L}$)} &

1478: \frac{

1479: \displaystyle

1480: \Gamma \vdash_\leq e : \Bool_{L} ~~

1481: \Gamma \vdash C_1 \hookrightarrow D_1 ~|~ D_{1L} ~~

1482: \Gamma \vdash C_2 \hookrightarrow D_2 ~|~ D_{2L}

1483: }{

1484: \displaystyle

1485: \Gamma \vdash \ifS{(e)}{C_1}{C_2} \hookrightarrow

1486: \ifS{(e)}{D_1}{D_2} ~|~

1487: \ifS{(e)}{D_{1L}}{D_{2L}}

1488: }

1489: \\[5ex]

1490: \mbox{(While)} &

1491: \frac{

1492: \displaystyle

1493: \Gamma \vdash_\leq e : \Bool_{L} ~~~~

1494: \Gamma \vdash C \hookrightarrow D ~|~ D_{L}

1495: }{

1496: \displaystyle

1497: \Gamma \vdash \whileS{(e)}{C} \hookrightarrow 

1498: \whileS{(e)}{D} ~|~ \whileS{(e)}{D_{L}}

1499: }

1500: \\[5ex]

1501: \mbox{(Choose)} &

1502: \frac{

1503: \displaystyle

1504: \Gamma \vdash C_1 \hookrightarrow D_1 ~|~ D_{1L} ~~~~

1505: \Gamma \vdash C_2 \hookrightarrow D_2 ~|~ D_{2L}

1506: }{

1507: \displaystyle

1508: \Gamma \vdash \chooseL{p}{C_1}{C_2} \hookrightarrow

1509: \chooseL{p}{D_1}{D_2} ~|~ \chooseL{p}{D_{1L}}{D_{2L}}

1510: }

1511: \\[5ex]

1512: \mbox{(SkipAsn)} &

1513: \frac{

1514: \displaystyle 

1515: ~

1516: }{

1517: \displaystyle

1518: \Gamma \vdash \SkipAsn~x~e \hookrightarrow 

1519: \SkipAsn~x~e ~|~ \SkipAsn~x~e

1520: }

1521: \\[5ex]

1522: \mbox{(SkipIf)} &

1523: \frac{

1524: \displaystyle

1525: \Gamma \vdash C \hookrightarrow D ~|~ D_{L}

1526: }{

1527: \displaystyle

1528: \Gamma \vdash \SkipIf~e~C \hookrightarrow

1529: \SkipIf~e~D ~|~ \SkipIf~e~D_{L}}

1530: \end{array}

1531: \]

1532: \hrule\vspace{1em}

1533: \caption{Probabilistic Program Transformation}

1534: \label{ProgTrans}

1535: \end{table}

1536: %---------------------------------------------------------------------

1537: 

1538: %------------------------------------------

1539: 

1540: \subsection{An Example}

1541: 

1542: Our probabilistic version of Agat's padding algorithm allows us to obtain {\em

1543:   partially} fixed programs. Depending on the parameter $p$ with which we

1544: introduce empty low slices to obfuscate the timing leaks we can determine the

1545: (average) execution time of the fixed program in comparison with the

1546: improvement in security.

1547: 

1548: Agat presents in his paper \cite{Agat00}\ an example which itself is based on

1549: Kocher's study \cite{Kocher96}\ of timing attacks against the RSA algorithm.

1550: In order to illustrate our approach we simplify the example slightly: The

1551: insecure program {\tt agat} we start with is depicted on the left side in

1552: Table~\ref{AgatProgs}. The fully padded version Agat's algorithm produces,

1553: {\tt fagat}, is on the right hand side of Table~\ref{AgatProgs}\ (to keep

1554: things simple we omit Agat's empty statements like {\tt skipAsn s s}; as {\tt

1555:   skip} as well as {\tt s:=s} can be used just to `spend time' without having

1556: any real effect on the store we can use e.g. {\tt s:=s} in place of Agat's

1557: {\tt skipAsn s s}). The program, {\tt pagat}, presented in the middle of

1558: Table~\ref{AgatProgs}\ is the result of {\em probabilistic padding}: The

1559: original program {\tt agat} is transformed in such a way that the compensating

1560: statements, i.e. low slices, are executed only with probability $p$ while with

1561: probability $q=1-p$ the original code is executed.  For $p=0$ we have the same

1562: behaviour as the original program {\tt agat} while for $p=1$ this program

1563: behaves in the same way as Agat's fully padded version {\tt fagat}.

1564: 

1565: %---------------------------------------------------------------------

1566: \begin{table}[t]

1567: \hrule\vspace{1em}

1568: \begin{center}

1569: \begin{minipage}[t]{3.8cm}

1570: \begin{verbatim}

1571: i := 1;

1572: while i<=3 do

1573:  if k[i]==1 then

1574:    s := s;  

1575:  else 

1576:    skip;

1577:  fi;

1578:  i := i+1;

1579: od;

1580: \end{verbatim}

1581: \end{minipage}

1582: ~

1583: \begin{minipage}[t]{5cm}

1584: \begin{verbatim}

1585: i := 1;

1586: while i<=3 do

1587:  if k[i]==1 then

1588:    choose p: s := s; skip 

1589:    or     q: s := s 

1590:    ro 

1591:  else 

1592:    choose p: skip

1593:    or     q: s := s; skip

1594:    ro

1595:  fi;

1596:  i := i+1;

1597: od;

1598: \end{verbatim}

1599: \end{minipage}

1600: ~

1601: \begin{minipage}[t]{3cm}

1602: \begin{verbatim}

1603: i := 1;

1604: while i<=3 do

1605:  if k[i]==1 then

1606:    s := s; skip 

1607:  else 

1608:    s := s; skip

1609:  fi; 

1610:  i := i+1;

1611: od;

1612: \end{verbatim}

1613: \end{minipage}

1614: \end{center}

1615: \hrule\vspace{1em}

1616: \caption{Versions of Agat's Program: {\tt agat},{\tt pagat}, and {\tt fagat}}

1617: \label{AgatProgs}

1618: \end{table}

1619: %---------------------------------------------------------------------

1620: 

1621: In our concrete experiments we used the following assumptions. The variable

1622: ${\tt i}$ can take values in $\{1,..,4\}$ while ${\tt k}$ is a three

1623: dimensional array with values in $\{0,1\}$ -- nothing is concretely assumed

1624: about ${\tt s}$. The variables ${\tt k}$, representing a {\em secret key}, and

1625: ${\tt s}$ have security typing $H$, while ${\tt i}$ is the only low variable

1626: which can be observed by an attacker. We implemented this example using

1627: (arbitrary) execution times: $t_{asn}= 3$ (assign time), $t_{br} = 2$

1628: (test/branch time), and $t_{skip} = 1$ (skip time), and $t_{ch} = 0$ (choice

1629: time).

1630: 

1631: The abstract semantics for the {\tt pagat} program -- which only records

1632: choice points and the moments in time when the low variable changes its value

1633: -- produces the following execution trees if we start with keys {\tt k=011}

1634: and {\tt k=010}:

1635: \[

1636:   \xymatrix@C=13mm{

1637:     \bullet \ar@2[r]_{1:5} &

1638:     \bullet \ar@/^/@2[r]^{q:4} 

1639:             \ar@/_/@2[r]_{p:7} &

1640:     \bullet \ar@2[r]_{1:2} &

1641:     \bullet \ar@/^/@2[r]^{q:6} 

1642:             \ar@/_/@2[r]_{p:7} &

1643:     \bullet \ar@2[r]_{1:2} &

1644:     \bullet \ar@/^/@2[r]^{q:6} 

1645:             \ar@/_/@2[r]_{p:7} &

1646:     \bullet \ar@2[r]_{1:1} &

1647:     \bullet

1648:   }

1649: \]

1650: \[

1651:   \xymatrix@C=13mm{

1652:     \bullet \ar@2[r]_{1:5} &

1653:     \bullet \ar@/^/@2[r]^{q:4} 

1654:             \ar@/_/@2[r]_{p:7} &

1655:     \bullet \ar@2[r]_{1:2} &

1656:     \bullet \ar@/^/@2[r]^{q:6} 

1657:             \ar@/_/@2[r]_{p:7} &

1658:     \bullet \ar@2[r]_{1:2} &

1659:     \bullet \ar@/^/@2[r]^{q:4} 

1660:             \ar@/_/@2[r]_{p:7} &

1661:     \bullet \ar@2[r]_{1:1} &

1662:     \bullet

1663:   }

1664: \]

1665: One can easily see from this how probabilistic padding influences the

1666: behaviour of a program: For every bit in the key ${\tt k}$ -- i.e. every

1667: iteration -- we have a choice between executing the original code with

1668: probability $q=1-p$ or the `safe' code with probability $p$. The new code

1669: always takes the same time (in our case $7$ ticks) while the original code's

1670: execution time depends on whether ${\tt k[i]}$ is set or not (either $4$ or

1671: $6$ time steps in our case). Clearly, for $p=0$ we get in every iteration a

1672: different execution time, depending on the bit ${\tt k[i]}$, and thus can

1673: deduce the secrete value ${\tt k}$ by just observing the execution times.

1674: However, as the execution time is always the same for the replacement code, it

1675: is impossible to do the same for $p=1$. For values of $p$ between $0$ and $1$,

1676: the (average) execution times for ${\tt k[i]}=0$ and ${\tt k[i]}=1$ become

1677: more and more similar. This means in practical terms that the attacker has to

1678: spend more and more time (i.e. repeated observations of the program) in order

1679: to determine with high confidence the exact execution time and thus deduce the

1680: value of ${\tt k[i]}$ (cf. e.g. \cite{TCS05}).

1681: 

1682: %---------------------------------------------------------------------

1683: \begin{figure}[t]

1684: \begin{tikzpicture}[y=5mm,x=6.66mm]

1685: \draw[style=help lines] (0,28) grid[ystep=5mm,xstep=6.66mm] (10,38);

1686: \draw (0,27.33) node{$0$};

1687: \foreach \x in {1,...,9} {\draw (\x,27.33) node{$\frac{\x}{10}$};}

1688: \draw (10,27.33) node{$1$};

1689: %

1690: \foreach \y in {28,...,38} {\draw (-0.5,\y) node{\y}; }

1691: %

1692: \draw (0.00,29.00) -- (1.00,29.90) -- (2.00,30.80) -- (3.00,31.70) --

1693: (4.00,32.60) -- (5.00,33.50) -- (6.00,34.40) -- (7.00,35.30) -- (8.00,36.20)

1694: -- (9.00,37.10) -- (10.00,38.00); \draw (0.00,31.00) -- (1.00,31.70) --

1695: (2.00,32.40) -- (3.00,33.10) -- (4.00,33.80) -- (5.00,34.50) -- (6.00,35.20)

1696: -- (7.00,35.90) -- (8.00,36.60) -- (9.00,37.30) -- (10.00,38.00); \draw

1697: (0.00,31.00) -- (1.00,31.70) -- (2.00,32.40) -- (3.00,33.10) -- (4.00,33.80)

1698: -- (5.00,34.50) -- (6.00,35.20) -- (7.00,35.90) -- (8.00,36.60) --

1699: (9.00,37.30) -- (10.00,38.00); \draw (0.00,33.00) -- (1.00,33.50) --

1700: (2.00,34.00) -- (3.00,34.50) -- (4.00,35.00) -- (5.00,35.50) -- (6.00,36.00)

1701: -- (7.00,36.50) -- (8.00,37.00) -- (9.00,37.50) -- (10.00,38.00); \draw

1702: (0.00,31.00) -- (1.00,31.70) -- (2.00,32.40) -- (3.00,33.10) -- (4.00,33.80)

1703: -- (5.00,34.50) -- (6.00,35.20) -- (7.00,35.90) -- (8.00,36.60) --

1704: (9.00,37.30) -- (10.00,38.00); \draw (0.00,33.00) -- (1.00,33.50) --

1705: (2.00,34.00) -- (3.00,34.50) -- (4.00,35.00) -- (5.00,35.50) -- (6.00,36.00)

1706: -- (7.00,36.50) -- (8.00,37.00) -- (9.00,37.50) -- (10.00,38.00); \draw

1707: (0.00,33.00) -- (1.00,33.50) -- (2.00,34.00) -- (3.00,34.50) -- (4.00,35.00)

1708: -- (5.00,35.50) -- (6.00,36.00) -- (7.00,36.50) -- (8.00,37.00) --

1709: (9.00,37.50) -- (10.00,38.00); \draw (0.00,35.00) -- (1.00,35.30) --

1710: (2.00,35.60) -- (3.00,35.90) -- (4.00,36.20) -- (5.00,36.50) -- (6.00,36.80)

1711: -- (7.00,37.10) -- (8.00,37.40) -- (9.00,37.70) -- (10.00,38.00);

1712: \end{tikzpicture}

1713: \begin{tikzpicture}[y=5mm,x=6.66mm]

1714: \draw[style=help lines] (0,0) grid[ystep=5mm,xstep=6.66mm] (10,10);

1715: %  \draw[style=help lines] (0,0) grid (10,10);

1716: \draw (0,-0.66) node{$0$};

1717: \foreach \x in {1,...,9} {\draw (\x,-0.66) node{$\frac{\x}{10}$};}

1718: \draw (10,-0.66) node{$1$};

1719: %

1720: \foreach \y in {0,...,9} {\draw (-0.5,\y) node{0.\y}; }

1721: \draw (-0.5,10) node{1.0};

1722: %

1723: \draw (0.00,0.00) -- (1.00,0.00) -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00)

1724: -- (5.00,0.00) -- (6.00,0.00) -- (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) --

1725: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1726: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1727: (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40)

1728: -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) --

1729: (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1730: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1731: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00)

1732: -- (1.00,9.00) -- (2.00,8.00) -- (3.00,7.00) -- (4.00,6.00) -- (5.00,5.00) --

1733: (6.00,4.00) -- (7.00,3.00) -- (8.00,2.00) -- (9.00,1.00) -- (10.00,0.00);

1734: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1735: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1736: (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90)

1737: -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) --

1738: (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1739: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1740: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1741: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1742: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,0.00)

1743: -- (1.00,0.00) -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00) -- (5.00,0.00) --

1744: (6.00,0.00) -- (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) -- (10.00,0.00);

1745: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1746: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1747: (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90)

1748: -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) --

1749: (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1750: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1751: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,9.00)

1752: -- (2.00,8.00) -- (3.00,7.00) -- (4.00,6.00) -- (5.00,5.00) -- (6.00,4.00) --

1753: (7.00,3.00) -- (8.00,2.00) -- (9.00,1.00) -- (10.00,0.00); \draw (0.00,10.00)

1754: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1755: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1756: \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60)

1757: -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) --

1758: (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90)

1759: -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) --

1760: (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1761: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1762: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,0.00) -- (1.00,0.00)

1763: -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00) -- (5.00,0.00) -- (6.00,0.00) --

1764: (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) -- (10.00,0.00); \draw (0.00,10.00)

1765: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1766: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1767: \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60)

1768: -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) --

1769: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1770: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1771: (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,9.00) -- (2.00,8.00)

1772: -- (3.00,7.00) -- (4.00,6.00) -- (5.00,5.00) -- (6.00,4.00) -- (7.00,3.00) --

1773: (8.00,2.00) -- (9.00,1.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1774: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1775: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00)

1776: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1777: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1778: \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60)

1779: -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) --

1780: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1781: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1782: (9.00,0.81) -- (10.00,0.00); \draw (0.00,0.00) -- (1.00,0.00) -- (2.00,0.00)

1783: -- (3.00,0.00) -- (4.00,0.00) -- (5.00,0.00) -- (6.00,0.00) -- (7.00,0.00) --

1784: (8.00,0.00) -- (9.00,0.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1785: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1786: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00)

1787: -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) --

1788: (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00);

1789: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1790: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1791: (10.00,0.00); \draw (0.00,10.00) -- (1.00,9.00) -- (2.00,8.00) -- (3.00,7.00)

1792: -- (4.00,6.00) -- (5.00,5.00) -- (6.00,4.00) -- (7.00,3.00) -- (8.00,2.00) --

1793: (9.00,1.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,9.00) -- (2.00,8.00)

1794: -- (3.00,7.00) -- (4.00,6.00) -- (5.00,5.00) -- (6.00,4.00) -- (7.00,3.00) --

1795: (8.00,2.00) -- (9.00,1.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1796: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1797: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00)

1798: -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) --

1799: (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00);

1800: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1801: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1802: (10.00,0.00); \draw (0.00,0.00) -- (1.00,0.00) -- (2.00,0.00) -- (3.00,0.00)

1803: -- (4.00,0.00) -- (5.00,0.00) -- (6.00,0.00) -- (7.00,0.00) -- (8.00,0.00) --

1804: (9.00,0.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1805: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1806: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10)

1807: -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) --

1808: (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00)

1809: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1810: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1811: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1812: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1813: (10.00,0.00); \draw (0.00,10.00) -- (1.00,9.00) -- (2.00,8.00) -- (3.00,7.00)

1814: -- (4.00,6.00) -- (5.00,5.00) -- (6.00,4.00) -- (7.00,3.00) -- (8.00,2.00) --

1815: (9.00,1.00) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1816: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1817: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10)

1818: -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) --

1819: (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00)

1820: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1821: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1822: \draw (0.00,0.00) -- (1.00,0.00) -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00)

1823: -- (5.00,0.00) -- (6.00,0.00) -- (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) --

1824: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1825: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1826: (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40)

1827: -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) --

1828: (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10)

1829: -- (2.00,6.40) -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) --

1830: (7.00,2.10) -- (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00)

1831: -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) --

1832: (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00);

1833: \draw (0.00,10.00) -- (1.00,9.00) -- (2.00,8.00) -- (3.00,7.00) -- (4.00,6.00)

1834: -- (5.00,5.00) -- (6.00,4.00) -- (7.00,3.00) -- (8.00,2.00) -- (9.00,1.00) --

1835: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1836: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1837: (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40)

1838: -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) --

1839: (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1840: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1841: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,0.00)

1842: -- (1.00,0.00) -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00) -- (5.00,0.00) --

1843: (6.00,0.00) -- (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) -- (10.00,0.00);

1844: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1845: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1846: (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43)

1847: -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) --

1848: (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40)

1849: -- (3.00,4.90) -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) --

1850: (8.00,1.60) -- (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29)

1851: -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) --

1852: (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,10.00)

1853: -- (1.00,9.00) -- (2.00,8.00) -- (3.00,7.00) -- (4.00,6.00) -- (5.00,5.00) --

1854: (6.00,4.00) -- (7.00,3.00) -- (8.00,2.00) -- (9.00,1.00) -- (10.00,0.00);

1855: \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12) -- (3.00,3.43) -- (4.00,2.16)

1856: -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) -- (8.00,1.28) -- (9.00,0.81) --

1857: (10.00,0.00); \draw (0.00,10.00) -- (1.00,8.10) -- (2.00,6.40) -- (3.00,4.90)

1858: -- (4.00,3.60) -- (5.00,2.50) -- (6.00,2.40) -- (7.00,2.10) -- (8.00,1.60) --

1859: (9.00,0.90) -- (10.00,0.00); \draw (0.00,10.00) -- (1.00,7.29) -- (2.00,5.12)

1860: -- (3.00,3.43) -- (4.00,2.16) -- (5.00,1.25) -- (6.00,1.44) -- (7.00,1.47) --

1861: (8.00,1.28) -- (9.00,0.81) -- (10.00,0.00); \draw (0.00,0.00) -- (1.00,0.00)

1862: -- (2.00,0.00) -- (3.00,0.00) -- (4.00,0.00) -- (5.00,0.00) -- (6.00,0.00) --

1863: (7.00,0.00) -- (8.00,0.00) -- (9.00,0.00) -- (10.00,0.00);

1864: \end{tikzpicture}

1865: \caption{Running Time $t(p)$ and Security Level $\de'(p)$ as Functions of $p$}

1866: \label{AgatGraphs}

1867: \end{figure}

1868: %---------------------------------------------------------------------

1869: 

1870: The price we have to pay for increased security, i.e. indistinguishability of

1871: behaviours, is an increased (average) execution time. The graph on the left in

1872: Figure~\ref{AgatGraphs}\ shows how the running time (vertical axis) increases

1873: in dependence of the padding probability $p$ (horizontal axis) for the eight

1874: execution trees we have to consider in this example, i.e. for ${\tt k=000}$,

1875: ${\tt k=001}$, ${\tt k=010}$, etc. Depending on the number of bits set in

1876: ${\tt k}$ we get four different curves which show how, for example for ${\tt

1877:   k=000}$ the running time increases from $29$ time steps (for $p=0$, i.e.

1878: {\tt agat} program) to $38$ (for $p=1$, i.e. {\tt fagat} program).

1879: 

1880: We can employ the bisimilarity measures $\delta$ and $\delta'$ in order to

1881: determine the security of the partially padded program. For this we compute

1882: using our algorithm $\delta({\tt k}_i,{\tt k}_j)$ and $\delta'({\tt k}_i,{\tt

1883:   k}_j)$ for all possible keys, i.e. $i,j=0,\ldots7$. It turns out that

1884: $\delta=1$ for all values of $p<1$ and any pair of keys ${\tt k}_i$ and ${\tt

1885:   k}_j$ with $i \neq i$; only for $p=1$ we get, as one would expect,

1886: $\delta=0$ for all key pairs.  The weighted measure $\delta'$ is more

1887: sensitive and we get for example for $p=0.5$ the following values when we

1888: compare ${\tt k}_i$ and ${\tt k}_j$:

1889: \[

1890: \begin{array}{c|rrrrrrrr}

1891: \delta' &{\tt000}&{\tt001}&{\tt010}&{\tt011}&{\tt100}&{\tt101}&{\tt110}&{\tt111}\\ 

1892: \hline

1893: {\tt000}& 0.000 & 0.125 & 0.250 & 0.125 & 0.500 & 0.125 & 0.250 & 0.125 \\

1894: {\tt001}& 0.125 & 0.000 & 0.125 & 0.250 & 0.125 & 0.500 & 0.125 & 0.250 \\

1895: {\tt010}& 0.250 & 0.125 & 0.000 & 0.125 & 0.250 & 0.125 & 0.500 & 0.125 \\

1896: {\tt011}& 0.125 & 0.250 & 0.125 & 0.000 & 0.125 & 0.250 & 0.125 & 0.500 \\

1897: {\tt100}& 0.500 & 0.125 & 0.250 & 0.125 & 0.000 & 0.125 & 0.250 & 0.125 \\

1898: {\tt101}& 0.125 & 0.500 & 0.125 & 0.250 & 0.125 & 0.000 & 0.125 & 0.250 \\

1899: {\tt110}& 0.250 & 0.125 & 0.500 & 0.125 & 0.250 & 0.125 & 0.000 & 0.125 \\

1900: {\tt111}& 0.125 & 0.250 & 0.125 & 0.500 & 0.125 & 0.250 & 0.125 & 0.000 \\

1901: \end{array}

1902: \]

1903: The diagonal entries are, of course, all zero as every execution tree is

1904: bisimilar to itself. The other entries however are different from $0$ and $1$

1905: and reflect the similarity between the two keys and thus the resulting

1906: execution trees. If we plot the development of $\delta'$ as a function of $p$

1907: we observe only three patterns as depicted in the right graph in

1908: Figure~\ref{AgatGraphs}. In all three cases $\delta'$ decreases from an

1909: original value $1$ to $0$, but in different ways.

1910: 

1911: In analysing the trade-off between increased running time and security we need

1912: to define a {\em cost} function. For example, one could be faced with a

1913: situation where a certain code fragment needs to be executed in a certain

1914: maximal time, i.e. there is a (cost) penalty if the execution takes longer

1915: than a certain number of micro-seconds. In our case we will consider a very

1916: simple cost function $c(p) = 6\delta'(p) + t(p)$ with $\delta'(p)$ and $t(p)$

1917: the average $\delta'$ between all possible execution trees and $t$ the average

1918: running time. The diagram in Figure~\ref{TradeOff}\ depicts how $c(p)$,

1919: $\delta'(p)$ and $t(p)$ depend on the padding parameter $p$.

1920: 

1921: %---------------------------------------------------------------------

1922: \begin{figure}[t]

1923: \begin{center} 

1924: \begin{tikzpicture}[y=5mm,x=10mm]

1925: \draw[style=help lines] (0,3) grid[ystep=5mm,xstep=10mm] (10,10);

1926: %  \draw[style=help lines] (0,0) grid (10,10);

1927: \draw (0,2.33) node{$0$};

1928: \foreach \x in {1,...,9} {\draw (\x,2.33) node{$\frac{\x}{10}$};}

1929: \draw (10,2.33) node{$1$};

1930: % time

1931: \draw (-0.50,3.00) node{$t(p)$};

1932: \draw (0.00,3.00) -- (1.00,3.60) -- (2.00,4.20) -- (3.00,4.80) -- (4.00,5.40)

1933: -- (5.00,6.00) -- (6.00,6.60) -- (7.00,7.20) -- (8.00,7.80) -- (9.00,8.40) --

1934: (10.00,9.00);

1935: % delta'

1936: \draw (-0.50,8.50) node{$\de'(p)$};

1937: \draw (0.00,8.83) -- (1.00,7.53) -- (2.00,6.44) -- (3.00,5.54) -- (4.00,4.82)

1938: -- (5.00,4.25) -- (6.00,4.21) -- (7.00,4.09) -- (8.00,3.86) -- (9.00,3.50) --

1939: (10.00,3.00);

1940: % costs

1941: \draw (-0.50,10.00) node{${\mathbf c(p)}$};

1942: \draw[style=ultra thick] (0.00,10.00) -- (1.00,9.04) -- (2.00,8.33) --

1943: (3.00,7.85) -- (4.00,7.58) -- (5.00,7.50) -- (6.00,8.06) -- (7.00,8.51) --

1944: (8.00,8.83) -- (9.00,9.00) -- (10.00,9.00);

1945: \end{tikzpicture}

1946: \end{center}

1947: \caption{Trade-Off and Costs $c(p)$ as a Functions of $p$}

1948: \label{TradeOff}

1949: \end{figure}

1950: %---------------------------------------------------------------------

1951: 

1952: One can argue about the practical relevance of the particular cost function we

1953: chose. Nevertheless, this example illustrates already nicely the non-linear

1954: nature of security cost optimisation: The optimal, i.e. minimal, cost is

1955: reached in this case for $p=0.5$, i.e. keeping the cost of security

1956: counter measures in mind it is better to use a ``half-fixed'' program rather

1957: than a completely safe one.

1958: 

1959: %---------------------------------------------------------------------

1960: 

1961: \section{Related and Further Work}

1962: 

1963: The idea of defining a secure system via the requirement that an attacker must

1964: be unable to observe different behaviours as a result of different secrets --

1965: i.e. the system ``operates in the same way'' whatever value a secret key has

1966: -- goes back at least to the seminal work of Goguen and Meseguer

1967: \cite{GoguenMeseguer82}.

1968: 

1969: This led in a number of settings to formalisations of security concepts such as

1970: ``non-interference'' via various notions of behavioural equivalencies (see

1971: e.g. \cite{RyanSchneider99,FocardiGorrieri01}). One of the perhaps most

1972: prominent of these equivalence notions, namely {\em bisimilarity}, plays an

1973: important role in the context of security of concurrent systems but also found

1974: application for sequential programs such as in Agat's work (as the interaction

1975: between system and attacker can be modelled as a parallel composition).

1976: In order to allow for a decision theoretic analysis of security

1977: counter-measures and associated efforts it appears to be desirable to

1978: introduce a ``quantitative'' notion of the underlying behavioural equivalence.

1979: In the case of {\em bisimilarity} a first step was the introduction of the

1980: notion of {\em probabilistic bisimulation} by Larson and Skou

1981: \cite{LarsenSkou91}. However, this notion turns out to be still too strict and

1982: a number of researchers developed ``approximate'' versions; among them we just

1983: name the approaches by Desharnais et.al. \cite{Desharnais99,Desharnais02}\ and

1984: van~Breugel \cite{vanBreugel05}\ and our work

1985: \cite{CONCUR03,JCS04}\ (an extensive bibliography on this issue can be found in

1986: \cite{ABE08}). We based this current paper on the latter approach because it allows for

1987: an implementation of the semantics of pWhile via linear operators, i.e.

1988: matrices, and an efficient computation of $\de$ and $\de'$ using standard

1989: software such as {\tt octave} \cite{octave}.

1990: 

1991: Further research will be needed in order to clarify the relation between our

1992: measures $\delta$ and existing notions of {\em approximate bisimilarity}

1993: mentioned above, e.g. the $\ep$ in \cite{TCS05}. Furthermore, we also would

1994: like to shed more light on the relationship between our notion and information

1995: theoretic concepts used in the work of, for example Clark et.al.

1996: \cite{ClarkEtAL05}\ and Boreale \cite{Boreale06}.

1997: 

1998: %---------------------------------------------------------------------

1999: 

2000: \newpage

2001: 

2002: \begin{thebibliography}{10}

2003: 

2004: \bibitem{VolpanoSmith98b}

2005: Smith, G., Volpano, D.:

2006: \newblock Secure information flow in a multi-threaded imperative language.

2007: \newblock In: Proceedings of POPL'98, ACM Press (1998)  355--364

2008: 

2009: \bibitem{Kocher96}

2010: Kocher, P.:

2011: \newblock Timing attacks on implementations of {Diffie-Hellman}, {RSA}, {DSS},

2012:   and other systems.

2013: \newblock In: Proceedings of {CRYPTO} '96. Volume 1109 of Lecture Notes in

2014:   Computer Science., Springer Verlag (1996)  104--113

2015: 

2016: \bibitem{Agat00}

2017: Agat, J.:

2018: \newblock Transforming out timing leaks.

2019: \newblock In: Proceedings of POPL'00, ACM Press (2000)  40--53

2020: 

2021: \bibitem{alur94}

2022: Alur, R., Dill, D.L.:

2023: \newblock A theory of timed automata.

2024: \newblock Theoretical Computer Science \textbf{126}(2) (1994)  183--235

2025: 

2026: \bibitem{KNSW04}

2027: Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.:

2028: \newblock Symbolic model checking for probabilistic timed automata.

2029: \newblock In Lakhnech, Y., Yovine, S., eds.: Proceedings of FORMATS/FTRTFT'04.

2030:   Volume 3253 of Lecture Notes in Computer Science., Springer Verlag (2004)

2031:   293--308

2032: 

2033: \bibitem{JonssonEtAl01}

2034: Jonsson, B., Yi, W., Larsen, K.

2035: \newblock In: Probabilistic Extentions of Process Algebras. Elsevier Science,

2036:   Amsterdam (2001)  685--710

2037: 

2038: \bibitem{Stirzaker99}

2039: Stirzaker, D.:

2040: \newblock Probability and Random Variables.

2041: \newblock Cambridge University Press (1999)

2042: 

2043: \bibitem{LarsenSkou91}

2044: Larsen, K., Skou, A.:

2045: \newblock Bisimulation through probabilistic testing.

2046: \newblock Information and Computation \textbf{94} (1991)  1--28

2047: 

2048: \bibitem{TCS05}

2049: {Di Pierro}, A., Hankin, C., Wiklicky, H.:

2050: \newblock Measuring the confinement of probabilistic systems.

2051: \newblock Theoretical Computer Science \textbf{340}(1) (2005)  3--56

2052: 

2053: \bibitem{CONCUR03}

2054: {Di Pierro}, A., Hankin, C., Wiklicky, H.:

2055: \newblock Quantitative relations and approximate process equivalences.

2056: \newblock In Lugiez, D., ed.: Proceedings of CONCUR'03. Volume 2761 of Lecture

2057:   Notes in Computer Science., Springer Verlag (2003)  508--522

2058: 

2059: \bibitem{PaigeTarjan87}

2060: Paige, R., Tarjan, R.:

2061: \newblock Three partition refinement algorithms.

2062: \newblock SIAM Journal of Computation \textbf{16}(6) (1987)  973--989

2063: 

2064: \bibitem{JLAP06}

2065: {Di Pierro}, A., Hankin, C., Siveroni, I., Wiklicky, H.:

2066: \newblock Tempus fugit: How to plug it.

2067: \newblock Journal of Logic and Algebraic Programming \textbf{72}(2) (2007)

2068:   173--190

2069: 

2070: \bibitem{DerisaviEtAl03}

2071: Derisavi, S., Hermanns, H., Sanders, W.H.:

2072: \newblock Optimal state-space lumping in {M}arkov chains.

2073: \newblock Information Processing Letters \textbf{87}(6) (September 2003)

2074:   309--315

2075: 

2076: \bibitem{DovierEtAl04}

2077: Dovier, A., Piazza, C., Policriti, A.:

2078: \newblock An efficient algorithm for computing bisimulation equivalence.

2079: \newblock Theoretical Computer Science \textbf{311}(1-3) (2004)  221--256

2080: 

2081: \bibitem{TheEconomist08}

2082: {Software Bugtraps}:

2083: \newblock Software that makes software better.

2084: \newblock Economist \textbf{386}(8570) (March 2008)

2085: 

2086: \bibitem{VolpanoSmith98a}

2087: Volpano, D., Smith, G.:

2088: \newblock Confinement properties for programming languages.

2089: \newblock SIGACT News \textbf{29}(3) (September 1998)  33--42

2090: 

2091: \bibitem{GoguenMeseguer82}

2092: Goguen, J., Meseguer, J.:

2093: \newblock Security {P}olicies and {S}ecurity {M}odels.

2094: \newblock In: IEEE Symposium on Security and Privacy, IEEE Computer Society

2095:   Press (1982)  11--20

2096: 

2097: \bibitem{RyanSchneider99}

2098: Ryan, P., Schneider, S.:

2099: \newblock Process algebra and non-interference.

2100: \newblock Journal of Computer Security \textbf{9}(1/2) (2001)  75--103 Special

2101:   Issue on CSFW-12.

2102: 

2103: \bibitem{FocardiGorrieri01}

2104: Focardi, R., Gorrieri, R.:

2105: \newblock Classification of {S}ecurity {P}roperties ({P}art {I}: {I}nformation

2106:   {F}low).

2107: \newblock In: Foundations of Security Analysis and Design - Tutorial Lectures.

2108:   Volume 2171 of Lecture Notes in Computer Science., Springer Verlag (2001)

2109:   331--396

2110: 

2111: \bibitem{Desharnais99}

2112: Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.:

2113: \newblock Metrics for labeled markov systems.

2114: \newblock In: Proceedings of CONCUR'99. Volume 1664 of Lecture Notes in

2115:   Computer Science., Springer Verlag (1999)  258--273

2116: 

2117: \bibitem{Desharnais02}

2118: Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.:

2119: \newblock The metric analogue of weak bisimulation for probabilistic processes.

2120: \newblock In: Proceedings of LICS'02, IEEE (2002)  413--422

2121: 

2122: \bibitem{vanBreugel05}

2123: {van Breugel}, F.:

2124: \newblock A behavioural pseudometric for metric labelled transition systems.

2125: \newblock In Abadi, M., de~Alfaro, L., eds.: Proceedings of CONCUR'05. Volume

2126:   3653 of Lecture Notes in Computer Science., Springer Verlag (2005)  141--155

2127: 

2128: \bibitem{ABE08}

2129: ABE'08:

2130: \newblock Workshop on {A}pproximate {B}ehavioural {E}quivalences (2008) {\tt

2131:   www.cse.yorku.ca/abe08}.

2132: 

2133: \bibitem{JCS04}

2134: {Di Pierro}, A., Hankin, C., Wiklicky, H.:

2135: \newblock Approximate {N}on-{I}nterference.

2136: \newblock Journal of Computer Security \textbf{12}(1) (2004)  37--81

2137: 

2138: \bibitem{octave}

2139: Eaton, J.W.:

2140: \newblock Octave.

2141: \newblock Technical report, Free Software Foundation, Boston, MA

2142: 

2143: \bibitem{ClarkEtAL05}

2144: Clark, D., Hunt, S., Malacaria, P.:

2145: \newblock Quantitative information flow, relations and polymorphic types.

2146: \newblock Journal of Logic and Computation \textbf{15}(2) (2005)  181--199

2147: 

2148: \bibitem{Boreale06}

2149: Boreale, M.:

2150: \newblock Quantifying information leakage in process calculi.

2151: \newblock In Bugliesi, M., Preneel, B., Sassone, V., Wegener, I., eds.:

2152:   Proceedings of ICALP'06. Volume 4052 of Lecture Notes in Computer Science.,

2153:   Springer Verlag (2006)  119--131

2154: 

2155: \end{thebibliography}

2156: 

2157: %---------------------------------------------------------------------

2158: \end{document}

2159: %---------------------------------------------------------------------

2160: 

2161: