Time insertion functions as a way how to guarantee state-based security with respect to timing attacks are proposed and studied. As regards the security property, we work with the property called process opacity. First, we define timing attacks and later we show how security with respect to them can be enforced by such functions. The time insertion function can alter the time behaviour of the original system by inserting some time delays to guarantee its security. We investigate conditions under which such functions do exist and also some of their properties.
[
As regards formalism, we will work with a timed process algebra and opacity, which is
the security property based on an absence of information flow. This formalism enables us to
formalize timing attacks. In [
The paper is organized as follows. In Section 2 we describe the timed process algebra TPA which will be used as a basic formalism and information flow state-based security process opacity. The next section is devoted to time insertion functions as a way how to guarantee state this security property with respect to timing attacks.
In this section we briefly recall Timed Process Algebra, TPA for short (for more details see [
To define the language TPA, we first assume a set of atomic action symbols not containing symbols and , and such that for every ∈ there exists ∈ and = . We define = ∪ { }, = ∪ {}, = ∪ {}. We assume that , , . . . range over , , , . . . range over , and , . . . range over .
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 . The transition relation → is a subset of TPA × × TPA. We write → ′ instead of (, , ′) ∈ → and ̸ → if there is no ′ such that → ′. The meaning of the expression → ′ is that the term can evolve to ′ by performing action , by → we will denote that there exists a term ′ such that → ′. We define the transition relation as the least relation satisfying the inference rules for CCS plus the following inference rules:
→ 2 be performed by , i.e. ( ) = {| →., ∈ * }.
For = 1.2. . . . ., ∈ we write → instead of →1 →2 . . . → and we say that is a trace of . The set of all traces of will be denoted by ( ). By we denote the empty sequence and by * we denote the set of sequences of elements from . We use ⇒ for transitions including actions (see [16]). By | we will denote the sequence obtained from by removing all actions not belonging to . By ( ) we will denote a set of actions which can
We define two behavior equivalences trace equivalence and weak bisimulation, respectively (see [16]).
′}.
The set of weak traces of process is defined as ( ) = { ∈ ⋆|∃ ′. ⇒ Two processes and are weakly trace equivalent if ( ) = (). relating and .
Let (TPA, , →) be a labelled transition system (LTS). A relation ℜ ⊆ TPA× TPA is called a weak bisimulation if it is symmetric and it satisfies the following condition: if (, ) ∈ ℜ and → ′, ∈ then there exists a process ′ such that ⇒̂︀ ′ and ( ′, ′) ∈ ℜ Two processes , are weakly bisimilar, abbreviated ≈ , if there exists a weak bisimulation .
To formalize an information flow we do not divide actions into public and private ones at the system description level, as it is done for example in [18], but we use a more general concept of observation and opacity. This concept was exploited in [19] and [20] in a framework of Petri Nets and transition systems, respectively. Firstly we define observation function on sequences from ⋆. Various variants of observation functions difers according to contexts which they take into account. For example, an observation of an action can depend on the previous actions. ⋆ ( ≥
→
Θ⋆ is an observation function. It is called static /dynamic /orwellian / m-orwellian
Let Θ be a set of elements called observables. Any function : 1) if the following conditions hold respectively (below we assume = 1 . . . ): () = ′(1) . . . ′(), • static if there is a mapping ′ : → Θ ∪ { } such that for every ∈ ⋆ it holds • dynamic if there is a mapping ′ : ⋆ →
Θ ∪ { } such that for every ∈ ⋆ it holds () = ′(1).′(1.2) . . . ′(1 . . . ), it holds () = ′(1, ).′(2, ) . . . ′(, ), • orwellian if there is a mapping ′ : × ⋆ → Θ ∪ { } such that for every ∈ ⋆ = {1,− +1}.{1,− +1}+1 . . . {,+− 1}. • m-orwellian if there is a mapping ′ : × ⋆ → Θ ∪ { } such that for every ∈ ⋆ it holds () = ′(1, 1).′(2, 2) . . . ′(, ) where 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 previous actions in the sequence, respectively. The static observation function is the special case of m-orwellian one for = 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. Note that the same action can be seen diferently during an observation (except static observation function) and this express a possibility to accumulate some knowledge by intruder. For example, an action not visible at the beginning could become somehow observable. From now on we will assume that Θ ⊆ .
Now let us assume hat an intruder is interested whether a given process has reached a state with some given property which is expressed by a (total) predicate. This property might be process deadlock, capability to execute only traces with some given actions, capability to perform at the same actions form a given set, incapacity to idle (to perform action ) etc. We do not put any restriction on such predicates but we only assume that they are consistent with some suitable behavioral equivalence. The formal definition follows.
Definition 4. We say that the predicate over processes is consistent with respect to relation ∼= if whenever ∼= ′ then ( ) ⇔ ( ′).
As the consistency relation ∼= we could take bisimulation, weak bisimulation, weak trace equivalence or any other suitable equivalence.
An intruder cannot learn validity of predicate observing process’s behaviour if there are two traces, undistinguished for him (by observation function ), where one leads to a state which satisfy and another one leads to a state for which ¬ holds. The formal definition follows.
Definition 5 (Process Opacity). Given process , a predicate over processes is process opaque w.r.t. the observation function whenever → ′ for ∈ * and ( ′) holds then there exists ′′ such that ′ → ′′ for some ′ ∈ * and ¬( ′′) holds and moreover () = (′). The set of processes for which the predicate is process opaque w.r.t. to the will be denoted by .
Timing attacks belong to powerful tools for attackers who can observe or interfere with systems in real time. On the other side these techniques is useless for of-line systems and hence they could be consider safe with respect to attackers who cannot observe (real) time behaviour. By the presented formalism we have a way how to distinguish these two cases. First we define untimed version of an observation function, i.e. a function which does not take into account time information. From now on we will consider observation functions : ⋆ → ⋆ for which there exists untimed variants . Function is untimed variant of if () = (|), i.e. untimed variant represents an observer who does not see elapsing of time since both traces, with and without actions , are seen equally. Now we can formally describe situation when a process could be jeopardized by a timing attack i.e. is secure only if an observer cannot see elapsing of time.
Definition 6 (Timinig Attacks). We say that process is prone to timing attacks with respect to and if ̸∈ but ∈ .
Example 1. Let us assume an intruder who tries to learn whether a private action ℎ was performed by a given process while (s)he can observe only public action but not ℎ itself. Then process = .. + ... is not opaque for static observation function () = for ̸= , () = and (), ¬() hold, i.e. ̸∈ . But if an observer cannot see elapsing of time this process is opaque, i.e. ∈ .
From now on we will consider only processes which are prone to timing attacks (see Definition
6) and moreover we will assume that predicate is decidable. There are basically three ways
how to solve vulnerability to timing attacks except putting a system of-line. First, redesign
the system, put some monitor or supervisor which prevents dangerous behavior which could
leak some classified information (see, for example, [
Definition 7 (Time Insertion function). Any function ℱ : ⋆ → ⋆ is an insertion
function if for every ∈ * we have ≪ {} ℱ (). It is called static /dynamic /orwellian /
morwellian ( ≥ 1) if the following conditions hold respectively (below we assume = 1 . . . ):
• static if there is a mapping : → {}* such that for every ∈ ⋆ it holds
ℱ () = 1. (1).2. (2) . . . . (),
• dynamic if there is a mapping : ⋆ → {}* such that for every ∈ ⋆ it holds
ℱ () = 1. (1).2. (1.2) . . . . (1. . . . .),
• orwellian if there is a mapping ′ : × ⋆ → {}* such that for every ∈ ⋆ it
holds ℱ () = 1. (1, ).2. (2, ) . . . . (, ),
= {1,− +1}.{1,− +1}+1 . . . {,+− 1}.
• m-orwellian if there is a mapping ′ : × ⋆ → {}* such that for every ∈ ⋆ it
holds ℱ () = 1. (1, 1).2. (2, 2) . . . . (, ),
Note that contrary to general insertion function (see [
Definition 8. We say that process can be immunized for process opacity with respect to a predicate over ⋆ and the observation function if for every ′, → ′ such that ( ′) holds and there does not exists ′′ such that →′ ′′ for some ′ such that () = (′) and ( ′′) does not hold, there exist , ≪ {} such that → ′′ and and there exists ′′′ and In Fig. 1 process immunization is depicted.
=⇒ ′ ̸=⇒ =⇒ ′′ =⇒ ( ′) ¬( ′′) ( ′) ¬( ′′′) () ‖ (′) () ‖ (′′)
Now we will study an existence of time insertion functions. First we need some notations. We begin with observational functions which do not see actions.
Definition 9. We say that observational function is not sensitive to action if () = (|) for every ∈ * . Otherwise we say that is sensitive to action. Example 2. Process , = . + (.|¯. ) ∖ {}, cannot be immunized if is sensitive to action and (), ¬() hold. An immunization should put a time delay into the trace performed by the right part of the process but this subprocess cannot perform action due to the inference rule before communication by means of channel .
Lemma 1. Let is prone to timing attack with respect to and . Let ̸∈ ( ), is sequential (i.e. does not contain parallel composition) and is static. Then can be immunized.
Another problem, which causes that processes cannot be immunized, is related to observation of time, namely, if this observation is context sensitive, as it is stated by the following example. Example 3. Process , = ℎ.. + .. cannot be immunized for dynamic such that (.ℎ.* .′) = (.′), (..′) = ()..(′), if does not end with action ℎ we have (..′) = ()..(′), and (), ¬() hold.
Definition 10. We say that observational function is time non-contextual if () = (′) for every , ′ such that ≪ {} ′.
Proposition 1. Let process is prone to timing attacks with respect to and time non-contextual observation function which does not see . Then can be immunized for opacity with respect to timing attacks.
Proof 1. The main idea. Let ̸∈ but ∈ . This means that there exists a sequence and ′ such that → ′, ( ′) holds and there does not exist ′′ such that →′ ′′ for some ′ such that () = (′) and ( ′′) does not hold.
Suppose that cannot be immunized, i.e. for every , ≪ {} if → ′′′, ( ′′′) holds, there does not exist ′′′′′ such that →′′ ′′′′ for some ′′ such that () = (′′′). But due to our assumption we have () = () and hence it is with contradiction that is prone to timing attacks.
Corollary 1. Let is a static observation function such that ( ) = and () = . Then process which is prone to timing attacks with respect to and observation function can be immunized for process opacity with respect to timing attacks.
Under some special conditions time insertion functions can be computed efectively a it is stated by the following proposition.
Proposition 2. Let process is prone to timing attacks with respect to and time non-contextual observation function which does not see . Then can be immunized for opacity with respect to timing attacks by a m-orwellian insertion function, moreover such one, which can be emulated by finite state process.
Proof 2. Sketch. The prove follows an idea from Proposition 3 and Theorem 4.10 and Lemma
4.5.in [
Definition 11. We say that predicate is time sensitive if whenever ( ) holds for then there exists , > 0 such that → ′ and ( ′) does not hold.
Proposition 3. Let process is prone to timing attacks with respect to time sensitive predicate ¬ and time non-contextual observation function which does not see . Then can be immunized for opacity with respect to timing attacks, and .
Proof 3. Sketch. By inserting some time actions after performing a sequence we can always reach a state for which holds and hence becomes safe with respect to ¬. Corollary 2. Let process is prone to timing attacks with respect and time non-contextual observation function which does not see . Let ¬ is not time sensitive predicate then can be immunized for opacity with respect to timing attacks and and.
In general, we cannot decide whether process can be immunized as it is stated by the following proposition. Fortunately, it is decidable for the most important static and m-orwellian observation functions.
Proposition 4. Immunizability is undecidable i.e. it cannot be decided whether can be immunized for opacity with respect to timing attacks.
Proof 4. Sketch. Let represents i-th Turing machine under some numeration of all Turing machines. We start with generalized process from Example 3. Let = ℎ.. + ∑︀∈ ... Let (.ℎ..′) = (.′) whenever halts with the empty tape and (.ℎ..′) = ()..(′) otherwise. It is easy to check that immunization of is undecidable. Proposition 5. Immunizability is decidable for static and m-orwellian observation function . Proof 5. According to Proposition 3 it is enough to show that observation function is time noncontextual observation function and it does not see . Clearly both these properties are decidable for static and m-orwellian observation functions.
We have investigated time insertion functions for timed process algebra which enforce the
security with respect to timing attack formalized process opacity. Time insertion functions
add some delays to system’s behaviour to prevent a timing attack. We study an existence of
an insertion function for a given process, given observational function and a predicate over
processes. In future work we plan to investigate minimal insertion functions, i.e. such functions
which add as little as possible time delays to guarantee process’s security with respect to timing
attacks. The presented approach allows us to exploit also process algebras enriched by operators
expressing other "parameters" (space, distribution, networking architecture, power consumption
and so on). Hence we could obtain security properties which have not only theoretical but
also practical value. Moreover, we can use similar techniques as in [21] to minimize time,
as well as other resources, added to process’s behaviour. Moreover, we plan to model both
observation functions as well as predicates over processes by processes themselves, to obtain
some complexity results as it was done in [
This work was supported by the Slovak Research and Development Agency under the Contract no. APVV-19-0220 (ORBIS) and by the Slovak VEGA agency under Contract no. 1/0778/18 (KATO).