Commit bd0dc9da authored by Jonathan Shahen's avatar Jonathan Shahen

Adding 3 Heuristics and 1 new optimization to Mohawk 2.0 (regression tests...

Adding 3 Heuristics and 1 new optimization to Mohawk 2.0 (regression tests pass, still need to test ASASPTIME tests)
parent 9ff9ec5c
package mohawk.refine;
import java.io.IOException;
import java.util.*;
import java.util.logging.Logger;
import mohawk.global.pieces.mohawk.CAEntry;
import mohawk.global.pieces.mohawk.CREntry;
import mohawk.global.timing.MohawkTiming;
import mohawk.output.WriteRBACSpec;
import mohawk.rbac.RBACInstance;
public class RemoveUnsetRoles {
public static final Logger logger = Logger.getLogger("mohawk");
private RBACInstance inst;
private MohawkTiming timing;
private String timingPrefix;
// target role name -> list of rules
private Map<String, Vector<CAEntry>> mCA;
// target role name -> list of rules
private Map<String, Vector<CREntry>> mCR;
// user name -> list of roles using their index
private Map<String, Vector<Integer>> mUA;
private boolean debugMsg = true;
public RemoveUnsetRoles(RBACInstance in, MohawkTiming timing, String timingPrefix) {
inst = in;
this.timing = timing;
this.timingPrefix = timingPrefix;
mCA = new HashMap<String, Vector<CAEntry>>(in.getCA());
mCR = new HashMap<String, Vector<CREntry>>(in.getCR());
mUA = new HashMap<String, Vector<Integer>>();
}
/**
* Slices away the Unset (not used in a single rule as the target for CA) Roles and replaces them with literals
* IF the precondition requires a Unset Role then it is defaulted to FALSE (and thus can remove the whole rule)
* IF the precondition requires to NOt have a Unset Role then the role is substituted to TRUE
* @return whether an error occurred
* @throws Exception
*/
public RBACInstance getOptimizedRBAC() throws Exception {
String timerKey = timingPrefix + "->RemoveUnsetRoles.slice()";
/* timing */timing.startTimer(timerKey);
Set<String> targets = new HashSet<String>(inst.getTargetRolesSet()); // new list of roles
targets.addAll(inst.getAdminRoles());
Vector<String> vRoles = new Vector<String>(targets);
Set<String> unset = inst.getRolesSet();
unset.removeAll(targets);
// If there are no roles to remove, just return the original RBAC instance
if (unset.isEmpty()) { return inst; }
HashSet<Integer> removeRolesIndex = new HashSet<Integer>(unset.size());
for (String role : unset) {
logger.fine("[RemoveUnsetRoles] Removing role: " + role + " from all Rules");
removeRolesIndex.add(inst.getRoleIndex(role));
}
Vector<String> caRoles = new Vector<String>(mCA.keySet());
for (int j = mCA.keySet().size() - 1; j >= 0; j--) {
Vector<CAEntry> mCa = mCA.get(caRoles.get(j));
for (int i = mCa.size() - 1; i >= 0; i--) {
CAEntry ca = mCa.get(i);
if (ca.updateRule(removeRolesIndex, vRoles, inst.getRoleMap()) == false) {
logger.fine("[RemoveUnsetRoles] Removing CA rule: " + ca + " from all Rules");
mCa.remove(i);
}
}
if (mCa.isEmpty()) {
mCA.remove(caRoles.get(j));
}
}
Vector<String> crRoles = new Vector<String>(mCR.keySet());
for (int i = crRoles.size() - 1; i >= 0; i--) {
// Remove the CR rule if the target role is in unset
if (unset.contains(crRoles.get(i))) {
logger.fine("[RemoveUnsetRoles] Removing all CR rules for: " + crRoles.get(i));
mCR.remove(crRoles.get(i));
}
}
// Update mUA to point to the new role indexes
for (String user : inst.getUA().keySet()) {
Vector<Integer> roles = inst.getUA().get(user);
Vector<Integer> newRoles = new Vector<Integer>(roles.size());
for (Integer role : roles) {
newRoles.add(vRoles.indexOf(inst.getRoleFromIndex(role)));
}
mUA.put(user, newRoles);
}
if (debugMsg == true) {
System.out.println("vRoles: " + vRoles);
System.out.println("unset: " + unset);
System.out.println("mUA: " + mUA);
System.out.println("mCR: " + mCR);
System.out.println("mCA: " + mCA);
System.out.println("SPEC: " + inst.getSpec());
}
/* timing */timing.stopTimer(timerKey);
RBACInstance bb = new RBACInstance(vRoles, inst.getUsers(), inst.getAdmin(), mUA, mCR, mCA, inst.getSpec());
try {
WriteRBACSpec writer = new WriteRBACSpec();
writer.Write2File(bb, "logs/testingRemoveUnsetRoles.mohawk");
} catch (IOException e1) {
e1.printStackTrace();
}
return bb;
}
}
......@@ -69,7 +69,7 @@ public class MohawkSettings {
* Flag for optimizing RBAC instances by removing the roles that are not present in any rules as a target
* and replacing them in all CA rule conditions as a constant (TRUE or FALSE)
*/
public boolean removeUnsetRolesRBAC = false;
public boolean removeUnsetRolesRBAC = true;
/**
* Flag that will run heuristics that speeds up results for easy/simple test cases
......
......@@ -12,8 +12,10 @@ import mohawk.global.pieces.mohawk.NuSMVMode;
import mohawk.global.results.ExecutionResult;
import mohawk.global.results.TestingResult;
import mohawk.math.CalculateDiameter;
import mohawk.output.WriteNuSMV;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
import mohawk.refine.RemoveUnsetRoles;
import mohawk.refine.RolesAbsRefine;
import mohawk.singleton.MohawkSettings;
import mohawk.slicer.RoleSlicer;
......@@ -93,6 +95,7 @@ public class TestingSuite {
for (Integer i = 0; i < numSpecFiles; i++) {
/* TIMING */settings.timing.startTimer("runTests.mainLoop (" + (i + 1) + "/" + numSpecFiles + ")");
for (Integer j = 0; j < modes.size(); j++) {
try {
String specFile = settings.smvHelper.specFiles.get(i).getAbsolutePath();
String timerName = "runTests.mainLoop (" + (i + 1) + "/" + numSpecFiles + ") - "
+ settings.smvHelper.specFiles.get(i).getName() + " (" + modes.get(j) + ")";
......@@ -106,8 +109,8 @@ public class TestingSuite {
RBACSpecReader reader = new RBACSpecReader(specFile);
RBACInstance rbac = reader.getRBAC();
logger.info("[DETAILS] Number of Roles: " + rbac.getNumRoles() + "; Number of Rules: "
+ (rbac.getCA().size() + rbac.getCR().size()));
logger.info("[DETAILS] Number of Roles: " + rbac.getNumRoles() +
"; Number of Rules: " + rbac.getNumRules());
// *******************************************************************************
// Heuristic #1
......@@ -123,7 +126,8 @@ public class TestingSuite {
settings.smvHelper.specFiles.get(i).getAbsolutePath(), "0",
comment + "; Result obtained by Heuristic #1");
System.out.println("Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
System.out.println(
"Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ rbac.getSpecRole()
+ "' in following spec file (in mode "
......@@ -138,34 +142,59 @@ public class TestingSuite {
// *******************************************************************************
try {
if (settings.sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
/* TIMING */settings.timing.startTimer(timerName + " (slicing)");
RoleSlicer roleslicer = new RoleSlicer(rbac, settings.timing, timerName);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles()
+ "; Number of Rules: " + (rbac.getCA().size() + rbac.getCR().size()));
rbac = this.optimizeRBAC(rbac, timerName);
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
/* TIMING */settings.timing.stopTimer(timerName + " (slicing)");
continue;
}
logger.info("[DETAILS] (After Optimizing) Number of Roles: " + rbac.getNumRoles() +
"; Number of Rules: " + rbac.getNumRules());
if (settings.sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
/* TIMING */settings.timing.startTimer(timerName + " (slicingQuery)");
if (rbac.getNumRoles() == 0) {
logger.info(
"[HEURISTIC #3a] There are no roles after optimization, thus the state isd UNREACHABLE "
+ "and will not convert to SMV and run");
// Setting up the lastResult information
/* TIMING */settings.timing.stopTimer(timerName);
settings.lastResult = new TestingResult(ExecutionResult.GOAL_UNREACHABLE,
settings.timing.getLastElapsedTime(),
settings.smvHelper.specFiles.get(i).getAbsolutePath(), "0",
comment + "; Result obtained by Heuristic #3a");
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
System.out.println("Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ rbac.getSpecRole()
+ "' in following spec file (in mode "
+ modes.get(j) + "): " + specFile);
/* TIMING */settings.timing.stopTimer(timerName + " (slicingQuery)");
settings.results.add(settings.lastResult);
settings.results.writeOutLast(resultsFW);
continue;
}
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
if (rbac.getNumRules() == 0) {
logger.info(
"[HEURISTIC #3b] There are no rules after optimization, thus the state is UNREACHABLE "
+ "and will not convert to SMV and run");
// Setting up the lastResult information
/* TIMING */settings.timing.stopTimer(timerName);
settings.lastResult = new TestingResult(ExecutionResult.GOAL_UNREACHABLE,
settings.timing.getLastElapsedTime(),
settings.smvHelper.specFiles.get(i).getAbsolutePath(), "0",
comment + "; Result obtained by Heuristic #3b");
System.out.println("Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ rbac.getSpecRole()
+ "' in following spec file (in mode "
+ modes.get(j) + "): " + specFile);
settings.results.add(settings.lastResult);
settings.results.writeOutLast(resultsFW);
continue;
}
......@@ -192,7 +221,8 @@ public class TestingSuite {
settings.smvHelper.specFiles.get(i).getAbsolutePath(), "0",
comment + "; Result obtained by Heuristic #2");
System.out.println("Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
System.out.println(
"Result: " + settings.lastResult + " for role '" + rbac.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ rbac.getSpecRole()
+ "' in following spec file (in mode "
......@@ -277,16 +307,93 @@ public class TestingSuite {
}
logger.info("Previous Elapsed Time: " + settings.timing.getLastElapsedTimeSec() + " seconds");
} catch (IOException e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
continue;
}
}
/* TIMING */settings.timing.stopTimer("runTests.mainLoop (" + (i + 1) + "/" + numSpecFiles + ")");
}
executor.shutdown();
try {
resultsFW.close();
} catch (IOException e) {
// DO NOTHING
}
/* TIMING */settings.timing.stopTimer("runTests.mainLoop");
logger.exiting(getClass().getName(), "runTests()");
}
public RBACInstance optimizeRBAC(RBACInstance rbac, String timerName) throws Exception {
int numRoles, numRules;
if (settings.sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
/* TIMING */settings.timing.startTimer(timerName + " (slicing)");
numRoles = rbac.getNumRoles();
numRules = rbac.getNumRules();
RoleSlicer roleslicer = new RoleSlicer(rbac, settings.timing, timerName);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> " +
"Number of Roles: " + numRoles + "->" + rbac.getNumRoles() +
" (" + (numRoles - rbac.getNumRoles()) + " diff); "
+ "Number of Rules: " + numRules + "->" + rbac.getNumRules() +
" (" + (numRules - rbac.getNumRules()) + " diff); ");
/* TIMING */settings.timing.stopTimer(timerName + " (slicing)");
}
if (settings.sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
/* TIMING */settings.timing.startTimer(timerName + " (slicingQuery)");
numRoles = rbac.getNumRoles();
numRules = rbac.getNumRules();
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
logger.info("[DETAILS] After Slicing Query -> " +
"Number of Roles: " + numRoles + "->" + rbac.getNumRoles() +
" (" + (numRoles - rbac.getNumRoles()) + " diff); "
+ "Number of Rules: " + numRules + "->" + rbac.getNumRules() +
" (" + (numRules - rbac.getNumRules()) + " diff); ");
/* TIMING */settings.timing.stopTimer(timerName + " (slicingQuery)");
}
if (settings.removeUnsetRolesRBAC) {
logger.info("[Slicing] Optimizing the RBAC Instance file by removing the unset roles");
/* TIMING */settings.timing.startTimer(timerName + " (removeUnsetRoles)");
numRoles = rbac.getNumRoles();
numRules = rbac.getNumRules();
RemoveUnsetRoles ruRole = new RemoveUnsetRoles(rbac, settings.timing, timerName);
rbac = ruRole.getOptimizedRBAC();
logger.info("[DETAILS] After Removing Unused Roles -> " +
"Number of Roles: " + numRoles + "->" + rbac.getNumRoles() +
" (" + (numRoles - rbac.getNumRoles()) + " diff); "
+ "Number of Rules: " + numRules + "->" + rbac.getNumRules() +
" (" + (numRules - rbac.getNumRules()) + " diff); ");
/* TIMING */settings.timing.stopTimer(timerName + " (removeUnsetRoles)");
}
logger.info("[DETAILS] (before returning) Number of Roles: " + rbac.getNumRoles() +
"; Number of Rules: " + rbac.getNumRules());
return rbac;
}
/**
* If you only want to convert SPEC files to SMV files. This can be used before running if there happens to be a
* crash while running the tests you can just resume from the test and not have to convert the SPEC to SMV every
......
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