Supervisory control as a way how to guarantee security of processes is discussed and studied. We work with a security property called processes opacity and we investigate how it can be enforced. Supervisors can restrict behaviour of the original systems by enabling or disabling some actions to guarantee its security. We study maximal supervisors as the least restricting supervisory control processes. Moreover, we study also enhanced supervisory control which can add idling between system's action to prevent timing attacks.
? Work supported by the grant VEGA 1/0778/18. most general one and many other security properties could be viewed as its special cases (see, for example, [Gru15,Gru12,Gru11,Gru10,Gru08,Gru07]). Opacity properties could be divided into two types: language based opacity, expressing security (privacy) of system's actions or traces of actions and state based one, concentrating on system's states (see an overview paper [JLF16]). The former one is much more studied for process algebra's formalism. But also for the later one there is some research already done. In [Gru15] we consider an intruder who wants to discover whether a process reaches a con dent state. Resulting security property is called process opacity. It turned out that in this way some new security aws could be expressed. If a process is not secure with respect to process opacity we can either re-design its behavior, what might be costly, di cult or even impossible, in the case that it is already part of a hardware solution, proprietary rmware and so on or we can use supervisory control (see [RW89]) to restrict system's behaviour in such a way that the system becomes secure. A supervisor can see (some) system's actions and can control (disable or enable) some set of system's action. In this way it restricts system's behaviour to guarantee its security. This is a trade-o between security and functionality. But in many cases it is not a fatal problem. Suppose that a communication protocol can reach (with a low probability) a state which is not secure. In that case the transmission of a packet is interrupted and it should start from the begging. Sometimes this restriction has even smaller impact on system's behavior. Suppose that the system can perform action a and b in an arbitrary order but only a sequence b:a could leak some classi ed information about intermediate states. Restricting this sequence make system secure but could not have in uence on overall system's functionality. In this paper we do not assume any relation among a set of actions visible for an intruder, a set of actions visible for a controller and a set of controllable actions, i.e. sets EI ; ES ; EC , respectively, similarly to [TLSG18]. Note that in [DDM10] it is assumed that EI ES (or ES EI ) and EC ES . In [YL10] EI ES is assumed and in [TLSG16] EC ES is assumed. As regards the related work, besides already mentioned works there is a large body of work on controller synthesis in temporal model checking. From the rest we mention just two papers. In [RS01] the idea of controller to enforce secure information ow is discussed for language based security in process algebra setting. Opacity-enforcing (called strategic noninterference) was proposed and investigated for transition systems in [JT15].
Timing attacks, as side channel attacks, represent serious threat for many systems. They allow intruders \break" \unbreakable" systems, algorithms, protocols, etc. Even relatively recently discovered possible attacks on most of currently used processors (Meltdown and Spectre) also belong to timing attacks. To protect systems against some type of timing attacks we propose to enhance capabilities of the supervisory control. Such controller can add some idling between actions to enforce process's security.
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 supervisory control. The next section contains some basic de nition on information ow security and process opacity. Sections 5 and 6 deals with supervisory and enhanced supervisory control for process opacity, respectively. 2
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" (i.e. for example, the process a:N il can perform t action since it is not contained the process speci cation). But in both cases internal communications have priority to action t in the parallel composition. 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 determinancy 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; At = A [ ftg; 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
XP 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 subterm t:A i.e. between any two t actions only nitely many non timed actions can be performed) are called TPA processes.
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) i.e. performing of t action does not lead to the choice between summands of +. 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].
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 . The set of all traces of P will be denoted by T r(P ). By we will denote the empty sequence of actions, by Succ(P ) we will denote the set of all successors of P i.e. Succ(P ) = fP 0jP !s P 0; s 2 Actt g. If the set Succ(P ) is nite we say that P is a nite state process. We de ne modi ed transitions )xM which "hide" actions from M . Formally, we will write P )xM P 0 for M Actt i P !s1 !x !s2 xP 0 for s1; s2 2 M ? and P )sM instead of P )x1 M )M : : : )xnM . We will write P )M if there exists P 0 such that P )M P 0.
x2 x We will write P )bx M P 0 instead of P )M P 0 if x 2 M . Note that )xM is de ned for arbitrary action x but in de nitions of security properties we will use it for actions (or sequence of actions) not belonging to M . We can extend the de nition of )M for sequences of actions similarly to !s . 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. By Sort(P ) we will denote the set of actions from A which can be performed by P . The set of traces of process P is de ned as L(P ) = fs 2 Actt?j9P 0:P )s P 0g. The set of weak timed traces of process P is de ned as Lw(P ) = fs 2 (A[ftg)?j9P 0:P )sf g P 0g. Two processes P and Q are weakly timed trace equivalent (P 'w Q) i Lw(P ) = Lw(Q). We conclude this section with de nitions of M-bisimulation and weak timed trace equivalence. De nition 1. Let (TPA; Actt; !) be a labelled transition system (LTS). A relation < TPA TPA is called a 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 M-bisimulation relating P and Q. 3
In this section we introduce some basic concepts of supervisory control theory. For more details see [RW89]. Let us assume deterministic nite automaton (DFA) G = (X; E; ; x0), where X is the nite set of states, E is the set of events, : X E ! X is the (partial) transition function, x0 2 X is the initial state. The transition function can be naturally extended to strings of events. The generated language of G = (X; E; ; x0) is de ned as L(G) = fs; s 2 E such that (x0; s) is de nedg.
The goal of supervisory control is to design a control agent (called supervisor) that restricts the behavior of the system within a speci cation language K L(G). The supervisor observes a set of observable events ES E and is able to control a set of controllable events EC E. The supervisor enables or disables controllable events. When an event is enabled (resp., disabled) by the supervisor, all transitions labeled by the event are allowed to occur (resp., prevented from occurring). After the supervisor observes a string generated by the system it tells the system the set of events that are enabled next to ensure that the system will not violate the speci cation.
A supervisor can be represented by Sup = (Y; ES ; s; y0; ), where (Y; ES ; s; y0) is an automaton and : Y ! fE0 EjEUC E0g where EUC = E n EC speci es the set of events enabled by the supervisor in each state. System G under the control of a suitable supervisor Sup is denoted as Sup=G, and it satis es L(Sup=G) K.
De nition 2 (Controllability). Given a DF AG, a set of controllable events EC , and a language K L(G), K is said to be controllable (wrt L(G) and EC ) if
K where K is the pre x closer of K.
The controllability of K requires that for any pre x s; s 2 K, if s followed by an uncontrollable event e 2 EUC is in L(G), then it must also be a pre x of a string in K.
De nition 3 (Observability). Given a DF AG, a set of controllable events EC , a set of observable events ES , and a language K L(G), K is said to be observable (wrt L(G), ES and EC ) if for all s; s0 2 K and all e 2 EC such that se 2 L(G), s =S s0 (s =S s0 is means that strings are equal with respect to the set ES ), s:e 2 K.
Observability requires that supervisors observation of the system (i.e., the projection of s on ES ) provides su cient information to decide after the occurrence of a controllable event whether the resultant string is still in K . Proposition 1. Let K L(G) be a pre x-closed nonempty language, EC the set of controllable events and ES the set of observable events. There exists a supervisor Sup such that L(Sup=G) = K if and only if K is controllable and observable. 4
In this section we will present our working security concept. First we de ne the absence-of-information- ow property - Strong Nondeterministic Non-Interference (SNNI, for short, see [FGM00]). Suppose that all actions are divided into two groups, namely public (low level) actions L and private (high level) actions H. It is assumed that L [ H = A. SNNI property assumes an intruder who tries to learn whether a private action was performed by a given process while (s)he can observe only public ones. If this cannot be done then the process has SNNI property. Namely, process P has SNNI property (we will write P 2 SN N I) if P nH behaves like P for which all high level actions are hidden (namely, replaced by action ) for an observer. To express this hiding we introduce the hiding operator P=M; M A, for which it holds that 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 . Formally, we say that P has SNNI property, and we write P 2 SN N I i P n H 'w P=H. A generalization of this concept is given by opacity (this concept was exploited in [BKR04], [BKMR06] and [Gru07] in a framework of Petri Nets, transition systems and process algebras, respectively). Actions are not divided into public and private ones at the system description level but a more general concept of observations and predicates are exploited. 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 the both traces are indistinguishable for an observer (which is expressed by an observation function). This means that the observer (intruder) cannot say whether a trace for which the predicate holds has been performed or not. Now let us assume a di erent scenario, namely that an intruder is not interested in traces and their properties but he or she tries to discover whether a given process always reaches 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 time length less then n time unites, capability to perform at the same time actions form a given set, incapacity to idle (to perform t 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 de nition follows.
De nition 4. We say that the predicate over processes is consistent with respect to relation = if whenever P = P 0 then (P ) , (P 0).
As the consistency relation = we could take bisimulation ( ;), weak bisimulation ( f g) or any other suitable equivalence. A special class of such predicates are such ones (denoted as Q=) which are de ned by a given process Q and equivalence relation = i.e. Q=(P ) holds i P = Q.
We suppose that the intruder can observe only some activities performed by the process. Hence we suppose that there is a set of public actions which can be observed and a set of hidden (not necessarily private) actions. To model such s observations we exploit the relation )M where actions from M are those ones which could not be seen by the observer. The formal de nition of process opacity (see [Gru15]) is the following.
De nition 5 (Process Opacity). Given process P , a predicate over processes is process opaque w.r.t. the set M if whenever P )sM P 0 for s 2 (Actt n M ) and (P 0) holds then there exists P 00 such that P )sM P 00 and : (P 00) holds. The set of processes for which the predicate is process opaque w.r.t. to the M will be denoted by P OpM .
Note that if P = P 0 then P 2 P OpM , P 0 2 P OpM whenever is consistent with respect to = and = is such that it is a subset of the trace equivalence (de ned as 'w but instead of )sf g we use )s;).
P P
s =)M
(P 0) s =)M : (P 00) In this section we will concentrate on enforcing process opacity, namely, how to guarantee that there is no leakage of information on validity of in a current state, i.e. security with respect to process opacity. Let M Actt by M we will denote the complement of M i.e. M = Actt n M . Let s 2 Actt , by sM we denote the string obtained form s by removing all elements belonging to M . Formally, M = , s:xM = s:x i x 62 M and s:xM = s i x 2 M . We can extend this de nition to a set of strings. Let T Actt then TM = fsM js 2 T g.
Now let as suppose that process P is not secure with respect to process opacity P OpM i.e. P 62 P OpM . That means that there exists s 2 L(P )M such that P )sM P 0 and (P 0) holds then there does not exist P 00 such that P )sM P 00 and : (P 00) holds. Hence, by observing s, an intruder knows that a state satisfying has been reached. For security reasons we want to prohibit such computations what will be the role for the supervisory control. Formally, let K; K L(P )M is a set of safe observations, i.e. for every s 2 K, P )sM P 0 and s (P 0) does not hold or if it holds then there exists P 00 such that P )M P 00 and : (P 00) holds. Clearly, if P 2 P OpM then K = L(P )M , otherwise K L(P )M but K 6= L(P )M . The aim of the control is to design a supervisor Sup which will restrict behaviour of the original process P in such a way that for the resulting process Sup=P we have L(Sup=P ) K. Note that we do not assume any relations among set of actions visible for an intruder, a set of actions visible for a controller and a set of controllable actions, i.e. sets EI (EI = M ); ES ; EC , respectively, similarly to [TLSG18]. Note that in [DDM10] it is assumed that EI ES (or ES EI ) and EC ES . In [YL10] EI ES is assumed and in [TLSG16] EC ES is assumed.
Example 1. Let P = c:(a:b:N il+b:(a:N il+d:N il)), M = fc; dg and predicate is de ned as follows: (Q) holds i Q !d. Then it is easy to check that P 62 P OpM . The execution of c:b (visible as b) at the beginning leads to the state satisfying but no execution visible as b can lead to a state not satisfying .
Now we will model supervisory control by means a special process Sup. Process Sup runs in parallel with P , communicates with environment via actions Sort(P ) and internally with P by actions renamed by function f which maps every action a from Sort(P ) to a new "ghost" action a0 (see Fig. 2). The formal de nition of process supervisor is the following.
f
P
Sup
P De nition 6 (Process Supervisor). Given process P , a process Sup is called supervisor if Lw(Sup=P ) Lw(P ) where Sup=P = (P [f ]jSup) n f (Sort(P )) where f : Sort(P ) ! Sort(P )0 where Sort(P )0 = fx0jx 2 Sort(P ); x 6= g.
We will use a process supervisor to restrict behaviour of the original process in such a way that the resulting process becomes secure with respect to process opacity.
De nition 7 (Process Supervisor for Process Opacity). Given process P , process Sup is called supervisor for opacity property P OpM i P 62 P OpM but Sup=P 2 P OpM . By Sup(P; P OpM ) we will denote the set of all supervisors for opacity property P OpM for a given process P .
Example 2. Let us continue with the Example 1. Let Sup1 = c0:c:N il Sup2 = c0:c:a0:aN il and Sup3 = c0:c:a0:a:b0:b:N il then it is easy to check that all processes Supi are process supervisors for P and opacity property P OpM . Actually these process supervisors restrict the execution of action b immediately after c.
Clearly, Sup(P; P OpM ) 6= ; since N il 2 Sup(P; P OpM ). Note that supervisor N il restricts all behaviour of P which consequently becomes trivially secure. We can formulate some properties of the set Sup(P; P OpM ).
Proposition 2. Let Sup1; Sup2 2 Sup(P; P OpM ).
Proof. The main idea. The rst actions which is performed by (Sup1 + Sup2)=P is performed either by Sup1 or by Sup2.
Sup(P; P OpM ). ; Sup2. Then Sup2 2 Proof. Sketch. The proof follows from the the fact that trace equivalence is congruence i.e. for Sup1 ; Sup2 we have (P [f ]jSup1)nf (Sort(P )) ; (P [f ]jSup1)n f (Sort(P )) and so L((P [f ]jSup1) n f (Sort(P ))) = L((P [f ]jSup2) n f (Sort(P ))) i.e.L(Sup1=P ) = L(Sup2=P ).
To guarantee a minimal restriction of process behaviour our aim is to nd a maximal process supervisor in a sense that it minimally restricts behavior of the original process. The formal de nition is the following.
De nition 8 (Maximal Process Supervisor for Process Opacity). Process Sup 2 Sup(P; P OpM ) is called maximal process supervisor for process opacity P OpM i for every Sup0 2 Sup(P; P OpM ) L(Sup0=P ) L(Sup=P ). Example 3. Let us continue with the Examples 1 and 2. It is easy to check that process Sup3 is a maximal process supervisor for P and opacity property P OpM . Processes Sup1 and Sup2 are not maximal process supervisors for P and opacity property P OpM .
Unfortunately it is undecidable to verify whether a process Sup is a process supervisors for P and opacity property P OpM as it is stated by the following proposition.
Proposition 4. The property that Sup is a process supervisor for process opacity for process P is undecidable in general.
Proof. The proof is based on an idea that already process opacity is undecidable (see Proposition 2. in [Gru15]). Suppose that the property is decidable. Let Sup = X: Px2Actt x0:x:X i.e Sup does not restrict anything. We have that Sup is a process supervisor for process opacity for process P i P 2 P OpM . Hence we would be able to decide process opacity what contradicts its undecidability. Corollary. The property that Sup is a maximal process supervisor for process opacity for process P is undecidable in general.
To obtain a decidable variant of the previous property we put some restriction on process predicates. First we model predicates by special processes called tests. For now we assume that action is not visible for an intruder, i.e. 2 M . The tests communicate with processes and produce p action if corresponding predicates hold for the processes. In the subsequent proposition we show how to exploit this idea to express process opacity by means of appropriate M-bisimulation.
De nition 9. We say that the process T is the test representing predicate if (P ) holds i (P jT ) n At t p:N il where p is a new action indicating a passing of the test. If T is the nite state process we say that is the nitely de nable predicate.
Suppose that both and : are the nitely de nable predicates. Then we can reduce checking whether Sup is a process supervisor for process opacity to checking bisimulation (see Proposition 4. in [Gru15]). Since we can reduce the problem of decidability to nite automata (see [TLSG18]) we obtain the following result.
Proposition 5. Let and : are nitely de nable predicates. The property that Sup is a process supervisor for process opacity for nite state process P is decidable. Moreover, we can always nd a maximal supervisor for process opacity. 6
Time attacks belong to powerful tools for attackers who can observe or interfere with systems in real time. By the presented formalism we can distinguish timing attacks. Suppose that P 62 P OpM but P 2 P OpM[ftg. This means that an attack is possible only for an observer who can see elapsing of time, i.e. there is a possibility of timing attacks. To prevent them, we can use process supervisor which restricts process behaviour with respect to actions from A or we introduce a new type of process supervisor, called enhanced process supervisor which can add some idling between actions to ensure that the resulting process becomes secure with respect to timing attacks. In this case the restriction with respect to atomic actions from A could be smaller as in the case of original supervisory control.
De nition 10 (Enhanced Process Supervisor). Given process P , a process s ESup is called enhanced supervisor if whenever s 2 Lw(P ) then ESup=P )t; where ESup=P = (P [f ]jESup) n f (Sort(P )) where f : Sort(P ) ! Sort(P )0 where Sort(P )0 = fx0jx 2 Sort(P ); x 6= g.
De nition 11 (Enhanced Process Supervisor for Process Opacity). Given process P , P 2 P OpM[ftg, a process ESup is called enhanced supervisor for opacity property P OpM i P 62 P OpM ; but ESup=P 2 P OpM . By ESup(P; P OpM ) we will denote the set of all supervisors for opacity property EP OpM for a given process P .
Now we can formulate a condition which guarantees existence of an enhanced supervisory control.
Proposition 6. Let P 62 P OpM and there exists P 0, P ;t P 0 such that P 0 2 P OpM . Then there exists nontrivial (not equivalent to N il with respect to ) enhanced supervisory control for P .
Proof. The main idea. According to the assumption processes P and P 0 behave essentially in the same way but the later performs more idling between actions from Act. The enhanced supervisory control adds this idling to behaviour of P in such a way that the resulting process is process opaque.
Moreover, the previous proposition has the following consequence which guaranties that the maximal enhanced supervisory control does not restrict action from A.
Corollary. Let P 2 P OpM[ftg and P 62 P OpM . For the maximal enhanced supervisory control for P we have L(ESup=P )A = KA. 7
We have presented the new concepts called supervisory and enhanced supervisory controller for process algebra which enforce the security property called process opacity. Particularly, we have investigated nite state systems and time sensitive observations. A supervisor can see (some) system's actions and can control (disable or enable) some set of system's action. In this way it restricts system's behaviour to guarantee its security. Sometimes either we simply cannot redesign original insecure system which could have, for example, hardware implementation or some small restriction of system's behaviour is not essential for overall system functionality. In the case of enhanced supervisory controller it can only add some idling between actions which would have no in uence on system non-timing properties. The presented approach allows us to exploit also process algebras enriched by operators expressing other "parameters" (space, distribution, networking architecture, processor or power consumption and so on). In this way also other types of attacks, which exploit information ow through various covert channels, can be described and enforced. Hence we could obtain security properties which have not only theoretical but also practical value, since many protocols, particularly low level protocols for IoT, could be described by means of some process algebra formalism.