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



Download

Features

Experiments

VAC is evaluated on several benchmarks from the literature: 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 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
361
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


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

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


People