Opacity testing is formalized and studied. We specify opacity testers as well as tested systems by (timed) process algebras. We model various testers according to how sophisticated observations of tested system they can make and which kind of conclusions they can obtain. We use this technique to de ne several realistic security properties. The properties are studied and compared with other security concepts.
Introduction Several formulations of system security can be found in the literature. Many of them are based on non-interference (see [GM82]) which assumes an absence of any information ow between private and public systems activities. More precisely, systems are considered to be secure if from observations of their public activities no information about private activities can be deduced. This approach has found many reformulations for di erent formalisms, computational models and nature or \quality" of observations.
One of the most general notion is opacity (see [BKR04,BKMR06]) and many security properties can be viewed as its special cases (see, for example, [Gru07]). A predicate is opaque if for any trace of a system for which it holds there exists another trace for which it does not hold and both traces are indistinguishable for an observer. Opacity is widely studied also in process algebras framework. Here, as well as later in this paper, we mention those ones which are close to the the presented work. For example, in [Gru07,Gru12] opacity for very simple observations is studied for timed process algebra. In [Gru09] a quanti cation of opacity by means of the information theory is studied. In [Gru10,Gru12a] we de ned security properties which could be described by speci c relations on contexts. In general, opacity is an undecidable property even for very simple observation functions or predicates. On the other side, opacity is based on traces and hence inadequate for any ner "attacker" who is capable not only observe traces but also interact with systems.
The aim of this paper is twofold. On the one side, we weaken opacity by modeling both predicate and observations by processes (particularly, nite state ? Work supported by the grant VEGA 1/1333/12. processes) and hence we obtain (polynomial time) decidable properties. On the other side, we strength opacity by de ning simulation opacity which is not restricted to trace observations and which is stronger than opacity. While opacity of predicate is de ned for a given process (and an observation function), simulation opacity requires (roygly speaking) that it is opaque also for every successor of the process. Moreover, our formalism of timed process algebra, allows us to express various types of timed attacks.
The paper is organized as follows. In Section 2 we describe the timed process algebra TPA which will be used as a basic formalism. In Section 3 we present opacity and in the next section simulation opacity is de ned and studied. 2
Timed Process Algebra In this section we de ne Timed Process Algebra, TPA for short. TPA is based on Milner's CCS but the special time action t which expresses elapsing of (discrete) time is added. The presented language is a slight simpli cation of Timed Security Process Algebra introduced in [FGM00]. We omit an explicit idling operator used in tSPA and instead of this we allow implicit idling of processes. Hence processes can perform either "enforced idling" by performing t actions which are explicitly expressed in their descriptions or "voluntary idling". But in the both cases internal communications have priority to action t in the case of the parallel operator. Moreover we do not divide actions into private and public ones as it is in tSPA. TPA di ers also from the tCryptoSPA (see [GM04]). TPA does not use value passing and strictly preserves time determinacy in case of choice operator + what is not the case of tCryptoSPA.
To de ne the language TPA, we rst assume a set of atomic action symbols A not containing symbols and t, and such that for every a 2 A there exists a 2 A and a = a. We de ne Act = A [ f g; Actt = Act [ f g t . We assume that a; b; : : : range over A, u; v; : : : range over Act, and x; y : : : range over Actt. Assume the signature = Sn2f0;1;2g n, where 0 = fN ilg 1 = fx: j x 2 A [ ftgg [ f[S] j S is a relabeling functiong [fnM j M
Ag 2 = fj; +g with the agreement to write unary action operators in pre x form, the unary operators [S]; nM in post x form, and the rest of operators in in x form. Relabeling functions, S : Actt ! Actt are such that S(a) = S(a) for a 2 A; S( ) = and S(t) = t.
The set of TPA terms over the signature is de ned by the following BNF notation:
P ::= X j op(P1; P2; : : : Pn) j where X 2 V ar, V ar is a set of process variables, P; P1; : : : Pn are TPA terms, X is the binding construct, op 2 .
The set of CCS terms consists of TPA terms without t action. We will use an usual de nition of opened and closed terms where X is the only binding operator. Closed terms which are t-guarded (each occurrence of X is within some subexpression t:A i.e. between any two t actions only nitely many non timed actions can be performed) are called TPA processes. Note that N il will be often omitted from processes descriptions and hence, for example, instead of a:b:N il we will write just a:b.
We give a structural operational semantics of terms by means of labeled transition systems. The set of terms represents a set of states, labels are actions from Actt. The transition relation ! is a subset of TPA Actt TPA. We write P !x P 0 instead of (P; x; P 0) 2 ! and P 6 !x if there is no P 0 such that P !x P 0. The meaning of the expression P !x P 0 is that the term P can evolve to P 0 by performing action x, by P !x we will denote that there exists a term P 0 such that P !x P 0. We de ne the transition relation as the least relation satisfying the inference rules for CCS plus the following inference rules:
N il !t N il P !t P 0; Q !t Q0; P j Q 6!
P j Q !t P 0 j Q0
A1 P a
u:P !t u:P P !t P 0; Q !t Q0 P + Q !t P 0 + Q0
A2 S
Here we mention the rules that are new with respect to CCS. Axioms A1; A2 allow arbitrary idling. Concurrent processes can idle only if there is no possibility of an internal communication (P a). A run of time is deterministic (S). In the de nition of the labeled transition system we have used negative premises (see P a). In general this may lead to problems, for example with consistency of the de ned system. We avoid these dangers by making derivations of independent of derivations of t. For an explanation and details see [Gro90]. Regarding behavioral relations we will work with the timed version of weak trace equivalence. Note that here we will use also a concept of observations which contain complete information which includes also actions and not just actions from A and t action as it is in [FGM00]. For s = x1:x2: : : : :xn; xi 2 Actt we write P !s instead of P !x1 !x2 : : : !xn and we say that s is a trace of P . By we will denote the empty sequence of actions, by Succ(P ) we will denote the set of all successors of P . If the set Succ(P ) is nite we say that P is nite state.
Let s 2 Actt?. By jsj we will denote the length of s i.e. a number of action contained in s. By sjB we will denote the sequence obtained from s by removing all actions not belonging to B. For example, jsjftgj denote a number of occurrences of t in s, i.e. time length of s.
To express what an observer can see from system behaviour we will de ne modi ed transitions )xM which hide actions from M (as well as action). Formally, we will write P )xM P 0 for M A i P !s1 !x !s2 P 0 for s1; s2 2 (M [ f g)? and P )sM instead of P )x1 M )x2 M : : : )xnM . Instead oxf ); we will write ) and instead of )fhg we will write )h. We will write P )M if there exists P 0 such x x that P )M P 0. We will write P )b M P 0 instead of P )M P 0 if x 2 M .
We conclude this section with de nitions of variants of weak simulation and weak bisimulation.
De nition 1. Let ( TOA; Actt; !) be a labelled transition system (LTS). A relation < CCS CCS is called a weak M-bisimulation if it is symmetric and it satis es the following condition: if (P; Q) 2 < and P !x P 0; x 2 Actt then there exists a process Q0 such that Q )bx M Q0 and (P 0; Q0) 2 <. Two processes P; Q are M-bisimilar, abbreviated P M Q, if there exists a strong bisimulation relating P and Q. If it is not required that relation < is symmetric we call it Msimulation and we say that process P simulates process Q, abbreviated P M Q, if there exists a simulation relating P and Q.
and instead of
M and
M , respectively, if M = ;. 3
Opacity To formalize an information ow we do not divide actions into public and private ones at the system description level, as it is done for example in [GM04,BG04], but we use a more general concept of observation and opacity. This concept was exploited in [BKR04] and [BKMR06] in a framework of Petri Nets and transition systems, respectively.
First we de ne observation function on sequences from Actt?.
De nition 2 (Observation). Let be a set of elements called observables. Any function O : Actt? ! ? is an observation function. It is called static /dynamic /orwellian / m-orwellian (m 1) if the following conditions hold respectively (below we assume w = x1 : : : xn): { static if there is a mapping O0 : Actt ! [f g such that for every w 2 Actt? it holds O(w) = O0(x1) : : : O0(xn), { dynamic if there is a mapping O0 : Actt? ! [ f g such that for every w 2 Actt? it holds O(w) = O0(x1):O0(x1:x2) : : : O0(x1 : : : xn), { orwellian if there is a mapping O0 : Actt Actt? ! [ f g such that for every w 2 Actt? it holds O(w) = O0(x1; w):O0(x2; w) : : : O0(xn; w), { m-orwellian if there is a mapping O0 : Actt Actt? ! [ f g such that for every w 2 Actt? it holds O(w) = O0(x1; w1):O0(x2; w2) : : : O0(xn; wn) where wi = xmaxf1;i m+1g:xmaxf1;i m+1g+1 : : : xminfn;i+m 1g.
In the case of the static observation function each action is observed independently from its context. In the case of the dynamic observation function an observation of an action depends on the previous ones, in the case of the orwellian and m-orwellian observation function an observation of an action depends on the all and on m previous actions in the sequence, respectively. The static observation function is the special case of m-orwellian one for m = 1. Note that from the practical point of view the m-orwellian observation functions are the most interesting ones. An observation expresses what an observer - eavesdropper can see from a system behavior and we will alternatively use both the terms (observation - observer) with the same meaning.
Now suppose that we have some security property. This might be an execution of one or more classi ed actions, an execution of actions in a particular classi ed order which should be kept hidden, etc. Suppose that this property is expressed by predicate over process traces. We would like to know whether an observer can deduce the validity of the property just by observing sequences of actions from Actt? performed by given process.
The observer cannot deduce the validity of if there are two traces w; w0 2 Actt? such that (w); : (w0) and the traces cannot be distinguished by the observer i.e. O(w) = O(w0). We formalize this concept by opacity. De nition 3 (Opacity). Given process P , a predicate over Actt? is opaque w.r.t. the observation function O if for every sequence w, w 2 T r(P ) such that (w) holds and O(w) 6= , there exists a sequence w0; w0 2 T r(P ) such that : (w0) holds and O(w) = O(w0). The set of processes for which the predicate is opaque with respect to O will be denoted by OpO.
The de nition of opacity (see De nition 3) of predicate is asymmetric in the sense that if (w) does not hold than it is not required that there exists another trace for which it holds (in general OpO 6= Op:O ). This means that opacity says something to an intruder which tries to detect only validity of (if it is opaque, than validity cannot be detected) but not its non-validity i.e. it says nothing about predicate : . Hence we de ne strong variant of opacity. De nition 4 (Strong Opacity). Given process P , a predicate over Actt? is strongly opaque w.r.t. the observation function O if for every sequence w, w 2 T r(P ) such that (w) holds and O(w) 6= , there exists a sequence w0; w0 2 T r(P ) such that : (w0) holds and O(w) = O(w0). Moreover, for for every sequence w, w 2 T r(P ) such that : (w) holds and O(w) 6= , there exists a sequence w0; w0 2 T r(P ) such that (w0) holds and O(w) = O(w0). The set of processes for which the predicate is opaque with respect to O will be denoted by sOpO.
such that sOp
O O
Op OpO.
O for every and O. Moreover, there exist and O Proof. Main idea. Let P 2 sOpO. Then for every trace of P for which holds there exists a trace indistinguishable by observation function O for which does not hold and hence P 2 OpO. Let us consider process P = h:l:N il +l:N il +l0:N il and let holds for tracecs which contain action h and observation function O which hide h action. Then we have P 2 OpO but P 62 sOpO and hence the inclusion is proper, i.e sOpO OpO for such and O. We start with a motivation example. Let us consider process P = l:h:l0:N il + l:(h:l0:N il + l0:N il), an observation function which does not see action h and a predicate which holds for sequences containing h action. It is easy to check that this predicate is opaque in this setting. That means than an attacker which can observe traces of P cannot deduce whether action h has occurred or nor. On the other side for a "simulation attacker" i.e. the attacker which can not only observe traces but can interact with systems, the predicate is not "opaque" anymore. This is a natural consequence of simulation being more powerful then just a trace inclusion. Now we will extend the notion of opacity to re ect more powerful attackers than those ones which just observe traces or alternatively, predicate should be opaque not only for a given process P but also for every its successor.
De nition 5 (Simulation Opacity). Given a set of processes <, predicate over Actt? is simulation opaque for < w.r.t. the observation function O if for every P 2 < if P !s P 0 for such s that (s) holds and o(s) 6= then there exists s0 such that : (s0) holds, O(s) = O(s0) and P s!0 and moreover P 0 2 <. Predicate is simulation opaque for process P with respect to O (denoted P 2 SOpO) if P 2 < for some simulation opaque < with respect to and O.
Now let us return to process P and the predicate and the observation function from the beginning of this section. Now we can check that P is not simulation opaque in this setting. This is also the proof that an inclusion from the next proposition is proper.
O such that SOpO
O OpO.
OpO for every and O. Moreover, there exist and Proof. The main idea. Let P 2 SOpO. Then we have that for every trace s of P for which holds there exists another trace s0 for which does not hold and both traces cannot be distinguished by O. Hence P 2 OpO. The example from of this section we see that the inclusion can be proper.
The simulation opacity is de ned for arbitrary predicates and observation functions. Now we we will reformulate it for those ones which can be expressed by process algebras. Now we will model simulation opacity in a process algebra setting. Suppose that Actt \ = ftg and hence we extend the set of actions A by . We combine a process which checks validity of with a process which computes observation function O into two process O and O: . Now we de ne process O .
De nition 6. Process O is called process de nition of predicate and observation function O over sequences of actions if for every P it holds (P jO ) n A )o (P 0jO ) n A i P !s P 0 such that (s) and O(s) = o.
Note that we expect that process O makes some computation resulting on observable o and then it returns to the initial state (actually, to be more precise, we should write to the process bisimilar with it). Now we will de ne simulation opacity with respect to O and O: (see Fig. 1). Its de nition is a reformulation of De nition 5 in process algebra setting.
o
P s
O o
P
s-0 O: De nition 7. We say that process P is simulation opaque with respect to O and O: (denoted P 2 SO(O ; O: ) i (P jO ) n A (P jO: ) n A.
In fact, from the following proposition we see that both types of simulation opacity coincide for those predicated and observation functions which can be expressed by processes.
Proposition 2. Let O and O: are process de nitions of observation function O and predicates and : , respectively. Then SOpO = SO(O ; O: ). Proof. The main idea. Process de nition O and O: mimic both observations and predicates validity (see De nition 7). Moreover, the simulation re ects the fact that after each "step" the resulting process is again opaque and hence similation opaque.
Many trace based security properties can be viewed as special cases of opacity (see for example [Gru07]) but not those ones which are based on more powerful equivalences. Now we show how we can express by simulation opacity a stronger security property. We de ne an absence-of-information- ow property - Bisimulation Strong Nondeterministic Non-Interference (BSNNI, for short, see [FGM00]). Suppose that all actions are divided in two groups, namely public (low level) actions L and private. Process P has BSNNI property (we will write P 2 BSN N I) if P n H behaves like P for which all high level actions are hidden for an observer. To express this hiding we introduce hiding operator P=M; M A, for which it holds if P !a P 0 then P=M !a P 0=M whenever a 62 M [ M and P=M ! P 0=M whenever a 2 M [ M . Formal de nition of BSNNI follows.
De nition 8. Let P 2 T P A. We say that P has BSNNI property, and we write P 2 BSN N I i P n H P=H.
Example 1. Let (s) holds i s contains actions from H and let O(s) = o such that o = ol1 : : : oln where sjL = l1:l2 : : : ln.
Then the following process = foxjx 2 L,
O =
X:(X x:ox:X + X x: Y:(X x:ox:Y + X x:Y )) x2L x2H x2L x2H is the process de nition of predicate
and observation function O.
O: =
X:(X x:ox:X) x2L is the process de nition of predicate : and observation function O.
Proposition 3. P 2 BSN N I i P 2 SO(O ; O: ) for O ; O: previous example. de ned in the Proof. Sketch. Process O outputs ox for every low level action which can be performed by P and switches to "accepting" state after the rst high level action occurs. Similarly for O: . In de nition of BSNNI the weak bisimulation is exploited but clearly, everything which can be performed by P n H can be performed by P=H and hence no more then simulation is needed.
Now we can return to the strong opacity. First we de ne its simulation version.
De nition 9 (Strong Simulation Opacity). Given a set of processes <, predicate over Actt? is strongly simulation opaque for < w.r.t. the observation function O if for every P 2 < if P !s P 0 for such s that (s) holds and o(s) 6= then there exists s0 such that : (s0) holds , O(s) = O(s0) and P and P 0 2 < and, moreover, P !s P 00 for such s that : (s) holds and o(s) 6= then there exists s0 such that (s0) holds , O(s) = O(s0) and P s!0, and P 00 2 <. Predicate is strongly simulation opaque for process P with respect to O (denoted P 2 sSOpO) if P 2 < for some strongly simulation opaque < with respect to and O. s!0,
Similarly to the opacity, its stronger version is really di erent as it is stated by the following proposition.
and O such that sSOp
O O
SOpO SOpO.
for every and O. Moreover, there exist Proof. The proof is just a variation of the proof of Proposition 1. De nition 10. We say that process P is strongly simulation opaque with respect to O and O: (denoted P 2 sSO(O ; O: ) i (P jO ) n A (P jO: ) n A. Proposition 5. Let O and O: are process de nitions of observation function O and predicates and : , respectively. Then sSOpO = sSO(O ; O: ). Proof. Again, the proof is similar as the proof of Proposition 2. sOpO
SOpO
To complete a relationship between proposed opacity concepts we have the following proposition.
Proposition 6. The relation between proposed opacities is depicted on Fig. 2. Proof. First we prove that sSOpO sOpO. Let P 2 sSOpO. Since for every sequence for which holds there exists observationally equal one, for which it does not hold and vice versa, we have P 2 sOpO. Now let us consider process P = l:l0:N il + l:(h:l0:N il + l0:N il), an observation function which does not see action h and a predicate which holds for sequences containing h action. It easy to check that P 2 SOpO but P 62 sOpO. For process P 0 = l:l0:N il + l:h:l0:N il we have P 0 62 SOpO but P 0 2 sOpO. The rest of the proof follows from Lemma 1, Propositions 1 and 4.
As it was mentioned, the opacity properties could be undecidable even for very simple observation functions or predicates (depending on their mutual combination). Here we can obtain its decidability by restrictions put on O and O: , respectively. Note that existence of O: for given O is not guaranteed in general due to Turing power of TPA. As regards observation function, m-orwellian ones are the most interesting, since for their computations we do not need innite memory and still the most of real attacks are based on them. As regards predicates, again those ones, which can be associated with nite automata are the most useful and frequent ones. If a combination of an observation function and predicates results in nite state process algebra the resulting properties are decidable. We elaborate this more precisely now.
We say that process E emulates an observational function O if it produces the corresponding output after receiving input traces. Formally, for every w 2 Actt it holds O(w) = o i (Ejw:N il) n A o.
Lemma 2. For every m-orwellian observation function there exists nite state process which emulates it.
Proof. Sketch. Emulating process has to record the previous m inputs from emulated trace to produce an output. Emulation is straightforward. If jAj = n then process which emulates given m-orwellian function has O(mn) states.
We call predicate nitely de nable, if there exist nite state process T such that for every w 2 Actt (w) holds i (T jw:N il) n A p:N il where p is a new symbol indicating the successful termination.
Proposition 7. Let and : are nitely de nable. Then opacity properties SOpO and sSOpO could be decided in time O((n:m:k:jAj)6) and O((n:m:k:jAj)3) for nite state processes and every m-orwellian observation function O, where n; m; k are numbers of states of P , process emulating O and maximum of number of states of processes corresponding to ; : , respectively.
Proof. Sketch. We combine processes ; : and O. First we need a special process which duplicates all action and one copy is send to process corresponding to the predicate and to proces for observation function. The size of this auxiliary process is O(jAj). Hence the overall size of the process is n:m:k:jAj. The rest of the proof follows from complexity results for weak simulation and weak bisimulation (see [CPS90,KS83]).
If we have a process which does not belong to SOpO for some and O then this means that the process could be jeopardize by an attacker which can react to process by means of O and is interested in validity of . But there are attacks which are not covered by our framework. For example, timing attacks, which have a particular position among attacks against systems security. They represent a powerful tool for \breaking" \unbreakable" systems, algorithms, protocols, etc. For example, by carefully measuring the amount of time required to perform private key operations, attackers may be able to nd xed Di e-Hellman exponents, factor RSA keys, and break other cryptosystems (see [Ko96]). This idea was developed in [DKL98] where a timing attack against smart card implementation of RSA was conducted.
We can extend our framework so that we can model also timing attacks and we can distinguish them from ordinary attacks. Here we formulate the property for simulation opacity but the same can be done also for strong simulation opacity.
De nition 11. We say that process P is jeopardized by timing attack on validity of with a given observation function i (P jO ) n A 6 (P jO: ) n A and (P jO ) n A ftg (P jO: ) n A.
Example 2. Let n;m(s) for 1 < n < m holds i s = s1:h:s2:h0:s3; h; h0 2 H such that n js2jftgj m and s1; s2; s3 2 (L [ ftg) , i.e. n;m(s) holds if s contains two private actions from H and time elapsing between their occurrences is between n and m time units and observation function see just low level actions and elapsing of time. Then the following process
O
X:(X x:ox:X + X x:F 0) x2L x2H
F 0 =
X:(X x:ox:X + t:F1); Fi =
X:(X x:ox:X + t:Fi+1) Fi =
X:(X x:ox:X + t:Fi0+1) for i < n and for i = n, for i < m and
Fi0 =
X:(X x:ox:X + X x:xg:F 00 + t:Fi0+1)
X:(X x:ox:X + X x:o:X +
X x:ox:O
+ X x:o:O ) x2L x2H x2L x2H is the process de nition of predicate n;m. Similarly, for predicate : n;m we can construct an appropriate nite state process. Clearly, timed proces are jeopardize by timing attacks on validity of n;m. 5
Conclusions We have presented generalization of opacity called simulation opacity and we have elaborated it in timed process algebra setting. This concept o ers not only an uniform framework for security theory but can be used to model more elaborated security properties than traditional ones and moreover, by careful choice of processes expressing predicated and observations we can obtain properties which can be e ectively checked (note that in general, opacity is undecidable). By this concept we can also naturally model security with respect to limited time length of an attack, with a limited number of attempts to perform an attack and so on.
The presented approach allows us to use also other types of process algebras enriched by operators expressing also other properties (space, distribution, networking architecture, processor or power consumption and so on) and in this way also other types of attacks which exploit these information to detect information ow through various covert channels can be described.
Our approach limits us to predicates and observation functions (i.e. observers) which can be expressed by process algebra processes. In fact, this restriction does not represent any real limitation. Practically, all predicates and observation function of interest (used in known attacks) can be described by nite state processes and there is even no need to exploit full universal power of process algebras. In other words, it has no practical meaning to consider predicates and observation functions which cannot be e ectively computed.