VAC -- Verifier Access Control

VAC is a tool to verify security of Administrative Role Based Access Control (ARBAC) policies. Given an ARBAC policy, a user u and a role r , the analysis tool can check whether the user u can obtain the role r sometime in the future, following the ARBAC policy. Several other security questions, including escalation of privileges, conflict-of-interest exclusion properties can be verified as well. The tool hence enables a security engineer crafting or changing an ARBAC system to determine the security properties of the system, and whether it achieves the policy goals. A salient aspect of the tool is that, since it works using abstraction techniques, it can handle security questions in a setting that considers an unbounded number of users that can be included dynamically into the system, independent of the number of users in the initial configuration.

VAC uses a combination of abstraction and reduction to program verification in order to perform the security analysis. VAC converts ARBAC policies to imperative programs that simulate the policy abstractly, and then utilizes further abstract-interpretation techniques from program analysis to analyze the programs in order to prove the policies secure.

Specifically, given an ARBAC system:

VAC first executes the ReduceAdmin algorithm to reduce the number of roles and rules of the system, if possible.
VAC then translates the reduced ARBAC system into a program that simulates the evolution of the system. There are two kinds of translations: precise transformer and abstract transformer
Finally, VAC uses model checkers to perform analysis, and checks whether the program can reach a particular program location. Using this, it infers whether it is impossible for the user to reach the role, hence proving security of the ARBAC system.

More details on VAC can be found in these papers:

Security Analysis of Access Control through Program Verification by Anna Lisa Ferrara, P. Madhusudan, and Gennaro Parlato.
25th IEEE Computer Security Foundations Symposium (CSF).Cambridge MA, USA, 2012.
Policy Analysis for Self-Administrated Role-based Access Control by Anna Lisa Ferrara, P. Madhusudan, and Gennaro Parlato.
19th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome, Italy, 2013.

VAC tool can be downloaded here:

VAC toolchain (New C Version)
VAC prototype tool (Old Java Version)

Benchmark Policies, Security Questions and Programs Instrumented for Analyzer Tools

REDUCEADMIN									PRECISE TRANSFORMER																ABSTRACT TRANSFORMER
Policy Suite				After Simplify Suite					INTERPROC			BLAST			GET-A-FIX			Z3			HSF			Query Answer	INTERPROC			BLAST			GET-A-FIX			Z3			HSF			Query Answer
Name	#roles	#rules	#users	File	#roles	#rules	#users	Time	File	Time	Answer	File	Time	Answer	File	Time	Answer	File	Time	Answer	File	Time	Answer	Query Answer	File	Time	Answer	File	Time	Answer	File	Time	Answer	File	Time	Answer	File	Time	Answer	Query Answer
Hospital1	15	32	8	H1	7	12	9	0.004s	H1	1.65s	N	H1	-	-	H1	1m7s	N	H1	6.26s	N	H1	1.61s	N	-	H1	0.12s	N	H1	-	-	H1	0.01s	N	H1	0.3s	N	H1	0.2s	N	N
Hospital2	15	32	8	H2	5	8	8	0.004s	H2	0.67s	N	H2	-	-	H2	0.91s	N	H2	2.1s	N	H2	0.63s	N	-	H2	0.06s	N	H2	0.22s	N	H2	0.00s	N	H2	0.17s	N	H2	0.12s	N	N
Hospital3	15	38	1093	H3	4	5	5	0.024s	H3	0.19s	R	H3	1.61s	R	H3	0.00s	R	H3	0.56s	R	H3	0.17s	R	R	H3	0.02s	U	H3	0.14s	U	H3	0.00s	U	H3	0.07s	U	H3	0.07s	U	U
University1	34	136	10	U1	10	20	11	0.004s	U1	7.96s	N	U1	-	-	U1	-	-	U1	53s	N	U1	6m4s	N	-	U1	0.5s	N	U1	-	-	U1	0.3s	N	U1	1.17s	N	U1	0.64s	N	N
University2	34	136	10	U2	2	0	3	0.003s	U2	0.02s	N	U2	0.02s	N	U2	0.00s	N	U2	0.09s	N	U2	0.09s	N	N	U2	0.01s	N	U2	0.01s	N	U2	0.00s	N	U2	0.04s	N	U2	0.08s	N	N
University3	34	136	10	U3	15	33	11	0.004s	U3	15.6s	N	U3	-	-	U3	-	-	U3	-	-	U3	2m40s	N	-	U3	1.05s	N	U3	-	-	U3	16.12s	N	U3	2.71s	N	U3	52.64s	N	N
University4	34	136	10	U4	2	1	3	0.004s	U4	0.03s	R	U4	0.2s	R	U4	0.07s	R	U4	0.07s	R	U4	0.09s	R	R	U4	0.2s	U	U4	0.01s	U	U4	0.00s	U	U4	0.04s	U	U4	0.07s	U	U
University5	34	455	944	U5	8	14	18	0.020s	U5	3.01s	N	U5	-	-	U5	-	-	U5	11s	N	U5	2.69s	N	-	U5	0.1s	N	U5	36.2s	N	U5	0.00s	N	U5	0.55s	N	U5	0.27s	N	N
University6	34	457	944	U6	8	15	18	0.040s	U6	3.12s	N	U6	-	-	U6	0.35s	N	U6	9.36s	N	U6	4.32s	N	-	U6	0.09s	N	U6	19.19s	N	U6	0.00s	N	U6	0.44s	N	U6	0.28s	N	N
University7	34	455	944	U7	6	8	13	0.035s	U7	0.54s	N	U7	-	-	U7	0.14s	N	U7	2.18s	N	U7	0.85s	N	-	U7	0.06s	N	U7	3.76s	N	U7	0.00s	N	U7	0.2s	N	U7	0.12s	N	N
University8	34	455	944	U8	14	62	47	0.024s	U8	25.14s	R	U8	-	-	U8	4m25s	R	U8	-	-	U8	151m4s	R	-	U8	0.44s	U	U8	-	-	U8	0.03s	U	U8	2.75s	U	U8	17.59s	U	U
Bank1	36	514	1	B1	2	0	2	0.024s	B1	0.03s	N	B1	0.02s	N	B1	0.00s	N	B1	0.06s	N	B1	0.08s	N	N	B1	0.01s	N	B1	0.01s	N	B1	0.00s	N	B1	0.08s	N	B1	0.07s	N	N
Bank2	70	1029	1	B2	2	0	2	0.036s	B2	0.02s	N	B2	0.04s	N	B2	0.00s	N	B2	0.07s	N	B2	0.08s	N	N	B2	0.01s	N	B2	0.01s	N	B2	0.00s	N	B2	0.05s	N	B2	0.08s	N	N
Bank3	104	1544	1	B3	2	0	2	0.072s	B3	0.02s	N	B3	0.04s	N	B3	0.00s	N	B3	0.09s	N	B3	0.07s	N	N	B3	0.01s	N	B3	0.01s	N	B3	0.00s	N	B3	0.04s	N	B3	0.08s	N	N
Bank4	138	2058	1	B4	2	0	2	0.084s	B4	0.02s	N	B4	0.03s	N	B4	0.00s	N	B4	0.09s	N	B4	0.08s	N	N	B4	0.01s	N	B4	0.01s	N	B4	0.00s	N	B4	0.06s	N	B4	0.08s	N	N
Bank5	71	1029	1	B5	2	0	2	0.048s	B5	0.01s	N	B5	0.02s	N	B5	0.00s	N	B5	0.09s	N	B5	0.08s	N	N	B5	0.01s	N	B5	0.01s	N	B5	0.00s	N	B5	0.06s	N	B5	0.08s	N	N
Bank6	105	1543	1	B6	2	0	2	0.076s	B6	0.02s	N	B6	0.04s	N	B6	0.00s	N	B6	0.09s	N	B6	0.08s	N	N	B6	0.01s	N	B6	0.01s	N	B6	0.00s	N	B6	0.04s	N	B6	0.08s	N	N
Bank7	139	2057	1	B7	2	0	2	0.112s	B7	0.02s	N	B7	0.03s	N	B7	0.00s	N	B7	0.08s	N	B7	0.07s	N	N	B7	0.01s	N	B7	0.01s	N	B7	0.00s	N	B7	0.06s	N	B7	0.08s	N	N

Note: R means Reachable, N means Not reachable and U means unknown (do not know whether reachable or not), - means timeout.

Benchmark of Reduce Admin tool

Mixed Testsuite									Mixednocr Testsuite									Positive Testsuite
Name	Before			After				Time	Name	Before			After				Time	Name	Before			After				Time
Name	#roles	#users	#rules	File	#roles	#users	#rules	Time	Name	#roles	#users	#rules	File	#roles	#users	#rules	Time	Name	#roles	#users	#rules	File	#roles	#users	#rules	Time
Mohawk1	4	5	9	M1R	4	3	5	0.000s	Mohawk1	4	2	8	M1R	4	3	5	0.000s	Mohawk1	4	5	11	M1R	2	3	1	0.000s
Mohawk2	6	10	22	M2R	2	3	1	0.000s	Mohawk2	6	2	19	M2R	2	3	1	0.000s	Mohawk2	6	10	20	M2R	2	3	2	0.000s
Mohawk3	21	50	88	M3R	15	3	43	0.000s	Mohawk3	27	2	75	M3R	17	3	48	0.000s	Mohawk3	21	50	89	M3R	2	3	2	0.000s
Mohawk4	41	100	176	M4R	2	3	1	0.000s	Mohawk4	41	2	154	M4R	6	3	7	0.000s	Mohawk4	41	100	178	M4R	2	3	2	0.000s
Mohawk5	201	500	872	M5R	2	3	2	0.020s	Mohawk5	199	2	736	M5R	2	3	1	0.020s	Mohawk5	201	500	880	M5R	2	3	2	0.020s
Mohawk6	501	1000	2201	M6R	2	3	1	0.110s	Mohawk6	499	2	1885	M6R	2	3	1	0.100s	Mohawk6	501	1000	2180	M6R	2	3	2	0.090s
Mohawk7	4001	10000	17536	M7R	2	3	2	5.710s	Mohawk7	3955	2	14857	M7R	2	3	1	5.760s	Mohawk7	4001	10000	17686	M7R	2	3	1	5.340s
Mohawk8	20000	50000	81210	M8R	2	3	1	2m41s	Mohawk8	19749	2	74324	M8R	2	3	1	2m34s	Mohawk8	20000	50000	83561	M8R	2	3	1	2m26s
Mohawk9	30000	70000	127713	M9R	2	3	1	6m37s	Mohawk9	29677	2	111800	M9R	2	3	1	6m19s	Mohawk9	30000	70000	125520	M9R	2	3	1	6m9s
Mohawk10	40001	100000	176062	M10R	2	3	1	15m45s	Mohawk10	39573	2	149156	M10R	2	3	1	18m55s	Mohawk10	40001	100000	176796	M10R	2	3	2	12m18s

Contacts
VAC has been devoloped by Anna Lisa Ferrara (U. of Bristol, UK), P. Madhusudan (U. of Illinois, USA), Gennaro Parlato (U. of Southampton, UK), and Truc Nguyen Lam (student at U. of Southampton, UK),

Verifier of Access Control