Commit 38a4c5bc authored by Jonathan Shahen's avatar Jonathan Shahen

Setting up Heuristics to make quicker decisions without having to convert to...

Setting up Heuristics to make quicker decisions without having to convert to NuSMv and without having to run it through the NuSMv SAT solver
Heuristic #1: returns GOAL_UNREACHABLE if the SPC role cannot be found in the target role of any CA rule (see heuristic1.spec for an example)
Heuristic #2: return GOAL_REACHABLE if there is a CA rule that has the target role equal to the SPEC role and that rule is 'startable' (ONLY negative preconditions or TRUE)
parent a30015c2
Roles role0 role1 role2 role3 role4;
Users user0 user1 user2 user3 user4;
UA
<user4,role3>;
CR
<FALSE,role0>
<FALSE,role2>;
CA
<role3,role2,role0>
<role3,role2&role1,role0>
<role3,role2&role0,role1>
<role3,TRUE,role1>
<role3,role0,role1>
<role3,role1&role0,role2>
<role3,role0,role2>
<role3,role1,role2>
<role3,TRUE,role2>;
ADMIN user4;
// This role is never targeted
SPEC user0 role4;
Roles role0 role1 role2 role3 role4;
Users user0 user1 user2 user3 user4;
UA
<user4,role3>;
CR
<FALSE,role0>
<FALSE,role2>;
CA
<role3,role2,role0>
<role3,role2&role1,role0>
<role3,role2&role0,role1>
<role3,TRUE,role1>
<role3,role0,role1>
<role3,role1&role0,role2>
<role3,role0,role2>
<role3,role1,role2>
<role3,TRUE,role2>;
ADMIN user4;
// The rule '<role3,TRUE,role2>' is startable and thus should be caught by heuristic #2
SPEC user0 role2;
Roles role0 role1 role2 role3 role4;
Users user0 user1 user2 user3 user4;
UA
<user4,role3>;
CR
<FALSE,role0>
<FALSE,role2>;
CA
<role3,role2,role0>
<role3,role2&role1,role0>
<role3,role2&role0,role1>
<role3,TRUE,role1>
<role3,role0,role1>
<role3,role1&role0,role2>
<role3,role0,role2>
<role3,role1,role2>
<role3,-role2,role4>;
ADMIN user4;
// The rule '<role3,-role2,role4>' is startable and thus should be caught by heuristic #2
SPEC user0 role2;
......@@ -23,11 +23,18 @@ public class RBACInstance {
private Vector<String> vRoles;
private Vector<String> vUsers;
private Vector<String> vAdmin;
// integer 1,2,3,...,vRoles.size() -> the role name
private Map<Integer, String> mRoleIndex;
// integer 1,2,3,...,vUsers.size() -> the user name
private Map<Integer, String> mUserIndex;
// user name -> list of roles using their index
private Map<String, Vector<Integer>> vUA;
// target role name -> list of rules
private Map<String, Vector<CREntry>> mCR;
// target role name -> list of rules
private Map<String, Vector<CAEntry>> mCA;
// [user name, goal role name]
private Vector<String> vSpec;
public RBACInstance(Vector<String> invRoles, Vector<String> invUsers, Vector<String> invAdmin,
......@@ -84,6 +91,10 @@ public class RBACInstance {
return vRoles;
}
public Set<String> getRolesSet() {
return new HashSet<String>(vRoles);
}
public Vector<String> getUsers() {
return vUsers;
}
......@@ -112,7 +123,19 @@ public class RBACInstance {
return vSpec;
}
public String getSpecUser() {
return vSpec.get(0);
}
public String getSpecRole() {
return vSpec.get(1);
}
public Vector<String> getAdminRoles() {
return new Vector<String>(getAdminRolesSet());
}
public Set<String> getAdminRolesSet() {
Set<String> roles = new HashSet<String>();
for (Vector<CAEntry> cas : mCA.values()) {
......@@ -121,6 +144,18 @@ public class RBACInstance {
}
}
return new Vector<String>(roles);
return roles;
}
public Vector<String> getTargetRoles() {
return new Vector<String>(getTargetRolesSet());
}
/**
* Returns the role names of the target CA rules
* @return the keyset for mCA
*/
public Set<String> getTargetRolesSet() {
return mCA.keySet();
}
}
......@@ -69,7 +69,12 @@ 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 optimizeRBAC = false;
public boolean removeUnsetRolesRBAC = false;
/**
* Flag that will run heuristics that speeds up results for easy/simple test cases
*/
public boolean runHeuristics = true;;
protected MohawkSettings() {
}
......
......@@ -26,7 +26,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
......@@ -37,7 +37,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
......@@ -48,7 +48,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
......@@ -59,7 +59,40 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
public void runHeuristic1() {
String param = "-input data/regressiontests/heuristic1.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_UNREACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
public void runHeuristic2() {
String param = "-input data/regressiontests/heuristic2.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
@Test
public void runHeuristic3() {
String param = "-input data/regressiontests/heuristic3.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult._result);
}
private String[] params(String param) {
......
......@@ -7,6 +7,7 @@ import java.util.concurrent.*;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.global.pieces.mohawk.CAEntry;
import mohawk.global.pieces.mohawk.NuSMVMode;
import mohawk.global.results.ExecutionResult;
import mohawk.global.results.TestingResult;
......@@ -103,6 +104,34 @@ public class TestingSuite {
logger.info("[DETAILS] Number of Roles: " + rbac.getNumRoles() + "; Number of Rules: "
+ (rbac.getCA().size() + rbac.getCR().size()));
// *******************************************************************************
// Heuristic #1
if (settings.runHeuristics == true) {
if (!rbac.getTargetRolesSet().contains(rbac.getSpecRole())) {
System.out.println("[HEURISTIC #1] Cannot find SPEC role in any of the CA target roles! "
+ "This RBAC Instance is unreachable!");
// 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 #1");
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;
}
}
// *******************************************************************************
try {
if (settings.sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
......@@ -131,7 +160,46 @@ public class TestingSuite {
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
continue;
}
// *******************************************************************************
// Heuristic #2
if (settings.runHeuristics == true) {
boolean ruleIsStartable = false;
for (CAEntry carule : rbac.getCA().get(rbac.getSpecRole())) {
if (carule.isStartable()) {
ruleIsStartable = true;
break;
}
}
if (ruleIsStartable) {
System.out.println("[HEURISTIC #2] Found a startable CA rule with the SPEC role, "
+ "thus this rule can fire upon starting and thus solve the SPEC in 1 step.");
// Setting up the lastResult information
/* TIMING */settings.timing.stopTimer(timerName);
settings.lastResult = new TestingResult(ExecutionResult.GOAL_REACHABLE,
settings.timing.getLastElapsedTime(),
settings.smvHelper.specFiles.get(i).getAbsolutePath(), "0",
comment + "; Result obtained by Heuristic #2");
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;
}
}
// *******************************************************************************
RolesAbsRefine absrefine = new RolesAbsRefine(rbac, settings.timing, timerName);
absrefine.setMode(modes.get(j));
......@@ -150,6 +218,7 @@ public class TestingSuite {
}
/* TIMING */settings.timing.stopTimer(timerName + " (TestRunner)");
// Setting up the lastResult information
/* TIMING */settings.timing.stopTimer(timerName);
settings.lastResult._duration = settings.timing.getLastElapsedTime();
settings.lastResult._filename = settings.smvHelper.specFiles.get(i).getAbsolutePath();
......
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