VAC -- Verifier Access Control

VAC is an efficient automatic tool for the analysis of Administrative Role Based Access Control (ARBAC) policies. Given an ARBAC policy, a user u and a role target, VAC checks whether u can obtain role target in any reachable configuration of the system (role-reachability problem). Several security requirements‑including escalation of privileges and conflict-of-interest properties‑can be automatically reduced to the role-reachability problem. Therefore, VAC enables policy designers and system administrators to check whether their policies meet the security requirements.

Architecture

The architecture of VAC is shown below. Given an ARBAC policy,

VAC first uses an aggressive pruning aiming at reducing roles, administrative roles, rules, and users while preserving the reachability of role target.
VAC then translates the reduced ARBAC policy into programs meant to simulate the evolution of the system, and several model checkers can be used for the analysis. VAC provides two kinds of translation:

Precise transformer: The obtained program faithfully simulates the reduced policy, and VAC supports several backends for the analysis. VAC can translate policies into

C programs which are analyzed by the C bounded model-checker CBMC (under-approximate analysis, useful to find security breaches).

Horn programs. VAC supports the following fixed point engines for the analysis: Eldarica, HSF, and µZ. This approach leads to complete analysis.
Boolean programs. VAC supports three model checkers for Boolean programs Getafix, Moped, and NuSMV. This approach also provides complete analysis.

Abstract transformer: 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 resulting programs in order to prove the policies secure. VAC uses Interproc for the analysis with box domain. If no error is found it is guaranteed that the target role is not reachable in the original policy as well. Otherwise, it is UNKNOWN whether it is also reachable in the original policy. This approach is in general more efficient for proving correctness than the precise approach.

VAC allows to select the backend for the analysis by setting the appropriate options. By default, VAC uses first the abstract approach looking for the absence of a breach. In the negative case, it uses bounded model checking (CBMC with unwind set to 2) on the precise translation seeking for errors. If an error is found a counter-example is provided. Otherwise, VAC runs µZ for complete analysis.

Structure

VAC architecture

Papers

Details on the verification approaches can be found in these papers:

Abstract transformer
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.
Aggressive pruning
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.
Tool description
VAC - Verifier of Administrative Role-based Access Control Policies by Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, and Gennaro Parlato.
26th Int'l Conference on Computer Aided Verification (CAV). Vienna, Austria, 2014.

Download

VAC source code (2015.10.12)
VAC binaries for Linux_32bit, Linux_64bit (2015.10.12)

Features

Role reachability check

For any user
For a specific user

Support of unbounded number of users
VAC input format, examples: sample1, sample2, sample3

ROLES - list of ALL roles
USERS - list of users
NEWUSERS - list of types of new users
UA - list of initial user-role assignments
CR - list of can-revoke rules
CA - list of can-assign rules
SPEC - role reachability query

SPEC r - checks whether any user can reach role r
SPEC u r - checks whether a specific user u can reach role r

Experiments

VAC is evaluated on several benchmarks from the literature:

a hospital and a university policy;
a policy modeling a bank comprising several branches;
three sets of complex test suites capturing the complexity of realistic systems.

All experiments were performed on a machine running Ubuntu 14.04 LTS 64 bit with an Intel i7-3770 CPU and 16 GB of Ram.
The results of our experiments are reported in the tables below.

University, Hospital, and Bank Benchmarks

ARBAC Benchmarks

PRECISE TRANSFORMER

ABSTRACT TRANSFORMER

VAC
(default option)

ARBAC Policies

After Pruning

CBMC
(with --unwind 2
--no-unwinding-assertions
options)

MOPED
(Moped with -b
option)

NuSMV
(Default option)

HSF
(Default option)

ELDARICA
(-horn -hin -princess -bup
options)

Z3
(with -smt2
option)

INTERPROC
(-domain box
options)

Name

#roles

#rules

#users

File

#roles

#rules

#users

Time

File

Time

Answer

File

Time

Answer

File

Time

Answer

File

Time

Answer

File

Time

Answer

File

Time

Answer

File

Time

Answer

Answer
(Counter Example)

Time

Hospital

1093

0.015s

0.114s

0.032s

0.016s

0.114s

2.468s

0.032s

0.016s

0.032s

Hospital

1092

0.015s

0.114s

0.032s

0.016s

0.114s

2.418s

0.032s

0.016s

0.032s

Hospital

1092

0.015s

0.114s

0.007s

0.016s

0.164s

1.867s

0.016s

0.007s

0.114s

Hospital

1092

0.015s

0.114s

0.016s

0.032s

0.264s

2.586s

0.064s

0.016s

0.164s

University

449

943

0.016s

0.264s

14.23s

0.364s

1.015s

7.777s

0.364s

0.032s

0.064s

University

449

943

0.016s

0.264s

1.265s

38.38s

0.715s

5.523s

0.114s

0.032s

0.314s

University

449

943

0.016s

0.564s

405.3s

5.623s

1.916s

9.603s

0.665s

0.032s

0.064s

University

449

943

0.016s

3.219s

620.5s

236.6s

11.13s

0.114s

3.719s

Bank

531

5126

2000

0.264s

0.114s

0.003s

0.008s

0.064s

1.366s

0.007s

0.264s

Bank

531

5126

2000

0.264s

0.114s

0.003s

0.008s

0.064s

1.366s

0.008s

0.007s

0.264s

Bank

531

5126

2000

0.264s

0.114s

0.007s

0.015s

0.164s

2.017s

0.032s

0.007s

0.414s

Bank

531

5126

2000

0.114s

0.032s

0.314s

2.868s

0.164s

0.016s

0.264s

Complex Benchmarks

Testsuite 1										Testsuite 2										Testsuite 3
Name	Before			After Pruning				VAC (default option)		Test Name	Before			After Pruning				VAC (default option)		Test Name	Before			After Pruning				VAC (default option)
Name	#roles	#users	#rules	File	#roles	#users	#rules	Answer	Time	Test Name	#roles	#users	#rules	File	#roles	#users	#rules	Answer	Time	Test Name	#roles	#users	#rules	File	#roles	#users	#rules	Answer	Time
test1	4	5	9	M1R	3	2	5	R	0.114s	test1	4	2	8	M1R	4	2	5	R	0.114s	test1	4	5	11	M1R	2	2	1	R	0.114s
test2	6	10	22	M2R	4	2	2	R	0.114s	test2	6	2	19	M2R	4	2	2	R	0.114s	test2	6	10	20	M2R	2	2	1	R	0.114s
test3	21	50	88	M3R	12	3	32	R	0.314s	test3	27	2	75	M3R	12	2	26	R	0.264s	test3	21	50	89	M3R	3	4	2	R	0.114s
test4	41	100	176	M4R	4	4	2	R	0.114s	test4	41	2	154	M4R	4	2	2	R	0.114s	test4	41	100	178	M4R	2	2	1	R	0.114s
test5	201	500	872	M5R	2	2	1	R	0.114s	test5	199	2	736	M5R	2	2	1	R	0.114s	test5	201	500	880	M5R	2	2	1	R	0.114s
test6	501	1000	2201	M6R	3	2	2	R	0.114s	test6	499	2	1885	M6R	3	2	2	R	0.114s	test6	501	1000	2180	M6R	3	2	2	R	0.164s
test7	4001	10000	17536	M7R	2	2	1	R	0.314s	test7	3955	2	14857	M7R	2	2	1	R	0.214s	test7	4001	10000	17686	M7R	4	2	3	R	0.314s
test8	20000	50000	81210	M8R	2	2	1	R	1.015s	test8	19749	2	74324	M8R	2	2	1	R	0.715s	test8	20000	50000	83561	M8R	3	2	2	R	1.065s
test9	30000	70000	127713	M9R	2	2	1	R	1.561s	test9	29677	2	111800	M9R	2	2	1	R	1.065s	test9	30000	70000	125520	M9R	2	2	1	R	1.561s
test10	40001	100000	176062	M10R	2	2	1	R	1.917s	test10	39573	2	149156	M10R	2	2	1	R	1.316s	test10	40001	100000	176796	M10R	4	2	3	R	2.017s

Note: 'R' stands for Reachable, 'N' stands for Not reachable, 'U' stands for unknown (unknown whether it is reachable), 'E' stands for tool internal error, and '-' stands for timeout of 20 minutes.

External Links

Role Reachability checkers for ARBAC systems

ASASP

Mohawk

People

Anna Lisa Ferrara (U. of Bristol, UK)
P. Madhusudan (U. of Illinois, USA)
Truc Nguyen Lam (U. of Southampton, UK)
Gennaro Parlato (U. of Southampton, UK)

Verifier of Access Control