Commit 4d9458dc authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

fixed README formatting; edited regression tests; allowed NOT to have...

fixed README formatting; edited regression tests; allowed NOT to have whitespace between it and the tilde (~); allowed for administrator role in a rule to be TRUE; included an Expected command in the SPEC files
parent e0b77992
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
# How To Use # How To Use
1. Best way to get working with the code is to open it in Eclipse 1. Best way to get working with the code is to open it in Eclipse
2. You will need to have Java 1.8 installed and Ant 2. You will need to have Java 1.8 installed and Ant
3. Load it up in eclipse and go to the Ant window (Window -> Show View -> Ant) and click on "Run the Default Target"<br/> 3. Load it up in eclipse and go to the Ant window (Window -> Show View -> Ant) and click on "Run the Default Target"
> If you do not want to use Eclipse, just run "ant build.xml" > If you do not want to use Eclipse, just run "ant build.xml"
4. 4.
...@@ -14,16 +14,17 @@ ...@@ -14,16 +14,17 @@
## Updating mohawk.converter.generated.MohawkTARBAC.g4 (Using Eclipse) ## Updating mohawk.converter.generated.MohawkTARBAC.g4 (Using Eclipse)
1. Update the file mohawk.converter.generated.MohawkTARBAC.g4 and save (you can ignore if it auto compiles) 1. Update the file mohawk.converter.generated.MohawkTARBAC.g4 and save (you can ignore if it auto compiles)
2. In the ant window in eclipse run "mohawk_converter -> parser" (where mohawk_converter is the build.xml name) 2. In the ant window in eclipse run "mohawk_converter -> parser" (where mohawk_converter is the build.xml name)
3. Go to the project "mohawk_converter" (I called it 'Mohawk-T Conversion Tool') and "refresh it":<br/> 3. Go to the project "mohawk_converter" (I called it 'Mohawk-T Conversion Tool') and "refresh it":
> Right click on the project and click "Refresh" or click on the project and click 'F5' (the single key) <br/> > Right click on the project and click "Refresh" or click on the project and click 'F5' (the single key)
> This step is very important > This step is very important
4. Check for any errors that appear in the Java code located in mohawk.converter.generated.* 4. Check for any errors that appear in the Java code located in mohawk.converter.generated.*
5. Open up the JUnit window and run the tests associated with the mohawk conversion tool<br/> 5. Open up the JUnit window and run the tests associated with the mohawk conversion tool
> If you do not see mohawk.converter.testing.RegressionTests then find the Java file and right click it and go to "Run As" and click on "JUnit Test" > If you do not see mohawk.converter.testing.RegressionTests then find the Java file and right click it and go to "Run As" and click on "JUnit Test"
6. Repeat until all tests have past 6. Repeat until all tests have past
## Updating mohawk.converter.generated.MohawkTARBAC.g4 (Using Commandline) ## Updating mohawk.converter.generated.MohawkTARBAC.g4 (Using Commandline)
NOTE: the scripts are surrently only tested on windows, so some tweaking may have to be made (like replacing 'cmd' with 'bash') NOTE: the scripts are currently only tested on windows, so some tweaking may have to be made (like replacing 'cmd' with 'bash')
1. Update the file mohawk.converter.generated.MohawkTARBAC.g4 and save 1. Update the file mohawk.converter.generated.MohawkTARBAC.g4 and save
2. Run "ant build regression", check that the output is all correct (it builds the source code and then runs the JUnit tests) 2. Run "ant build regression", check that the output is all correct (it builds the source code and then runs the JUnit tests)
3. Repeat until done 3. Repeat until done
...@@ -34,10 +35,16 @@ NOTE: the scripts are surrently only tested on windows, so some tweaking may hav ...@@ -34,10 +35,16 @@ NOTE: the scripts are surrently only tested on windows, so some tweaking may hav
This is a weird bug with eclipse only, check the ANT build file first to make sure it can build the JAR file properly. This is a weird bug with eclipse only, check the ANT build file first to make sure it can build the JAR file properly.
To solve this problem: To solve this problem:
1. Right click the project -> Build Path -> Configure Build Path 1. Right click the project -> Build Path -> Configure Build Path
2. Go to the Libraries Tab 2. Go to the Libraries Tab
3. Click "Add Library" and then click on JUnit 3. Click "Add Library" and then click on JUnit
4. Make sure to install JUnit 4 or higher (I doubt a lower version would give you trouble, but JUnit 4 is what is being used to build the JAR file in the ANT script) 4. Make sure to install JUnit 4 or higher
> I doubt a lower version would give you trouble, but JUnit 4 is what is being used to build the JAR file in the ANT script
# Contact # Contact
Author: Jonathan Shahen <jonathan.shahen@gmail.com> Author: Jonathan Shahen <jonathan.shahen@gmail.com>
\ No newline at end of file
# Notes
* In markdown if you want to start a new line you must end the line with two or more spaces [BitBucket Issue - The text editor is losing line breaks](https://bitbucket.org/site/master/issue/7396/the-text-editor-is-losing-line-breaks)
* Eclipse cannot do nested lists, but Bitbucket can: [BitBucket Tutorial - Markdown Demo](https://bitbucket.org/tutorials/markdowndemo/overview#markdown-header-links)
\ No newline at end of file
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
<target name="parser" depends="init" description="generate parser files"> <target name="parser" depends="init" description="generate parser files">
<!-- Create the parser files --> <!-- Create the parser files -->
<!-- <!-- This uses an old version of ANTLR (something below 4)
<antlr target="${antlr-script}/mohawktarbac.g4" outputdirectory="${antlr-script}"> <antlr target="${antlr-script}/mohawktarbac.g4" outputdirectory="${antlr-script}">
<classpath> <classpath>
<pathelement location="${antlr}" /> <pathelement location="${antlr}" />
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
* *
* *
* The order of the document doesn't matter: Query can be last, first, or somewhere in the middle and same goes for all the others * The order of the document doesn't matter: Query can be last, first, or somewhere in the middle and same goes for all the others
*/ */
CanAssign { CanAssign {
// <Admin role, starting timeslot - end timeslot for admin role, role preconditions, [time slot rule gives role to user for, another time slot (optional)...],role to give to the user> // <Admin role, starting timeslot - end timeslot for admin role, role preconditions, [time slot rule gives role to user for, another time slot (optional)...],role to give to the user>
<role0,t0-t5,TRUE,[t1,t1],role1> //(1) <role0,t0-t5,TRUE,[t1,t1],role1> //(1)
...@@ -24,5 +24,8 @@ CanDisable { ...@@ -24,5 +24,8 @@ CanDisable {
// same as above // same as above
} }
// Expected solution: {TRUE, FALSE, UNKNOWN}; where for TRUE is means that we can achieve the Query
Expected: UNKNOWN
// Query: timeslot to check, [set of roles that the user must have in the timeslot (no NOTs allowed)] // Query: timeslot to check, [set of roles that the user must have in the timeslot (no NOTs allowed)]
Query: t0,[role1,role0,role2] Query: t0,[role1,role0,role2]
\ No newline at end of file
/* This test is to show that unique role names can be used, they must only contain [0-9a-zA-Z]+ /* This test is to show that unique role names can be used, they must only contain [0-9a-zA-Z]+
* *
* NOT~ cannot have a space between NOT and the tilde ~ * This shows that NOT can have white space between it and the tilde (~)
*/ */
CanAssign { CanAssign {
...@@ -14,12 +14,13 @@ CanRevoke { ...@@ -14,12 +14,13 @@ CanRevoke {
CanEnable { CanEnable {
<manager,t0-t5,TRUE,[t1,t1],employee> //(3) <manager,t0-t5,TRUE,[t1,t1],employee> //(3)
<officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(4) <officer,t0-t0,employee & NOT ~ manager & NOT ~badguy,[t1,t2],contractor> //(4)
} }
CanDisable { CanDisable {
<manager,t0-t5,TRUE,[t1,t1],employee> //(5) <manager,t0-t5,TRUE,[t1,t1],employee> //(5)
<officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(6) <officer,t0-t0,employee & NOT ~manager & NOT ~ badguy,[t1,t2],contractor> //(6)
} }
Query: t0,[officer,manager,employee] Query: t0,[officer,manager,employee]
\ No newline at end of file Expected: UNKNOWN
\ No newline at end of file
/* This test is to show that the order of the blocks does not matter /* This test is to show that the order of the blocks does not matter
*/ *
Query: t0,[officer,manager,employee] * This test shows that you can have all roles act as the administrator role
*/
Query : t0,[officer,manager,employee]
Expected : UNKNOWN
CanDisable { CanDisable {
<manager,t0-t5,TRUE,[t1,t1],employee> //(5) <manager,t0-t5,TRUE,[t1,t1],employee> //(1)
<officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(6) <officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(2)
} }
CanEnable { CanEnable {
...@@ -17,6 +20,7 @@ CanRevoke { ...@@ -17,6 +20,7 @@ CanRevoke {
} }
CanAssign { CanAssign {
<manager,t0-t5,TRUE,[t1,t1],employee> //(1) <manager,t0-t5,TRUE,[t1,t1],employee> //(5)
<officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(2) <officer,t0-t0,employee & NOT~ manager & NOT~ badguy,[t1,t2],contractor> //(6)
<TRUE,t0-t0,employee,[t1,t2],person> //(7)
} }
/* Taken from sharelatex's "Working Files/Mohawk Examples/old-simple-tests.txt"
*
* Converted simple_test1.txt into the new format
*/
CanAssign {
// <Admin role, starting timeslot - end timeslot for admin role, role preconditions, [time slot rule gives role to user for, another time slot (optional)...],role to give to the user>
<role0,t0-t0,TRUE,[t0],role1> //(1)
<role0,t0-t0,role1,[t0],role2> //(2)
}
CanRevoke {}
CanEnable {}
CanDisable {}
Query: t0,[role2]
Expected: TRUE
\ No newline at end of file
...@@ -23,7 +23,7 @@ import org.apache.commons.lang3.StringUtils; ...@@ -23,7 +23,7 @@ import org.apache.commons.lang3.StringUtils;
public class ConverterInstance { public class ConverterInstance {
private final String VERSION = "v0.0.1"; private final String VERSION = "v0.0.1";
// Logger Fields // Logger Fields
public final Logger logger = Logger.getLogger("mohawk-converter"); public static final Logger logger = Logger.getLogger("mohawk-converter");
private String Logger_filepath = "mohawk-converter.log"; private String Logger_filepath = "mohawk-converter.log";
private String Logger_folderpath = "logs"; private String Logger_folderpath = "logs";
private ConsoleHandler consoleHandler = new ConsoleHandler(); private ConsoleHandler consoleHandler = new ConsoleHandler();
...@@ -103,24 +103,13 @@ public class ConverterInstance { ...@@ -103,24 +103,13 @@ public class ConverterInstance {
.withDescription("Path to the RBAC Spec file or Folder if the 'bulk' option is set").hasArg() .withDescription("Path to the RBAC Spec file or Folder if the 'bulk' option is set").hasArg()
.create("rbacspec")); .create("rbacspec"));
options.addOption(OptionBuilder.withArgName("filepath")
.withDescription("Path to the NuSMV program file (defaults to 'NuSMV')").hasArg().create("nusmv"));
// Add Functional Options // Add Functional Options
options.addOption("bulk", false, "Use the folder that rbacspec points to and run against all *.spec"); options.addOption("bulk", false, "Use the folder that rbacspec points to and run against all *.spec");
options.addOption(OptionBuilder options.addOption("ranise", false, "Convert input SPEC file to Ranise's format");
.withArgName("bmc|smc|both") options.addOption("uzun", false, "Convert input SPEC file to Uzun's format");
.withDescription( options.addOption("mohawk", false, "Convert input SPEC file to Mohawk's RBAC format");
"Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'") options.addOption("all", false, "Convert input SPEC file to All formats");
.hasArg().create("mode"));
// Add Actionable Options
options.addOption(OptionBuilder
.withArgName("all|smv")
.withDescription(
"Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'")
.hasArg().create("run"));
} }
......
...@@ -22,6 +22,7 @@ import mohawk.converter.pieces.*; ...@@ -22,6 +22,7 @@ import mohawk.converter.pieces.*;
public boolean canenable_found = false; public boolean canenable_found = false;
public boolean candisable_found = false; public boolean candisable_found = false;
public boolean query_found = false; public boolean query_found = false;
public boolean expected_found = false;
int tabsize = 1; int tabsize = 1;
/* Global States */ /* Global States */
...@@ -35,6 +36,7 @@ import mohawk.converter.pieces.*; ...@@ -35,6 +36,7 @@ import mohawk.converter.pieces.*;
public CanDisable canDisable = new CanDisable(); public CanDisable canDisable = new CanDisable();
public Query query = new Query(); public Query query = new Query();
public ExpectedResult expectedResult;
private void logmsg(String msg) { private void logmsg(String msg) {
...@@ -44,7 +46,7 @@ import mohawk.converter.pieces.*; ...@@ -44,7 +46,7 @@ import mohawk.converter.pieces.*;
init init
: :
/*stat stat*/ stat stat stat stat stat stat stat stat stat stat stat
; ;
stat stat
...@@ -90,6 +92,12 @@ stat ...@@ -90,6 +92,12 @@ stat
query query
{query_found=true;} {query_found=true;}
|
{expected_found==false}?
expected
{expected_found=true;}
; ;
/* /*
...@@ -169,23 +177,53 @@ candisable ...@@ -169,23 +177,53 @@ candisable
query query
: :
Query Colon t=timeslot Comma ra=roleArray Query Colon t = timeslot Comma ra = roleArray
{ {
query._timeslot = $t.val; query._timeslot = $t.val;
query._roles = $ra.r; query._roles = $ra.r;
} }
;
expected
:
Expected Colon
(
True
{expectedResult = ExpectedResult.TRUE;}
| False
{expectedResult = ExpectedResult.FALSE;}
| Unknown
{expectedResult = ExpectedResult.UNKNOWN;}
)
; ;
myrule [RuleType rt] returns [Rule r] myrule [RuleType rt] returns [Rule r]
locals [Boolean adminAllRoles]
: :
{logmsg("Adding Rule: "); tabsize++;} {logmsg("Adding Rule: "); tabsize++;}
LeftAngle adminRole = myrole Comma ti = timeInteral Comma pc=precondition Comma LeftAngle
tsa=timeslotArray Comma role = myrole RightAngle (
adminRole = myrole
{$adminAllRoles=false;}
| True
{$adminAllRoles=true;}
) Comma ti = timeInteral Comma pc = precondition Comma tsa = timeslotArray
Comma role = myrole RightAngle
{ {
$r = new Rule(); $r = new Rule();
$r._type = rt; $r._type = rt;
$r._adminRole = $adminRole.role; if($adminAllRoles == true) {
$r._adminRole = mohawk.converter.pieces.Role.allRoles();
} else {
$r._adminRole = $adminRole.role;
}
$r._adminTimeSlots[0] = $ti.t0; $r._adminTimeSlots[0] = $ti.t0;
$r._adminTimeSlots[1] = $ti.t1; $r._adminTimeSlots[1] = $ti.t1;
$r._preconditions = $pc.p; $r._preconditions = $pc.p;
...@@ -209,7 +247,7 @@ precondition returns [ArrayList<Role> p] @init { ...@@ -209,7 +247,7 @@ precondition returns [ArrayList<Role> p] @init {
{$p.add($b.r);} {$p.add($b.r);}
)* )*
| 'TRUE' | True
; ;
rolecondition returns [Role r] @init { rolecondition returns [Role r] @init {
...@@ -217,13 +255,13 @@ rolecondition returns [Role r] @init { ...@@ -217,13 +255,13 @@ rolecondition returns [Role r] @init {
} }
: :
( (
Not not
{not = true;} {not = true;}
)? myrole )? myrole
{ {
$r = new Role($myrole.rolet, not); $r = new Role($myrole.rolet, not);
/*logmsg("Role: "+ $r);*/ /* logmsg("Role: "+ $r); */
} }
; ;
...@@ -287,8 +325,36 @@ myrole returns [String rolet, Role role] ...@@ -287,8 +325,36 @@ myrole returns [String rolet, Role role]
; ;
// Key Words not
:
Not '~'
;
/* Whitespace and Comments */
Whitespace
:
[ \t]+ -> skip
;
Newline
:
(
'\r' '\n'?
| '\n'
) -> skip
;
BlockComment
:
'/*' .*? '*/' -> skip
;
LineComment
:
'//' ~[\r\n]* -> skip
;
/* Key Words */
Timeslot Timeslot
: :
't' INT 't' INT
...@@ -330,12 +396,38 @@ Query ...@@ -330,12 +396,38 @@ Query
'Query' 'Query'
; ;
Expected
:
'Expected'
;
Not
:
'NOT'
;
True
:
'TRUE'
;
False
:
'FALSE'
;
Unknown
:
'UNKNOWN'
;
// Special Notation // Special Notation
/* /*
RoleStrict RoleStrict
: :
'role' INT 'role' INT
;*/ ;
*/
Role Role
: :
[A-Za-z0-9]+ [A-Za-z0-9]+
...@@ -378,11 +470,6 @@ AND ...@@ -378,11 +470,6 @@ AND
'&' '&'
; ;
Not
:
'NOT~'
;
Colon Colon
: :
':' ':'
...@@ -402,28 +489,4 @@ DIGIT ...@@ -402,28 +489,4 @@ DIGIT
INT INT
: :
DIGIT+ DIGIT+
;
/*Whitespace and Comments*/
Whitespace
:
[ \t]+ -> skip
;
Newline
:
(
'\r' '\n'?
| '\n'
) -> skip
;
BlockComment
:
'/*' .*? '*/' -> skip
;
LineComment
:
'//' ~[\r\n]* -> skip
; ;
\ No newline at end of file
...@@ -10,12 +10,18 @@ public class MohawkTiming { ...@@ -10,12 +10,18 @@ public class MohawkTiming {
return timings; return timings;
} }
public void blankTimer(String key) {
timings.put(key, null);
}
public void startTimer(String key) { public void startTimer(String key) {
timings.put(key, System.currentTimeMillis()); timings.put(key, System.currentTimeMillis());
} }
public void stopTimer(String key) { public void stopTimer(String key) {
timings.put(key, System.currentTimeMillis() - (Long) timings.get(key)); if (timings.get(key) != null) {
timings.put(key, System.currentTimeMillis() - (Long) timings.get(key));
}
} }
/** /**
...@@ -47,6 +53,5 @@ public class MohawkTiming { ...@@ -47,6 +53,5 @@ public class MohawkTiming {
} }
} }
return t.toString(); return t.toString();
} }
} }
package mohawk.converter.pieces;
public enum ExpectedResult {
TRUE("Query Reachable"), FALSE("Query Unreachable"), UNKNOWN("Unknown");
private String _str;
ExpectedResult(String str) {
_str = str;
}
@Override
public String toString() {
return "Expected Result: " + _str;
}
}
...@@ -3,6 +3,7 @@ package mohawk.converter.pieces; ...@@ -3,6 +3,7 @@ package mohawk.converter.pieces;
public class Role { public class Role {
public String _name; public String _name;
public Boolean _not; public Boolean _not;
private Boolean _allRoles = false;
public Role(String name, Boolean not) {