Testing of security for multi-agent systems is proposed and studied. We assume an attacker, as an agent, who can accumulate and exploit knowledge about other agents. This will be done by observation function and security property called process opacity. Unfortunately, this property is undecidable in general, so we propose its more realistic variant based on tests and testing. Here we consider systems to be secure if they cannot be compromised by a given test or set of tests. In the end, we state a decidability result for security testing.
Formal methods play an important role to guarantee software quality. On the other side their application is frequently either rather expensive or practically impossible due to complexity issues. On top of these there are properties which cannot be formally veri ed in general due to their undecidability. In such cases, tests and testing o er a more realistic approach.
In this paper, we address security properties of systems, particularly multiagent (MAS). We consider an attacker, as one of agents, who can accumulate some knowledge on the behaviour of other agents. We propose corresponding security properties and means how to test these properties. In a sense, we combine formal veri cation with testing. The presented approach combines several ideas emerged from the security theory. We exploit an idea (of an absence) of information ow between public and private system's behaviour (see [GM82]). This concept has been exploited many times in various formalisms. For example, the security property called Bisimulation Strong Nondeterministic Non-Interference requires that it cannot be distinguished (by means of bisimulation) between forbidding and hiding of private actions. In [Gru13] we have exploited this idea, but we weaken it by requiring that forbidding and the hiding of the private actions cannot be distinguished by a given test, i.e. we exploit a kind of testing equivalence (see also [NH84,SL95]). ? Work supported by the grant VEGA 1/0778/18. Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Here we start with security concept called opacity. To explain the opacity principle, let's suppose that we have some property over sequences of actions. Such property 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. We would like to know whether an observer can deduce the validity of the property just by partially observing (not all actions are visible) sequences of actions (traces) performed by the given process. The observer cannot deduce the validity of if there are two traces w; w0 such that (w) ^ : (w0) holds and the traces cannot be distinguished by the observer. In [Gru15] opacity is modi ed (the result is called process opacity) in such a way that instead of a process' traces we focus on properties of reachable states and attackers which can see only some process's actions. Hence we assume an intruder who is not primarily interested in whether some sequence of actions performed by a given process has some given property but we consider an intruder who wants to discover whether this process reaches a state which satis ed some given (classi ed) predicate. It turned out that in this way we could capture many new security aws. On the other hand some security aws, particularly important for multi-agent systems, are not covered by this state-based security property neither by its variant called an initial state opacity or in nite studied in [Gru17,GR19b].
In this paper we extend process opacity to re ect attackers which can accumulate some knowledge about other system's behaviour. This approach is particularly appealing for multi-agent systems where one of the agents could be an attacker. Qualitative security properties are often criticized for being either too restrictive or too benevolent. For example, a standard access control process should be considered insecure even if there always exists some (even very small) information ow which could help an attacker who tries to learn a password. By every attempt an attacker can learn, at least, what is not the correct one. There are several ways to overcome these disadvantages i.e. either quantify information ow or put some restrictions on attacker's capabilities. An amount of leaked information could be expressed by means of the Shannon's information theory as it was done, for example, in [CHM07,CMS09] for simple imperative languages. In this way we can obtain quanti cation of information ow either as a number of bits of private information which could leak or as a probability that an intruder can learn some secrete property. Here we exploit a di erent approach. We de ne tests and testing of security properties. Hence instead of requiring general security we require security with respect to a given set of tests. Each test represents a possible scenario of an attacker as well his or her capabilities. For example, an access control system with strong password policy should be considered reasonable secure with respect to a "small" attackers (tests), which can try only a few passwords. Moreover, testing allow us, besides other advantages, to express security of a system with respect to size of the test which could jeopardize its security. Hence the resulting level of security gives us relevant information on real (practical) system's security.
In this paper we also exploit an idea of observation function which express a capability of an attacker to accumulate some knowledge over MAS behaviour. Attacker's observations may not be just simple ones, say that some actions are visible for her and others are not (see [GR19a]). Visibility of a particular action could depend on previous actions as well. Hence the presented testing approach is strictly stronger then that of [Gru11], which is based on simple process's observations.
Contribution of the work can be summarized as follows: 1. de nition of security with respect to a given test, 2. modeling observations by processes, 3. modeling predicates by processes, 4. reducing security checking to process's traces checking, 5. decidability results, for practically the most interesting, nite states processes.
The paper is organized as follows. Our working formalism is introduced in Section 2. In Section 3 we describe information ow security properties of interest. In Sections 4 we de ne tests and testing and in Section 5 we relate testing and security. 2
As an working formalism we will use Milner's CCS (see [Mil89]). Let A be a se of atomic action symbols not containing symbols and such that for every a 2 A there exists a 2 A and a = a. We de ne Act = A [ f g. We assume that a; b; u; v : : : range over A, x; y; : : : range over Act, For s = x1:x2: : : : :xn; xi 2 Act 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 Act 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 x P 0 for M Act i P !s1 !x !s2 P 0 for s1; s2 2 M ? and P )M instead of P ))x1MM )x2 M : : : )xnM . We will s x x x write P )M )ifMthPer0eifexxis2tsMP.0 Nsuocthe tthhaatt )PxM)Mis dPe0.nWede fowrilalrwbirtirtearPy a)cbtMionPx0 instead of P 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. By sjB we will denote the sequence obtained from s by removing all actions not belonging to B.
We de ne two equivalences which are modi cations of trace equivalence and weak bisimulation, respectively (see [Mil89]).
s A is de ned as T rwM (P ) = fs 2 A?j9P 0:P )M P 0g. Instead of T rw;(P ) we will write T rw(P ).
Q) i T rwM (P ) = T rwM (Q). We will write w instead of w;.
De nition 2. Let (Act; Act; !) be a labelled transition system (LTS). A relation < Act Act 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 Act then there exists a process Q0 such that Q )bx M Q0 and (P 0; Q0) 2 <. Two processes P; Q are Mbisimilar, abbreviated P M Q, if there exists a M-bisimulation relating P and Q. 3
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. Firstly we de ne observation function on sequences from Act?.
Any function O : Act? ! ? 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 : Act ! [ f g such that for every w 2 Act? it holds O(w) = O0(x1) : : : O0(xn), { dynamic if there is a mapping O0 : Act? ! [ f g such that for every w 2 Act? it holds O(w) = O0(x1):O0(x1:x2) : : : O0(x1 : : : xn), { orwellian if there is a mapping O0 : Act Act? ! [ f g such that for every w 2 Act? it holds O(w) = O0(x1; w):O0(x2; w) : : : O0(xn; w), { m-orwellian if there is a mapping O0 : Act Act? ! [ f g such that for every w 2 Act? 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. Note that the same action can be seen di erently 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.
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 Act? performed by given process. The observer cannot deduce the validity of if there are two traces w; w0 2 Act? 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.
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.
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. 4
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 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 de nition follows.
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.
.
cesses is process opaque w.r.t. the observation function O whenever P !w P 0 for w 2 Act and (P 0) holds then there exists P 00 such that P !w0 P 00 for some w0 2 Act and : (P 00) holds and moreover O(w) = O(w0). The set of processes for which the predicate is process opaque w.r.t. to the O will be denoted by P OpO.
Schematically, Fig. 1 depicts process opacity. In [Gru15]) process opacity is de ned for static observational function, namely a set of public actions which can be observed and a set of hidden (not necessarily private) actions are assumed. To model such observations we exploit the relation )sM where actions from M are those ones which could not be seen by the observer.
w.r.t. the set M if whenever P )sM P 0 for s 2 (Act n M ) and (P 0) holds then s there exists P 00 such that P )M 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 .
Schematically, Fig. 2 depicts process opacity e w.r.t. the set M . 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;).
The process opacity is de ned for arbitrary predicates and observation functions. Now we will reformulate it for those ones which can be expressed by process algebras. Firstly we start with observation function O . Suppose that Act \ = ;. We extend the set of actions A by and we model O by a special process.
De nition 8. Process O is called process de nition of observation function O if for every P and s 2 Act it holds P !s P 0 i (P jO) n A )o (P 0jO0) n A for o 2 such that O(s) = o. i x 2 M and O(x) = x
Some observation function cannot be computed at all (we can prove this by de ning a function which returns a speci c symbol if a given Turing machine halts). But some observation functions can be emulated by nite state processes as it is stated by the following lemma.
Lemma 2. For any static or m-orwellian observation functions O there exists nite state process O which is process de nition of observation function O. Proof. Sketch. Any static or m-orwellian observation function can be simulated by nite-state transducer which can be simulated by nite state process.
Note that also some dynamic and orwellian observation function can be dened by nite state systems in a case that their computation does not need an unlimited memory.
Now we can relate observation functions de ned by processes with the de nition of process opacity.
Lemma 3. Let for every o 2 such that (P jO) n A )o (P 0jO0) n A and (P 0) holds there exists P 00 such that (P jO) n A )o (P 00jO0) n A such that : (P 00) holds. Then P 2 P OpO and vice versa.
Proof. Directly from De nitions 6 and 8.
An observation function de nes what an attacker can see from process behaviour. One attacker could see more that another attacker. There are several ways how to express this situation. In the following de nition we suppose that the set of observables for one attacker is a subset of observables of another attacker. This gives an ordering between observation functions.
De nition 9. Let O1; O2 are two observation functions with the common set of observables . We de ne ordering between them (denoted by ) as follows. O1 O2 i for every w; w 2 Act we have O1(w)jU = O2(w) for some set U; U .
Lemma 4. Let O1; O2 are two observation functions such that O1 O2. Then for every w; w 2 Act it holds that O1(w) = O1(w0) implies O2(w) = O2(w0). Proof. Let O1(w) = O1(w0). Then also O1(w)jU = O1(w0)jU for arbitrary U . Since O1 O2 we have O1(w)jU = O2(w) and O1(w0)jU = O2(w0) i.e. O2(w) = O2(w0).
The ordering between observation functions corresponds to stronger and weaker process opacity properties as it is stated by the following lemma. Lemma 5. Let O1; O2 are two observation functions such that O1 P OpO1 P OpO2 .
O2. Then Proof. Main idea. Let P 2 P OpO1 Then from De nitions 6 we know that whenever P !w P 0 for w 2 Act and (P 0) holds then there exists P 00 such that P !w0 P 00 for some w0 2 Act and : (P 00) holds and moreover O1(w) = O1(w0). But since O1 O2 we have by the previous lemma also O2(w) = O2(w0) and hence P 2 P OpO2 .
The ordering on observation functions could be related to the relations )M as it is stated by the following Lemma.
Lemma 6. Let O1; O2 are process de nitions of observation functions O1; O2, respectively and O1 O2. Then for every P and o 2 it holds (P jO1) n A )o (P 0jO10) n A i (P jO2) n A )oU (P 0jO20) n A for some U; U .
Proof. Sketch. Since O1 O2 from De nition 9 we have O1(w)jU = O2(w) for some set U; U . And from De nition 8 we have translation of this fact of this to traces.
Note that there also other possibilities how to order intruders with respect to their capabilities to observe processes behaviour expressed by observation function. For example, observation of one attacker can be included in observations of another one, one attacker cannot see completely something which can be seen by another one etc. We leave investigations of such orderings to future work. 5
Process opacity is undecidable property, since its special variant (see De nition 7) is undecidable (see [Gru15]). Undecidability results from many factors, one of them is too general notion of observer's capabilities. Now we use a concept of testing, which will help us to de ne security with respect to given test or set of tests.
A test examines process's capability to perform some set of actions. It is required that every sequence of test's actions should be emulated also by tested process i.e. for a test T and tested process P it should hold T rw(PT ) T rw(P ) where PT is behavior of P under the test T . But since we will later incorporate also visibility of such traces as well as properties of resulting processes we need a more elaborated de nition of testing. We suppose that a test communicates with tested process by means of new alternative actions, which are original ones just indexed by a (i.e. alternative actions to x; y; z are depicted as xa; ya; ya). The formal de nition follows.
De nition 10. Process T is called a test for process P i T rw((T jP [f ]) n Aa)
In the following example we present a test which examines all process traces. Example 1. Let T = X: Px2A(x:xa:X +x:xa:X). Then we have T rw((T jP [f ])n Aa) = T rw(P ) for every P and hence T will be called a simple complete test.
Now we are prepared for combining testing with observation functions. It reduces general process opacity to property which requires that for an observer/tester, expressed by T , tested process P is secure.
O and T is the test of process P . We say that P pass test T under O and (denoted by P 2 P OpO(T )) i if for every o 2 it holds ((T jP [f ]) AajO)nA )o ((T 0jP 0[f ]) AajO0)nA and (P 0) holds there exists P 00 such that ((T jP [f ]) AajO)n A )o ((T 0jP 00[f ]) AajO0) n A such that : (P 00) holds.
Testing by test T and observation function de ned by process O is depicted by Fig. 3. Actions of process P are rstly tested by T and its sequence of actions and then the same sequence is taken as an input for O to produce its visible part, i.e. as a sequence of observables from .
O
T
P
If a process P is process opaque with respect to and O then it should be process opaque with respect to any test T as its is stated by the following Lemma.
Lemma 7. Let process O is process de nition of observation function O, test T of process P and P 2 P OpO. Then P pass test T under O.
Proof. Directly from De nitions 6 and 11.
Now we can show how a natural ordering between tests de nes ordering on security of processes with respect to process opacity.
Then if P 2 P OpO(T2) then P 2 P OpO(T1).
T r(T2).
Proof. Sketch. Let P 2 P OpO(T2) i.e. it has to pass test T2 which represents, basically a set of traces. Since test T1 produces less traces it has to pass also this test and hence P 2 P OpO(T1).
As a direct consequence of the previous Lemma we have the following one. Lemma 9. Let T1; T2 are two tests for process P . Then if P 2 P OpO(T1 + T2) then P 2 P OpO(T1) and P 2 P OpO(T2).
Proof. The proof follows from the previous Lemma and facts that T r(T1) T r(T1 + T2) and T r(T2) T r(T1 + T2).
A property similar to the one expressed by Lemma 8 holds for predicates i.e. security with respect to weaker predicate implies security with respect to stronger one.
Lemma 10. Let 1; 2 are two predicates such that 1 ) process P . Then if P 2 P Op 2 (T ) then P 2 P Op 1 (T ).
O O
Proof. Let P 2 P OpO2 (T ) and let P !w P 0 for w 2 Act and 1(P 0) holds. SPi0n0 cseuch1 t)hat 2P t!hwe0nPa00lsfoor s2o(Pm0e) who0l2ds Aacntd sainndce:P 2(2P P00)OhpoOl2d(sTa)ntdhemreoreexoivsetsr O(w) = O(w0). Again since : 2 ) : 1 then also : 1(P 00) holds and hence P 2 P Op 1 (T ).
O
Now we show how checking of process opacity could be reduced to checking of standard process algebra properties. Firstly we de ne also a predicate over processes by a special process.
p P such that (P ) holds i (P jP ) n A ) where p is a new action p 62 A.
Example 2. Let (Q) holds of Q can once perform action a then later action b. Process P de ned as P = X: Px6=a x:X + a:P 0, where P 0 = X: Px6=b x:X + b:p:N il is process de nition of .
Now we can reduce process opacity checking to checking of trace inclusion as it is stated by the following theorem.
Theorem 1. Let O; P ; P: are process de nitions of observation functions O tahnadt pifreod:ipca2tesT r w;:(P ,jOrejPspe)cntivAeltyh.eTnhoe:npP2 2T rPwO(Pp OjOijP:for) nevAe.ry o 2 it holds Proof. The proof follows from De nitions 6, 8 and 12.
Now, thank to the above mention reduction, we can obtain decidable variant for process opacity.
Theorem 2. Let O; T; P ; P: are nite state process de nitions of observation functions O, test and predicates ; : , respectively. Then process opacity is decidable for any nite state test.
Proof. Sketch. The proof follows from De nitions 6, 8 and 12 and Theorem 1.
The security property process opacity expects an attacker who can just observe process' traces but cannot interact with the process. In many cases this does not cover real attacks and attackers, particularly in the case of multi-agent systems where a possible attacker could be one of the agents. Hence we generalize process opacity in such a way that also every successor of a process has to be process opaque as well. The formal de nition follows.
De nition 13 (Persistent Process Opacity). We say that process P is persistently process opaque w.r.t. the observation function O and if Succ(P ) P P OpO.
Proposition 1. P P Op and O such that P P Op
O O
P OpO for every P OpO.
and O. Moreover, there exist Proof. The main idea. Let P 2 P P OpO. Then directly from De nition 13 we have that P 2 P OpO. To show that the inclusion is proper let us assume the following example. Let P = a:b:b:N il + a:c:c:N il, an observation function O such that O(a) = a; O(b) = O(c) = and predicate such that (Q) hold i Q can perform a or b. Then P 2 P OpO but P 62 P P OpO since b:b:N il 62 P OpO.
For persistent process opacity similar properties as for process opacity but some modi cations are needed. For example, in Lemma 8 we have to replace trace inclusion by simulation, what is an asymmetric variant of bisimulation. 6
We have presented the security concept called process opacity and its stronger variant persistent process opacity. We show how to model observation functions, which express capability to observe a system as well as capabilities to accumulate some knowledge on its behaviour as well as security predicates by processes. We have proposed a way how to (partially) verify these properties by means of tests and testings. Each test represents a scenario for an attacker as well his or her capabilities. Instead of verifying process opacity we de ne system security with respect to a given set of tests. We have shown, that under some restriction, this testing is feasible or at least decidable.
As future work, we plan to de ne and study a minimal set of tests which are necessary to be passed to guarantee some security property. In this way we would simplify overall testing. Moreover we plan to work with di erent ordering on observation functions as well as tests.
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). Hence we could obtain security properties which have even higher practical value.