Commit ab80f376 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

Reordering so it goes Variables -> Constructor -> Getters -> Public...

Reordering so it goes Variables -> Constructor -> Getters -> Public Alteration/Setters -> Private functions
parent 95ffbb79
......@@ -5,12 +5,7 @@ package mohawk.refine;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.Vector;
import java.util.*;
import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
......@@ -30,6 +25,27 @@ import mohawk.rbac.RBACInstance;
public class RolesAbsRefine {
public final static Logger logger = Logger.getLogger("mohawk");
private RoleDepTree rdeptree;
private RBACInstance unsliced;
private RBACInstance nextinstance;
private Vector<String> allroles;
private Vector<String> nextsetroles;
private Map<String, Vector<CAEntry>> nextCA;
private Map<String, Vector<CREntry>> nextCR;
private Map<String, Vector<Integer>> nextUA;
private Vector<String> nextUsers;
private Vector<String> nextSpec;
private Vector<String> nextAdmin;
private Map<Integer, Integer> mMapping;
private Map<String, Vector<CAEntry>> mAllCA;
private Map<String, Vector<CREntry>> mAllCR;
private Map<String, Vector<Integer>> mAllUA;
private int refinementstep;
private String strRole;
private int k;
private int lastpriority;
private NuSMVMode mode;// mode
public RolesAbsRefine(RBACInstance inRbac) {
mode = NuSMVMode.BMC;// Default mode is BMC
......@@ -44,10 +60,208 @@ public class RolesAbsRefine {
buildTree();
}
public String getSpecRole() {
return strRole;
}
public RBACInstance getInputRBACInstance() {
return unsliced;
}
private Set<String> getAdminRoles() {
Set<String> sAdminRoles = new HashSet<String>();
Vector<String> Admin = unsliced.getAdmin();
for (int i = 0; i < Admin.size(); i++) {
String strUser = Admin.get(i);
Vector<Integer> vUA = mAllUA.get(strUser);
for (int j = 0; j < vUA.size(); j++) {
int roleindex = vUA.get(j);
String strRole = this.allroles.get(roleindex);
sAdminRoles.add(strRole);
}
}
return sAdminRoles;
}
public Boolean getResult(RBACInstance curInstance, Integer fileno) throws IOException, InterruptedException {
WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, "smvtemplate");
nusmv.fillAttributes(curInstance);
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC) {
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(curInstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
curInstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
} else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
return result;
}
public void getAllPosDeps(Vector<String> vPosDeps, Vector<String> vNegDeps, String strRole) {
Vector<String> vWorkQueue = new Vector<String>();
vWorkQueue.add(strRole);
rdeptree.addRole(strRole, 0);
while (!vWorkQueue.isEmpty()) {
String strNextRole = vWorkQueue.firstElement();// Get first element
// from queue.
vWorkQueue.remove(strNextRole);
Vector<String> vTmpPosDeps = new Vector<String>();
Vector<String> vTmpNegDeps = new Vector<String>();
getPosDeps(vTmpPosDeps, vTmpNegDeps, strNextRole);
int nextLevel = rdeptree.getRoleLevel(strNextRole) + 1;
Iterator<String> itrPos = vTmpPosDeps.iterator();
while (itrPos.hasNext()) {
String tmpRole = itrPos.next();
if (!vPosDeps.contains(tmpRole)) {
vPosDeps.add(tmpRole);
vWorkQueue.add(tmpRole);
rdeptree.addRole(tmpRole, nextLevel);
}
}
Iterator<String> itrNeg = vTmpNegDeps.iterator();
while (itrNeg.hasNext()) {
String tmpRole = itrNeg.next();
if (!vNegDeps.contains(tmpRole)) {
vNegDeps.add(tmpRole);
rdeptree.addRole(tmpRole, nextLevel);
}
}
}
}
/* Helper function for getAllPosDeps */
public void getPosDeps(Vector<String> vPosDeps, Vector<String> vNegDeps, String strRole) {
Vector<CAEntry> vMatchingCA = unsliced.getCA().get(strRole);
if (vMatchingCA == null)
return;
for (int i = 0; i < vMatchingCA.size(); i++) {
CAEntry cae = vMatchingCA.get(i);
PreCondition pcPreCond = cae.getPreConditions();
if (pcPreCond.size() != 0) {
for (int roleindex : pcPreCond.keySet()) {
String strDepRole = unsliced.getRoles().get(roleindex);
if (pcPreCond.getConditional(roleindex) == 1)
vPosDeps.add(strDepRole);
else
vNegDeps.add(strDepRole);
}
}
}
}
public void setMode(NuSMVMode curmode) {
this.mode = curmode;
}
public boolean refineRoles() {
if (nextsetroles.size() == allroles.size())
return false;
// Set<String> incrementRoles = rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>();// =
// rdeptree.getRoles(refinementstep);
for (int i = 0; i < k; i++) {
Set<String> sNextQueue = this.rdeptree.getRoles(lastpriority);
if (sNextQueue != null) {
incrementRoles.addAll(sNextQueue);
lastpriority++;
} else
break;
}
if (incrementRoles.size() == 0)
return false;
else
nextsetroles.addAll(incrementRoles);
refinementstep++;
return true;
}
public ExecutionResult absrefineloop() {
Integer fileno = 1;
try {
while (refine()) {
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
try {
writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
} catch (IOException e1) {
e1.printStackTrace();
}
System.out.printf("\n\n-----\n Starting Refinement Step %d, with %d Roles and %d Rules\n", fileno,
nextinstance.getNumRoles(), nextinstance.getNumRules());
Boolean result = getResult(nextinstance, fileno);
if (result) {
System.out.println("Found counter example in step " + (fileno));
WriteMapping(nextinstance, "ROLEMAPPING");
return ExecutionResult.GOAL_REACHABLE;
} else {
System.out.println("No counter example found in refinement step " + fileno);
}
fileno++;
}
} catch (Exception e) {
e.printStackTrace();
return ExecutionResult.ERROR_OCCURRED;
}
System.out.println("\n\n----\n No counter example found in " + (fileno - 1) + " refinement steps");
return ExecutionResult.GOAL_UNREACHABLE;
}
/**
* A quick function to see if this will get rid of the NuSMV error that is given when trying to use the SMV code
* generated by RBAC2SMV.java
*
* @author Jonathan Shahen
* @return
*/
public RBACInstance refineOnly() {
refine();
return nextinstance;
}
public void WriteMapping(RBACInstance inrbacinstance, String filename) throws IOException {
FileWriter file = new FileWriter(filename);
Vector<String> vRoles = inrbacinstance.getRoles();
for (int i = 0; i < vRoles.size(); i++) {
file.write(i + " " + vRoles.get(i) + "\n");
}
file.close();
}
private void firstabstraction() {
Set<String> sFirstSetRoles = new HashSet<String>();
......@@ -84,24 +298,6 @@ public class RolesAbsRefine {
this.refinementstep = 1;
}
private Set<String> getAdminRoles() {
Set<String> sAdminRoles = new HashSet<String>();
Vector<String> Admin = unsliced.getAdmin();
for (int i = 0; i < Admin.size(); i++) {
String strUser = Admin.get(i);
Vector<Integer> vUA = mAllUA.get(strUser);
for (int j = 0; j < vUA.size(); j++) {
int roleindex = vUA.get(j);
String strRole = this.allroles.get(roleindex);
sAdminRoles.add(strRole);
}
}
return sAdminRoles;
}
private void sliceUA() throws Exception {
if (nextUA == null)
......@@ -151,32 +347,6 @@ public class RolesAbsRefine {
}
}
public boolean refineRoles() {
if (nextsetroles.size() == allroles.size())
return false;
// Set<String> incrementRoles = rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>();// =
// rdeptree.getRoles(refinementstep);
for (int i = 0; i < k; i++) {
Set<String> sNextQueue = this.rdeptree.getRoles(lastpriority);
if (sNextQueue != null) {
incrementRoles.addAll(sNextQueue);
lastpriority++;
} else
break;
}
if (incrementRoles.size() == 0)
return false;
else
nextsetroles.addAll(incrementRoles);
refinementstep++;
return true;
}
/*
* This function is incharge of slicing the CA rules.
*/
......@@ -299,178 +469,4 @@ public class RolesAbsRefine {
return result;
}
public Boolean getResult(RBACInstance curInstance, Integer fileno) throws IOException, InterruptedException {
WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, "smvtemplate");
nusmv.fillAttributes(curInstance);
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC) {
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(curInstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
curInstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
} else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
return result;
}
public ExecutionResult absrefineloop() {
Integer fileno = 1;
try {
while (refine()) {
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
try {
writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
} catch (IOException e1) {
e1.printStackTrace();
}
System.out.printf("\n\n-----\n Starting Refinement Step %d, with %d Roles and %d Rules\n", fileno,
nextinstance.getNumRoles(), nextinstance.getNumRules());
Boolean result = getResult(nextinstance, fileno);
if (result) {
System.out.println("Found counter example in step " + (fileno));
WriteMapping(nextinstance, "ROLEMAPPING");
return ExecutionResult.GOAL_REACHABLE;
} else {
System.out.println("No counter example found in refinement step " + fileno);
}
fileno++;
}
} catch (Exception e) {
e.printStackTrace();
return ExecutionResult.ERROR_OCCURRED;
}
System.out.println("\n\n----\n No counter example found in " + (fileno - 1) + " refinement steps");
return ExecutionResult.GOAL_UNREACHABLE;
}
/**
* A quick function to see if this will get rid of the NuSMV error that is given when trying to use the SMV code
* generated by RBAC2SMV.java
*
* @author Jonathan Shahen
* @return
*/
public RBACInstance refineOnly() {
refine();
return nextinstance;
}
public void WriteMapping(RBACInstance inrbacinstance, String filename) throws IOException {
FileWriter file = new FileWriter(filename);
Vector<String> vRoles = inrbacinstance.getRoles();
for (int i = 0; i < vRoles.size(); i++) {
file.write(i + " " + vRoles.get(i) + "\n");
}
file.close();
}
public void getAllPosDeps(Vector<String> vPosDeps, Vector<String> vNegDeps, String strRole) {
Vector<String> vWorkQueue = new Vector<String>();
vWorkQueue.add(strRole);
rdeptree.addRole(strRole, 0);
while (!vWorkQueue.isEmpty()) {
String strNextRole = vWorkQueue.firstElement();// Get first element
// from queue.
vWorkQueue.remove(strNextRole);
Vector<String> vTmpPosDeps = new Vector<String>();
Vector<String> vTmpNegDeps = new Vector<String>();
getPosDeps(vTmpPosDeps, vTmpNegDeps, strNextRole);
int nextLevel = rdeptree.getRoleLevel(strNextRole) + 1;
Iterator<String> itrPos = vTmpPosDeps.iterator();
while (itrPos.hasNext()) {
String tmpRole = itrPos.next();
if (!vPosDeps.contains(tmpRole)) {
vPosDeps.add(tmpRole);
vWorkQueue.add(tmpRole);
rdeptree.addRole(tmpRole, nextLevel);
}
}
Iterator<String> itrNeg = vTmpNegDeps.iterator();
while (itrNeg.hasNext()) {
String tmpRole = itrNeg.next();
if (!vNegDeps.contains(tmpRole)) {
vNegDeps.add(tmpRole);
rdeptree.addRole(tmpRole, nextLevel);
}
}
}
}
/* Helper function for getAllPosDeps */
public void getPosDeps(Vector<String> vPosDeps, Vector<String> vNegDeps, String strRole) {
Vector<CAEntry> vMatchingCA = unsliced.getCA().get(strRole);
if (vMatchingCA == null)
return;
for (int i = 0; i < vMatchingCA.size(); i++) {
CAEntry cae = vMatchingCA.get(i);
PreCondition pcPreCond = cae.getPreConditions();
if (pcPreCond.size() != 0) {
for (int roleindex : pcPreCond.keySet()) {
String strDepRole = unsliced.getRoles().get(roleindex);
if (pcPreCond.getConditional(roleindex) == 1)
vPosDeps.add(strDepRole);
else
vNegDeps.add(strDepRole);
}
}
}
}
public RBACInstance getInputRBACInstance() {
return unsliced;
}
private RoleDepTree rdeptree;
private RBACInstance unsliced;
private RBACInstance nextinstance;
private Vector<String> allroles;
private Vector<String> nextsetroles;
private Map<String, Vector<CAEntry>> nextCA;
private Map<String, Vector<CREntry>> nextCR;
private Map<String, Vector<Integer>> nextUA;
private Vector<String> nextUsers;
private Vector<String> nextSpec;
private Vector<String> nextAdmin;
private Map<Integer, Integer> mMapping;
private Map<String, Vector<CAEntry>> mAllCA;
private Map<String, Vector<CREntry>> mAllCR;
private Map<String, Vector<Integer>> mAllUA;
private int refinementstep;
private String strRole;
private int k;
private int lastpriority;
private NuSMVMode mode;// mode
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment