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.

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).
If a breach is found VAC produces a counter-example of the
original policy showing how user *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.

*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.

- VAC source code
(2015.10.12)

- VAC binaries for Linux_32bit,
Linux_64bit
(2015.10.12)

- 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 usercan reach role*u**r*

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.

The results of our experiments are reported in the tables below.

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 | 13 |
37 |
1093 |
H1 |
4 |
5 |
7 |
0.015s |
H1 |
0.114s |
N |
H1 |
0.032s |
N |
H1 |
0.016s |
N |
H1 |
0.114s |
N |
H1 |
2.468s |
N |
H1 |
0.032s |
N |
H1 |
0.016s |
N |
N |
0.032s |

Hospital | 13 |
37 |
1092 |
H2 |
4 |
5 |
7 |
0.015s |
H2 |
0.114s |
N |
H2 |
0.032s |
N |
H2 |
0.016s |
N |
H2 |
0.114s |
N |
H2 |
2.418s |
N |
H2 |
0.032s |
N |
H2 |
0.016s |
N |
N |
0.032s |

Hospital |
13 |
37 |
1092 |
H3 |
3 |
2 |
5 |
0.015s |
H3 |
0.114s |
R |
H3 |
0.007s |
R |
H3 |
0.016s |
R |
H3 |
0.164s |
R |
H3 |
1.867s |
R |
H3 |
0.016s |
R |
H3 |
0.007s |
U |
R |
0.114s |

Hospital |
13 |
37 |
1092 |
H4 |
4 |
4 |
4 |
0.015s |
H4 |
0.114s |
R |
H4 |
0.016s |
R |
H4 |
0.032s |
R |
H4 |
0.264s |
R |
H4 |
2.586s |
R |
H4 |
0.064s |
R |
H4 |
0.016s |
U |
R |
0.164s |

University | 32 |
449 |
943 |
U1 |
7 |
15 |
13 |
0.016s |
U1 |
0.264s |
N |
U1 |
14.23s |
N |
U1 |
0.364s |
N |
U1 |
1.015s |
N |
U1 |
7.777s |
N |
U1 |
0.364s |
N |
U1 |
0.032s |
N |
N |
0.064s |

University | 32 |
449 |
943 |
U2 |
7 |
16 |
13 |
0.016s |
U2 |
0.264s |
R |
U2 |
1.265s |
R |
U2 |
38.38s |
R |
U2 |
0.715s |
R |
U2 |
5.523s |
R |
U2 |
0.114s |
R |
U2 |
0.032s |
U |
R |
0.314s |

University | 32 |
449 |
943 |
U3 |
9 |
25 |
23 |
0.016s |
U3 |
0.564s |
N |
U3 |
405.3s |
E |
U3 |
5.623s |
N |
U3 |
1.916s |
N |
U3 |
9.603s |
N |
U3 |
0.665s |
N |
U3 |
0.032s |
N |
N |
0.064s |

University | 32 |
449 |
943 |
U4 |
13 |
70 |
36 |
0.016s |
U4 |
3.219s |
R |
U4 |
- |
U |
U4 |
- |
U |
U4 |
620.5s |
R |
U4 |
236.6s |
R |
U4 |
11.13s |
R |
U4 |
0.114s |
U |
R |
3.719s |

Bank | 531 |
5126 |
2000 |
B1 |
2 |
0 |
2 |
0.264s |
B1 |
0.114s |
N |
B1 |
0.003s |
N |
B1 |
0.008s |
N |
B1 |
0.064s |
N |
B1 |
1.366s |
N |
B1 |
0.007s |
N |
B1 |
0.007s |
N |
N |
0.264s |

Bank | 531 |
5126 |
2000 |
B2 |
2 |
0 |
2 |
0.264s |
B2 |
0.114s |
N |
B2 |
0.003s | N |
B2 |
0.008s |
N |
B2 |
0.064s |
N |
B2 |
1.366s |
N |
B2 |
0.008s |
N |
B2 |
0.007s |
N |
N |
0.264s |

Bank | 531 |
5126 |
2000 |
B3 |
3 |
2 |
2 |
0.264s |
B3 |
0.114s |
R |
B3 |
0.007s | R |
B3 |
0.015s |
R |
B3 |
0.164s |
R |
B3 |
2.017s |
R |
B3 |
0.032s |
R |
B3 |
0.007s |
U |
R |
0.414s |

Bank | 531 |
5126 |
2000 |
B4 |
6 |
5 |
2 |
0.114s |
B4 |
0.114s |
R |
B4 |
0.032s | R |
B4 |
0.032s |
R |
B4 |
0.314s |
R |
B4 |
2.868s |
R |
B4 |
0.164s |
R |
B4 |
0.016s | U |
R |
0.264s |

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) |
||||||||||||||||||

#roles |
#users |
#rules |
File |
#roles |
#users |
#rules |
Answer |
Time |
#roles |
#users |
#rules |
File |
#roles |
#users |
#rules |
Answer |
Time |
#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 |

Role Reachability checkers for ARBAC systems

- 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)