The IF-Net complements the CPN by different security levels, access modes for transitions and tokens, and subjects, which are assigned to activities (transitions). We distinguish between two security levels low and high. Subjects can be assigned a security clearance, transitions have a security classification, and tokens have an attribute classification repre- sented as security level. Tokens with a high security classification are only allowed to be passed by activities with a high classification and only subjects with a high clearance are allowed to be assigned to such transitions as executor. This information is deposited in a so called labelling and access control model inside the IF-Net’s analysis context. There’s also a new type of declassification transition, which eases the security level by expecting a token with high classification and producing a token with low classification.
For example, a token with high classification can represent a construction plan in a company. Parts of the resulting product are produced by a third-party supplier, who shouldn’t be able to see the complete construction plan. For him an adjusted version of the construction plan with low classification is generated, which can be modelled in an IF-Net via a declassification transition.
Figure 4: Visualization of the IF-Net used in the example. The transition td is a declas- sification transition. Both the red tokens and the red transitions have a high security clearance, where the green tokens and green transitions have a low se- curity clearance. The subjects sh1 and sh2 have a high security clearance and the subject sl1 has a low clearance.
As an example, we build the IF-Net shown in figure 4. It contains a declassification transition and two regular transitions, where one has a high and the other has a low security clearance. The corresponding Java code using the SEPIA framework looks like the following:
IFNet ifnet = new IFNet();
ifnet.addPlace("pIn");
ifnet.addPlace("p1");
ifnet.addPlace("p2");
ifnet.addPlace("pOut");
ifnet.addTransition("tIn");
ifnet.addDeclassificationTransition("td");
ifnet.addTransition("tOut");
IFNetFlowRelation f1 = ifnet.addFlowRelationPT("pIn", "tIn");
IFNetFlowRelation f2 = ifnet.addFlowRelationTP("tIn", "p1");
IFNetFlowRelation f3 = ifnet.addFlowRelationPT("p1", "td");
IFNetFlowRelation f4 = ifnet.addFlowRelationTP("td", "p2");
IFNetFlowRelation f5 = ifnet.addFlowRelationPT("p2", "tOut");
IFNetFlowRelation f6 = ifnet.addFlowRelationTP("tOut", "pOut");
It is possible to add constraints to the flow relations to define the required and produced tokens and to set a maximum place capacity for specified token colors:
f2.addConstraint("red", 1);
f3.addConstraint("red", 1);
f4.addConstraint("green", 1);
f5.addConstraint("green", 1);
ifnet.getPlace("p2").setColorCapacity("green", 1);
Again an initial marking must be defined:
IFNetMarking sm = new IFNetMarking();
sm.set("pIn", new Multiset<String>("black"));
ifnet.setInitialMarking(sm);
The transitions can be assigned the access modes create, write, read, and delete for specified token colors. By default, they don’t have any of them assigned. Access modes can be set like follows:
RegularIFNetTransition tIn = ifnet.getTransition("tIn");
tIn.addAccessMode("red", AccessMode.CREATE);
For the assignment of security clearances for subjects, objects, and activities an analysis context is needed. It consists of a labeling and an access control model, which again contains a SOABase. The SOA base contains all names of subjects, objects, and activities:
SOABase context = new SOABase("DataUsage");
context.setSubjects(Arrays.asList("sh1", "sh2", "sl0"));
context.setObjects(Arrays.asList("red", "green", "black"));
context.setActivities(Arrays.asList("tIn", "td", "tOut"));
An access control model defines which activities subjects are allowed to perform, based on the formerly defined SOABase. Different access control models can be found in the SEWOL project (see Library Dependencies in section 1.1).
ACLModel acl = new ACLModel("ACL", context);
acl.addActivityPermission("sh1", "tIn");
acl.addActivityPermission("sh2", "td");
acl.addActivityPermission("sl0", "tOut");
In the other direction, the analysis context assigns subjects to transitions.
AnalysisContext ac = new AnalysisContext("ac", acl, true);
// Assign subjects to transitions
ac.setSubjectDescriptor("tIn", "sh1");
ac.setSubjectDescriptor("td", "sh2");
ac.setSubjectDescriptor("tOut", "sl0");
Based on this analysis context a labeling can be defined, which assigns security levels to transitions, subjects, and token colors:
Labeling l = ac.getLabeling();
// Set subject clearance
l.setSubjectClearance("sh1", SecurityLevel.HIGH);
l.setSubjectClearance("sh2", SecurityLevel.HIGH);
l.setSubjectClearance("sl0", SecurityLevel.LOW);
// set transition classification
l.setActivityClassification("tIn", SecurityLevel.HIGH);
l.setActivityClassification("td", SecurityLevel.HIGH);
l.setActivityClassification("tOut", SecurityLevel.LOW);
// set token color classification
l.setAttributeClassification("red", SecurityLevel.HIGH);
l.setAttributeClassification("green", SecurityLevel.LOW);
In the end the analysis context is given to the IF-Net:
ifnet.setAnalysisContext(ac);
The dependencies between analysis context, labeling, access control model, and SOA base can be seen in figure 5.
Figure 5: Relationships between analysis context, labeling, access control model, and SOA base.
For a valid IF-Net, the analysis context of an IF-Net must be valid, additionally to the conditions for validity of CPNs. This is the case, if the analysis context contains all token colors and activities of an IF-Net. Also a subject must be assigned to every activity and the security clearances of activities, objects, and subjects must be consistent. For a declassification transition producing a token color, no other transition in the Petri net is allowed to produce a token with the same color. A valid IF-Net must also meet some workflow conditions. At least one token of the control flow token color, by default black, must be consumed and produced by all transitions. The IF-Net must have the option to complete, i.e. the process can enter an end state. The end states must be proper, s.th. there are no remaining control flow tokens in the Petri net when entering the end state. Also there must be no dead transition, so every activity can be executed in at least one trace.