In distributed systems, it is often important that a user is not able to infer if a given action has been performed by another component, while still being able to interact with that component. This kind of problems has been studied with the help of a notion of “interference” in formal models of concurrent systems (e.g. CCS, Petri nets). Here, we propose several new notions of interference for ordinary Petri nets, study some of their properties, and compare them with notions already proposed in the literature. Our new notions rely on the unfolding of Petri nets, and on an adaptation of the “reveals” relation for ordinary Petri nets, previously defined on occurrence nets, and on a new relation, called “excludes”, here introduced for detecting negative information flow.
In distributed systems, information flows among components. The flow can be used to rule the behavior of the system, to guarantee the correct synchronization of tasks, to implement a communication protocol, and so on.
In some cases, a flow of information from one component to another is actually a leakage: that piece of information should not have passed from here to there. Such unwanted flows can endanger the working of the system.
In this paper, we study formal notions of unwanted information flow, based on a general notion of non-interference, within the theory of Petri nets, and compare our approach with existing approaches.
Non-interference was first defined for deterministic programs [
Broadly speaking, these approaches assume that the actions performed in a system belong to two types, conventionally called high (hidden) and low (observable). A system is then said to be free from interference if a user, by interacting only via low actions, cannot deduce information about which high actions have been performed.
This approach was formalized in terms of 1-safe Petri nets in [
We propose new notions of non-interference for ordinary Petri nets. They deal
with positive information flow as well as negative information flow, regarding
both past and future occurrences and are based on unfoldings and on reveals
and excludes relations which are formally defined in Section 3. Reveals was
originally defined as a relation between events of an occurrence net in [
The first notion of non-interference we introduce is called Reveals based NonInterference (RNI) and it states that a net is secure if no low transition reveals any high transition. This new notion is introduced in Section 4.1. We also propose more restrictive notions called k-Extended-Reveals based Non-Interference (k-ERNI) and n-Repeated-Reveals based Non-Interference (n-ReRNI), they are based on observation of multiple occurrences of low transitions. These two parametric non-interference notions are introduced and discussed in Section 4.2 and Section 4.3. In Section 4.4, Positive/Negative Non-Interference (PNNI) is introduced on the basis of both the reveals and excludes relations between low and high transitions capturing both positive and negative information flow. The new notions are discussed and compared with each other while they are introduced. In Section 5, we compare, on the basis of examples, the new introduced notions with the ones already introduced in the literature and mentioned at the beginning of Section 4. Finally, Section 6 concludes the paper and discusses some possible developments. 2
In this section we collect preliminary definitions and set the notation which will be used in the rest of the paper.
Let R ⊆ I × I be a binary relation, the transitive closure of R is denoted by R+; the reflexive and transitive closure of R is denoted by R∗.
A net is a triple N = (B, E, F ), where B and E are disjoint sets, and F ⊆ (B × E) ∪ (E × B) is called the flow relation. The pre-set of an element x ∈ B ∪ E is the set •x = {y ∈ B ∪ E | (y, x) ∈ F }. The post-set of x is the set x• = {y ∈ B ∪ E | (x, y) ∈ F }.
An (ordinary) Petri net N = (P, T, F, m0) is defined by a net (P, T, F ), and an initial marking m0 : P → N. The elements of P are called places, the elements of T are called transitions. A net is finite if the sets of places and of transitions are finite.
A marking is a map m : P → N. A marking m is safe if m(p) ∈ {0, 1} for all p ∈ P . Markings represent global states of a net.
A transition t is enabled at a marking m if, for each p ∈ •t, m(p) > 0. We write m[ti when t is enabled at m. A transition enabled at a marking can fire, producing a new marking. Let t be enabled at m; then, the firing of t in m produces the new marking m0, defined as follows: m0(p) = m(p) − 1 for all p ∈ •t \ t•
m(p) + 1 for all p ∈ t• \ •t m(p) in all other cases We will write m[tim0 to mean that t is enabled at m, and that firing t in m produces m0.
A marking q is reachable from a marking m if there exist transitions t1 . . . tk+1 and intermediate markings m1 . . . mk such that
m[t1im1[t2im2 . . . mk[tk+1iq The set of markings reachable from m will be denoted by [mi. If all the markings reachable from m0 are safe, then N = (P, T, F, m0) is said to be 1-safe (or, shortly, safe).
Let N = (B, E, F ) be a net, and x, y ∈ B ∪ E. If there exist e1, e2 ∈ E, such that e1 6= e2, e1F ∗x, e2F ∗y, and there is b ∈ •e1 ∩ •e2, then we write x#y.
A net N = (B, E, F ) is an occurrence net if the following restrictions hold: 1. ∀x ∈ B ∪ E : ¬(xF +x) 2. ∀x ∈ B ∪ E : ¬(x#x) 3. ∀e ∈ E : {x ∈ B ∪ E | xF ∗e} is finite 4. ∀b ∈ B : |•b| ≤ 1 The set of minimal elements of an occurrence net N with respect to F ∗ will be denoted by ◦N . The elements of B are called conditions and the elements of E are called events. If x#y in an occurrence net, then we say that x and y are in conflict. Let e ∈ E be an event in an occurrence net; then the past of e is the set of events preceding e in the partial order given by F ∗: ↑ e = {t ∈ E | tF ∗e}. An occurrence net represents the alternative histories of a process; therefore its underlying graph is acyclic, and paths branching from a condition, corresponding to a choice between alternative behaviors, never converge.
A run of an occurrence net N = (B, E, F ) is a set R of events which is closed with respect to the past, and free of conflicts: (1) for each e ∈ R, ↑ e ⊆ R; (2) for each e1, e2 ∈ R, ¬(e1#e2). A run is maximal if it is maximal with respect to set inclusion.
Let Ni = (Pi, Ti, Fi) be a net for i = 1, 2. A map π : P1 ∪ T1 → P2 ∪ T2 is a morphism from N1 to N2 if: 1. π(P1) ⊆ P2; π(T1) ⊆ T2 2. ∀t ∈ T1 the restriction of π to •t is a bijection from •t to •π(t) 3. ∀t ∈ T1 the restriction of π to t• is a bijection from t• to π(t)• In the rest of the paper, we will consider finite Petri nets, i.e., Petri nets whose underlying net is finite, except for occurrence nets. Of course, Petri nets may have infinite behavior. Moreover, we assume that all transitions of a Petri net have non-empty preset, i.e., all have input places.
A branching process of a Petri net N = (P, T, F, m0) is a pair (O, π), where O = (B, E, G) is an occurrence net, and π is a morphism from O to N such that: 1. ∀p ∈ P m0(p) = |π−1(p) ∩ ◦O| 2. ∀x, y ∈ E, if •x = •y and π(x) = π(y), then x = y A branching process Π1 = (O1, π1) is a prefix of Π2 = (O2, π2) if there is an injective morphism f from O1 to O2 which is a bijection when restricted to ◦O1, and such that π1 = π2f .
Any finite Petri net N has a unique branching process which is maximal
with respect to the prefix relation. This maximal process, called the unfolding of
N , will be denoted by Unf(N ) = ((B, E, F ), λ), where λ is the morphism from
(B, E, F ) to N [
The following definition will be used in the rest of the paper to denote the set of events of an unfolding corresponding to a specific transition of a given Petri net.
Definition 1. Let N = (P, T, F, m0) be a Petri net, Unf(N ) = ((B, E, F ), λ) be its unfolding and t ∈ T , the set of events corresponding to t is denoted Et = {e ∈ E | λ(e) = t}.
The following definitions concern the reveals relation, originally introduced in [
Definition 2. Let O = (B, E, F ) be an occurrence net, Ω ⊆ 2E be the set of
its maximal runs, and e1, e2 be two of its events. Event e1 reveals e2, denoted
e1 e2, iff ∀σ ∈ Ω, e1 ∈ σ =⇒ e2 ∈ σ
Definition 3. [
In other words, a set of events, A, extended-reveals another set of events, B, written A _ B, iff every maximal run that contains A also hits B. The reveals relation can be expressed as extended-reveals relation between singletons: a b can be written as {a} _ {b}. Example 1. To give a simple example on the original reveals and extendedreveals notions, we examine the occurrence net in Fig. 2. In this net, e2 e4 and e4 e2. In general reveals relation is not symmetrical. As an example, e6 e4 but e4 6 e6 since after e4, e7 can occur instead of e6.
In the same occurrence net, the occurrence of e1 does not necessarily mean that e5 will occur, but e1 together with e2 extended-reveals e5, denoted as {e1, e2} _ {e5}. The occurrence of e4 reveals neither e6 nor e7. However, it reveals that either e6 or e7 will occur, denoted as {e4} _ {e6, e7}. 3
In this section, we first introduce a new relation between transitions, called
excludes, which will be used to detect negative information flow. Later, we define
a reveals and an extended-reveals relation on the set of transitions of a Petri net,
relying on the corresponding relations on occurrence nets as recalled in Section 2.
Moreover, we introduce a new parametric relation, called repeated-reveals, again
on the set of transitions of a Petri net. Reveals, extended-reveals and
repeatedreveals relations will be used to detect positive information flow, however they
can also be applied in other areas, e.g. fault diagnosis as explored in [
Definition 4. Let N = (P, T, F, m0) be a Petri net and Unf(N ) = ((B, E, F ), λ) be its unfolding, Ω be the set of all its maximal runs. Let t1, t2 ∈ T be two transitions, we say t1 excludes t2, denoted t1 ex t2, iff ∀ω ∈ Ω Et1 ∩ ω 6= ∅ =⇒ Et2 ∩ ω = ∅, i.e., they never appear in the same run.
It is easy to see that excludes is a symmetric relation and it is not transitive as well as obviously not reflexive.
In the case of Petri nets whose underlying net is an acyclic graph, if two transitions are in conflict, i.e., they are both enabled and the firing of one disables the other one, then one excludes the other. However, in general, transitions which are in conflict can still appear in the same maximal run and therefore they could be in not-excludes relation.
Example 2. The transitions t2 and t4 of N1 in Fig. 1 are in conflict whereas ¬(t2 ex t4). In the unfolding in the same figure, it is possible to see a maximal run including occurrences of both.
t5 ex t4 although they are not in conflict.
t7 ex t5, t5 ex t1 but ¬(t7 ex t1), indeed the relation is not transitive. Definition 5. Let N = (P, T, F, m0) be a Petri net, and Unf(N ) = ((B, E, F ),λ), be the unfolding of N . Let Ω be the set of all maximal runs of N . Let t1, t2 ∈ T be two transitions, we say that t1 reveals t2, denoted t1 tr t2, iff ∀ ω ∈ Ω Et1 ∩ω 6= ∅ =⇒ Et2 ∩ ω 6= ∅.
We say transition t1 reveals transition t2 if and only if each maximal run which contains an occurrence of t1 also contains at least one occurrence of t2. This means that for each observation of t1, t2 has been already observed or will be observed.
Remark 1. The reveals relation on transitions is reflexive and transitive, i.e., let N = (P, T, F, m0) be a Petri net, t1, t2, t3 ∈ T , then t1 tr t1, and (t1 tr t2 ∧ t2 tr t3) =⇒ t1 tr t3.
Example 3. In the net N1, in Fig. 1, t3 reveals both t2 and t1. It is easy to notice that to be able to fire t3 we must first fire t1 and t2. In fact, in the unfolding, Unf(N1), given in Fig. 1, for each occurrence of t3 there is at least one occurrence of t2 and similarly, for each occurrence of t3 there is at least one occurrence of t1. However, t1 does not reveal t2 or t3, since there is a run in which t1 occurs and neither t2 nor t3 occurs. If an observer, who knows the structure of N1, can only observe t1 he cannot have information about t2 or t3, however if he is able to observe t3, he can deduce that t2 and t1 must have occurred.
Transition t1 also reveals transition t6 because when t1 fires, t5 cannot fire anymore and, since the net progresses, t6 must fire. Since we do not assume strong fairness, t1 6 tr t4, after the occurrence of t1, t2 and t3 can loop forever. Reveals relation is not only about past occurrences but also about future occurrences. Observing t1 does not tell us when t6 fires. It might have fired already or it will fire in the future. t1 tr t6 tells us that when t1 occurs, an occurrence of t6 is inevitable.
Remark 2. Reveals relation is neither symmetric nor antisymmetric. For example, in Fig. 1, t2 tr t3 and t3 tr t2 , however t2 tr t1 and t1 6 trt2. In some cases, one transition alone does not give much information about the behavior of the net whereas a set of transitions together can give some information about the behavior of the net. This relation is defined as in the following. Definition 6. Let N = (P, T, F, m0) be a Petri net, Unf(N ) = ((B, E, F ), λ) be its unfolding and Ω be the set of all maximal runs. Let W, Z ⊆ T and W extended-reveals Z, denoted W _tr Z, iff ∀ ω ∈ Ω ^ (ω ∩ Et 6= ∅) =⇒ t∈W _ (ω ∩ Et 6= ∅) t∈Z
We say that a set of transitions W extended-reveals another set of transitions Z, if and only if each maximal run, which contains at least an occurrence of each transition in W , also contains at least an occurrence of a transition in Z.
The reveals relation on transitions, t1 tr t2, corresponds to the extendedreveals relation between singletons, {t1} _tr {t2}.
Example 4. In the net shown in Fig. 3, t2 alone does not reveal t5, whereas t2 and t3 together tell us that t5 will fire, denoted as {t2, t3} _tr {t5}. In the same net, the occurrence of t5 tells us that either t8 or t9 will fire, denoted as {t5} _tr {t8, t9}. Similarly, {t7, t8} _tr {t10}, i.e., there is no maximal run which includes occurrences of t7, t8 and not t10.
In some cases, repeated occurrences of the same transition can give more information about the behavior of a net than only one occurrence of that transition. A relation based on this fact is defined in the following.
Definition 7. Let N = (P, T, F, m0) be a Petri net, Unf(N ) = ((B, E, F ),λ) be its unfolding and R be the set of all runs. Let t1, t2 ∈ T be two transitions of N , and n be a positive integer. Let Rtni = {ω ∈ R : |ω ∩ Eti | = n} and Ωtni denotes the set of maximal runs in Rtni with respect to set inclusion (i.e., Ωtni ⊆ Rtni such that if u, v ∈ Ωtni ∧ u ⊆ v then u = v).
If Ωtn1 6= ∅ then t1 n-repeated reveals t2, denoted t1 Ren tr t2, iff ∀ω ∈ Ωtn1 Et2 ∩ ω 6= ∅.
If Ωtn1 = ∅ then t1 Ren tr t2 is not defined.
Notation. t1 Ren6 tr t2 will denote that there is at least one run in Ωtn1 such that t1 appears n times and t2 does not appear. ¬(t1 Ren tr t2) will denote that either t1 Ren tr t2 is not defined, or t1 Ren6 tr t2.
Example 5. Let us consider N3 in Fig. 3. Transition t11 does not reveal t12, however if the occurrence of t11 is observed twice then it is evident that t12 occurred, therefore t11 2-Repeated reveals t12, denoted t11 Re2 tr t12, whereas t11 Re16 tr t12 since after the first occurrence of t11, t14 can fire instead of t12.
Note that t11 Re3 tr t12 and t11 Re36 tr t12 are both not defined since t11 can fire at most twice, therefore in this case ¬(t11 Re3 tr t12).
Proposition 1. Let N = (P, T, F, m0) be a Petri net, Unf(N ) = ((B, E, F ),λ) its unfolding and R be the set of all runs. Let t1, t2 ∈ T be two transitions of N , iPnroRot1f1. . LIeftt1Rt1R1 e=1tr{ωt2∈, tRhe:n |Ωωt1∩1 E6=t1∅| =an1d}∀aωnd∈ΩΩt11t11 bωe ∩thEets2e t6=of∅maximal runs . Let σ be an arbitrary maximal run of Unf(N ). Suppose that σ ∩ Et1 6= ∅ then we can always take a run ω ∈ Ωt11 such that ω ⊆ σ. Then we know that σ contains at least one occurrence of t2 and so t1 tr t2. tu
However, the implication of the previous proposition does not hold in the other direction. In fact, consider the net in Fig. 4, t1 tr t2, t1 tr t3, t1 Re16 tr t2 and t1 Re16 tr t3. The main difference is that we consider only maximal runs for reveals relation. For this net there is only one maximal run which contains t1 (twice), t2 and t3. However, there is a run in Ωt11 in which t1 appears and t2 does not appear, as well as a run in which t1 appears and t3 does not appear. All runs in Ωt21 , i.e., including t1 twice, contain both t2 and t3, i.e., t1 Re2 tr t2 and t1 Re2 tr t3. σ ∩ Et2 6= ∅, so t1 Ren +tr1 t2. 4
Proposition 2. Let N = (P, T, F, m0) be a Petri net, Unf(N ) = ((B, E, F ),λ) be its unfolding and R be the set of all runs. Let t1, t2 ∈ T be two transitions, if t1 Ren tr t2 and Ωtn1+1 6= ∅ then t1 Ren +tr1 t2.
Proof. Let Rtn1 = {ω ∈ R : |ω ∩ Et1 | = n} and Ωtn1 be the set of maximal runs in Rtn1 . If t1 Ren tr t2, then Ωtn1 6= ∅ and ∀ω ∈ Ωtn1 ω ∩ Et2 6= ∅. Let σ ∈ Ωtn1+1, we can always choose a run ω ∈ Ωtn1 such that ω ⊆ σ. Then we know that tu In this section, before introducing the new notions, we briefly recall the most used non-interference notions in the literature and discuss our motivation for introducing new non-interference notions based on reveals and excludes relations.
The notions recalled in the following are based on some notion of low observability of a system. It is what can be observed of a system from the point of view of low users.
There are mainly two kinds of information flows that non-interference notions
deal with. These are positive information flow and negative information flow. A
positive information flow arises when the occurrence of a high level transition
can be deduced from the low level behavior of the system, whereas a negative
information flow is concerned with the non-occurrences of a high transition.
Fig. 5. Relation between some existing interference notions in the literature.
SNNI ≡NDC, BSNNI ⊆SNNI, SBNDC ≡ BNDC ≡ PBNI+ ⊆ BSNNI, PBNI ⊆PBNI+
(see [
In the following, we will use acronyms to denote the set of nets satisfying the corresponding security notion.
The less restrictive notion, introduced in [
While SNNI is based on trace equivalence, the more restrictive notions Bisimulation based Strong Nondeterministic Non-Interference (BSNNI) and Bisimulation based Non-Deducible on Composition (BNDC) are based on bisimulation.
Strong Bisimulation based Non-Deducible on Composition (SBNDC) is an
alternative characterization of BNDC [
Another non-interference notion called Place Based Non-Interference (PBNI)
was introduced in [
In [
The overall relationship between these mentioned notions is illustrated in Fig. 5. In the rest of the paper, we will refer only to the notions which are illustrated in the figure since the others are equivalent to those.
With respect to the above mentioned different kinds of information flow, SNNI, BSNNI and PBNI+ deal with positive information flow, whereas PBNI deals also with negative information flow.
All these notions seem to aim mainly at deducing past occurrences of high transitions, for example they all consider system N6 in Fig. 7 secure, whereas, by considering progress, after the occurrence of l, a low user deduces h is inevitable and therefore N6 is not secure with respect to the ability of deducing information about the future behavior.
Differently from the previous notions, the ones we are going to propose do not only capture information flow about past occurrences of high transitions, but also information flow about inevitable or impossible future occurrences of high transitions.
In some cases, the mere ability to deduce that some high transition has occurred is not a security threat, provided the low user cannot know which one occurred.
Let us illustrate this issue with the help of an example. The net in Fig. 6 represents a system in which a user can repeatedly submit a paper to a committee, each time receiving a judgment (accept or reject). The black squares represent high transitions. The review process can follow either of two paths, and we do not want the user to know which one was chosen. When the user receives an answer, he knows that some high transition occurred, however he cannot infer which one.
For this reason, the new notions we are going to introduce in the following will consider such a system secure, whereas it is not secure with respect to SNNI, and the other above recalled notions.
In the sequel, the set of high transitions will be denoted by H and the set of low transitions will be denoted by L. 4.1
Reveals-based Non-Interference accepts a net as secure if no low transition reveals any high transition.
Definition 8. Let N = (P, T, F, m0) be a Petri net, T = H ∪ L, H ∩ L = ∅, L, H 6= ∅. N is secure with respect to Reveals-based Non-Interference (RNI) iff ∀l ∈ L ∀h ∈ H: l 6 trh.
Example 6. N4 in Fig. 6 is RNI secure. N5 and N6 in Fig. 7 are not secure with respect to RNI, since in both nets a low transition reveals a high transition, i.e., l tr h. An observer who knows the structure of the net can deduce that h has already fired in N5 by observing l. For N6, again by observing l, he can deduce that h will fire. N7 in Fig. 7 is also not secure in this context because the observation of l1 tells the observer that h has already fired or will fire since l2 cannot fire anymore.
With RNI, we are able to capture positive information flow. Moreover, we not only capture past occurrences of high transitions but also future occurrences, and this is because of the progress assumption.
Although it is useful to capture positive information flow, RNI is not able to capture the negative information flow. N8 in Fig. 7 is considered to be secure with respect to RNI since it cannot capture the flow between h and l. However, an observer could deduce that h has not fired and will not fire in the future by observing the occurrence of l. In Section 4.4 we will introduce a notion which deals with this kind of information flow. 4.2
As explained in Section 3, in some cases, a transition does not tell much about the behavior of the net, whereas a set of transitions together gives some more information. Extended-reveals deals with this relation between transitions of a Petri net. We propose to use this relation in order to define a new non-interference notion in which the occurrences of a set of low transition together give information about some high transitions.
Definition 9. Let N = (P, T, F, m0) be a Petri net, T = H ∪ L, H ∩ L = ∅, L, H 6= ∅, |L| ≥ k ≥ 1. N is secure with respect to k-Extended-Reveals based Non-Interference (k-ERNI) iff ∀{l1, ..., lk} ⊆ L ∀h ∈ H, {l1, ..., lk} _6 tr{h}.
N is ERNI secure if it satisfies the above condition for k = |L|.
Intuitively, we say that a net is k-ERNI secure, if an attacker is not able to deduce information about the hidden part of the net by observing occurrences of k low level transitions. If a net is k-ERNI secure then it is secure with respect to all n-ERNI where 1 ≤ n ≤ k.
Example 7. N9 in Fig. 8 is not secure with respect to 2-ERNI. When l2 and l3 occur, a low level observer can deduce that h will occur, i.e., {l2, l3} _tr {h}. In this net, the occurrence of only one low transition does not give sufficient information about any high transitions, whereas the occurrence of two low level transitions together does. In the net in Fig. 9, no low transition alone reveals a high transition as well as no pair of low level transitions reveals a high transition. However, {l2, l4, l6} _tr {h1}, i.e., a low user, observing that all these three transitions occurred, can deduce that h1 will inevitably occur. Thus, this net is 2-ERNI secure whereas it is not 3-ERNI secure.
Obviously, 1-ERNI coincides with RNI, where no low transition alone reveals a high transition. Moreover, k-ERNI ⊆ RNI, for k ≥ 1. N9 is RNI secure since none of the low transitions reveals a high transition alone. 4.3
Another case can be the one in which an attacker is not able to deduce information by observing low transitions and this is because only repeated occurrence of a low transition gives information about the hidden part of the net. Thus, we assume that the attacker can count the occurrences of low transitions and so he can deduce information about the high transitions.
Definition 10. Let N = (P, T, F, m0) be a Petri net, T = H ∪ L, H ∩ L = ∅, L, H 6= ∅. Let Unf(N ) be the unfolding of N , where Unf(N ) = ((B, E, F, c0), λ), λ : B ∪ E → P ∪ T . Let n > 0.
N is secure with respect to n-Repeated-Reveals based Non-Interference (nReRNI) iff ∀l ∈ L ∀h ∈ H ∀m ≤ n ¬(l Remtr h).
N is ReRNI, iff it is n-ReRNI for all n > 0.
Proposition 3. n-ReRNI =⇒ (n − 1)-ReRNI The proof follows from the definition.
Example 8. N10 in Fig. 8 is not 2-ReRNI secure. Although the first occurrence of l1 does not reveal a high transition, by observing its second occurrence an observer can deduce that h2 occurred. However, the net is RNI secure as well
Fig. 10. as ERNI secure. In the net in Fig. 10, an observer cannot infer about the high transitions by observing l1 occurring only once. Also the second occurrence of l1 does not tell the observer which high transition occurred or will occur. However, the observer can deduce that h2 has already occurred or will occur inevitably if he observes three occurrences of l1. Therefore, this net is 2-ReRNI secure but it is not 3-ReRNI secure. Note that if the transition h3 was absent then every maximal run would include at least one occurrence of h2 and then, even without observing l1, the occurrence of h2 would be inevitable.
The following proposition is directly derived from Prop. 1.
Proposition 4. If a net is RNI secure then it is 1-ReRNI secure.
However, the previous implication does not hold in the opposite direction. Consider the net in Fig. 4 and let t1 be a low transition, t2 and t3 be high transitions. This net is 1-ReRNI secure since the first occurrence of t1 does not reveal information about t2 and t3, as discussed in Example 5. However the net is not RNI secure since t1 tr t2 and t1 tr t3. Note that this net is not secure with respect to 2-ReRNI since the second occurrence of t1 reveals both t2 and t3, i.e. t1 Re2 tr t2 and t1 Re2 tr t3.
Although k-ERNI and n-ReRNI are not comparable since they are parametric notions which are based on observing different things (for k-ERNI it is observation of occurrences of different low transitions together whereas for nReRNI it is observation of multiple occurrences of the same low transition) there are nets which are secure with respect to both and which are secure with respect to only one of them.
Both k-ERNI and n-ReRNI catch positive information flow about the past or future occurrences of high transitions, whereas they allow negative information flow. In the following we will introduce a notion considering both positive and negative information flow. 4.4
Until now we explored positive information flow on Petri nets. In order to catch negative information flow which is related to non-occurrence of high transitions, we need to consider the excludes relation between low and high transitions, as introduced in Def. 4.
Definition 11. Let N = (P, T, F, m0) be a Petri net, T = H ∪ L, H ∩ L = ∅, L, H 6= ∅. N is secure with respect to Positive/Negative Non-Interference (PNNI) iff ∀l ∈ L ∀h ∈ H, l 6 trh and ¬(l ex h).
If in a Petri net N , no low transition reveals a high transition and no low transition excludes a high transition, N is considered to be PNNI secure. PNNI is stronger than RNI, i.e., PNNI ⊆ RNI, and this follows directly from the definitions. In order to be PNNI secure, a net has to be RNI secure (no low transition reveals a high transition) and to satisfy an additional requirement (no low transition excludes a high transition).
Fig. 11.
Example 9. Both N11 and N12 in Fig. 11 are not PNNI secure since a low transition l1 excludes a high transition h. Thus, by observing occurrence of l1, an observer can deduce that h did not occur and will not occur.
N13 in Fig. 12 is not secure with respect to PNNI because of the negative information flow, i.e., l2 excludes h1 as well as it excludes h2. An observer can deduce that none of the high transitions occurred and they will not occur in the future by observing l2 or l3. This net is RNI, ERNI and ReRNI secure.
In the same figure, N14 is a PNNI secure Petri net. No low transition reveals a high transition as well as no low transition excludes a high transition. However an observer is able to deduce that h1 will occur inevitably by observing the occurrences of both l2 and l3, i.e., {l2, l3} _tr {h1}. In other words, this net is not 2-ERNI while it is RNI and ReRNI secure.
Fig. 12.
As seen in the previous example, PNNI is strictly stronger than RNI.
PNNI and k-ERNI are intersecting for any k, PNNI ∩ k-ERNI 6= ∅, PNNI \ k-ERNI 6= ∅, k-ERNI \ PNNI 6= ∅. None of them is stronger than the other one. The net N15 in Fig. 13 is both ERNI and PNNI secure, whereas N16 in Fig. 13 is not PNNI secure, however it is ERNI secure. N14 of Fig. 12 is PNNI secure, whereas it is not secure with respect to 2-ERNI as it is discussed in example 9.
PNNI and n-ReRNI are also intersecting for any n. A net which is both PNNI and ReRNI secure is the one in Fig. 6. The net in Fig. 10 is not secure with respect to 3-ReRNI whereas it is PNNI secure. If we add to the net another low transition l2 which consumes a token from p5, the net becomes not secure with respect to PNNI as well as with respect to RNI, since l2 reveals h1.
We have introduced new notions of non-interference for Petri nets. These notions are based on the reveals and the excludes relations and on the progress assumption.
One major difference between these notions with the existing ones, recalled in Section 4, is that the new notions explicitly consider the information flow both about the past and the future occurrences of high transitions. For example, if a low user can tell that the occurrence of a high transition is inevitable in the future, such a system is considered to be not secure according to the notions we have here introduced, whereas it is considered secure by the old notions such as SNNI, BSNNI, PBNI+ and PBNI. Similarly, for the negative information flow, we consider both past and future non-occurrences of high transitions.
Another important difference is shown by N4 in Fig. 6. This net is not secure according to SNNI even if a low user cannot infer which high transitions actually occurred. On the other hand, it is secure with respect to all non-interference notions based on reveals and excludes, since these require the capability of differentiating among the high transitions.
Moreover, the notions recalled in Section 4 are defined for 1-safe Petri nets, whereas RNI, k-ERNI, n-ReRNI and PNNI are defined for general Petri nets.
Fig. 14.
Figure 14 illustrates the relation between our notions and the other notions we have discussed so far. For the sake of simplicity, we only consider the weakest (SNNI ) and the strongest (PBNI ) notions from the ones recalled in Section 4. with the weakest of the new notions, i.e., RNI, and with the intersection set, denoted R-E in Fig. 14, of the new notions RNI, k-ERNI, n-ReRNI and PNNI.
We will examine three examples to discuss the differences of these classes.
A net which is secure with respect to all notions based on reveals and excludes and which is not secure with respect to SNNI is denoted by X in Fig. 14 and it is the one in Fig. 6. We consider this net secure since an observer cannot differentiate among the high transitions even if he can know some high actions have been performed (or will be performed). However, this net is not secure with respect to SNNI.
The net denoted by Y in Fig. 14 is secure with respect to all non-interference notions based on reveals and excludes as well as with respect to PBNI. This net can be N15 in Fig. 13. This net is secure since no low transition reveals a high transition (alone or together with another transition) as well as no low transition excludes a high transition. Thus there is neither positive nor negative information flow. It is also secure with respect to PBNI due to the fact that there is no active causal or active conflict place.
Two nets which are secure with respect to PBNI but not secure with respect to any of the non-interference notions based on reveals and excludes, denoted by Z in Fig. 14, are for example N6 in Fig. 7 and N12 in Fig. 11. 6
In this paper, we have proposed several new notions of non-interference for Petri nets, and compared them with notions already proposed in the literature. In this approach, the transitions of a system net are partitioned into two disjoint sets: the low and the high transitions. A system net is considered secure, or free from interference, if, from the observation of the occurrence of a low transition, or a set of low transitions, it is not possible to infer information on the occurrence of a high transition. Our new non-interference notions rely on net unfolding and on two relations among transitions. The first one is an adaptation to Petri nets of the reveals relation, previously defined on occurrence nets and not yet considered in this context; in particular we have introduced a class of parametrized reveals relations for Petri nets. The second relation is called excludes and it has been introduced here with the aim of capturing negative information flow.
The notion of RNI states that a net is secure if no low transition reveals any high transition. We have shown that this notion captures some situations which were not captured by the existing notions. We also propose more restrictive notions: k-ERNI based on observing occurrences of multiple low transitions and n-ReRNI based on the ability of the low user to count the occurrences of a low transition.
By adding the excludes relation to the picture, we allow one to infer negative information, namely the fact that a high transition has not occurred and will not occur. This is the basis of PNNI. The paper includes a comparison between the notions introduced here and those found in the literature on the subject.
The notions proposed in this paper, and further variants of them, should now be tested on more realistic cases. Our aim is to build a collection of different non-interference properties, so that a system designer, or a system analyzer, can choose those more appropriate to a specific case. A generalization could be a noninterference notion based on a parametric reveals relation between multisets of transitions.
We are currently starting to explore algorithms to check non-interference. In
particular, along a similar line to that followed in [
We are also interested in further investigating the excludes relation and the possibility to apply it in different contexts.
This work was partially supported by MIUR and by MIUR - PRIN 2010/2011 grant ‘Automi e Linguaggi Formali: Aspetti Matematici e Applicativi’, code H41J12000190001.