VAC -- Verifier Access Control

VAC -- Verifier Access Control
Verifier of 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
and a role
target
VAC checks whether
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).
If a breach is found VAC produces a counter-example of the
original policy showing how user
can indeed
acquire the given target role.
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)
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
SPEC u r
- checks whether a specific user
can reach role
Experiments
VAC is evaluated on several benchmarks from the literature:
hospital and a university policy
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
13
37
1093
H1
0.015s
H1
0.114s
H1
0.032s
H1
0.016s
H1
0.114s
H1
2.468s
H1
0.032s
H1
0.016s
0.032s
Hospital
13
37
1092
H2
0.015s
H2
0.114s
H2
0.032s
H2
0.016s
H2
0.114s
H2
2.418s
H2
0.032s
H2
0.016s
0.032s
Hospital
13
37
1092
H3
0.015s
H3
0.114s
H3
0.007s
H3
0.016s
H3
0.164s
H3
1.867s
H3
0.016s
H3
0.007s
0.114s
Hospital
13
37
1092
H4
0.015s
H4
0.114s
H4
0.016s
H4
0.032s
H4
0.264s
H4
2.586s
H4
0.064s
H4
0.016s
0.164s
University
32
449
943
U1
15
13
0.016s
U1
0.264s
U1
14.23s
U1
0.364s
U1
1.015s
U1
7.777s
U1
0.364s
U1
0.032s
0.064s
University
32
449
943
U2
16
13
0.016s
U2
0.264s
U2
1.265s
U2
38.38s
U2
0.715s
U2
5.523s
U2
0.114s
U2
0.032s
0.314s
University
32
449
943
U3
25
23
0.016s
U3
0.564s
U3
405.3s
U3
5.623s
U3
1.916s
U3
9.603s
U3
0.665s
U3
0.032s
0.064s
University
32
449
943
U4
13
70
36
0.016s
U4
3.219s
U4
U4
U4
620.5s
U4
236.6s
U4
11.13s
U4
0.114s
3.719s
Bank
531
5126
2000
B1
0.264s
B1
0.114s
B1
0.003s
B1
0.008s
B1
0.064s
B1
1.366s
B1
0.007s
B1
0.007s
0.264s
Bank
531
5126
2000
B2
0.264s
B2
0.114s
B2
0.003s
B2
0.008s
B2
0.064s
B2
1.366s
B2
0.008s
B2
0.007s
0.264s
Bank
531
5126
2000
B3
0.264s
B3
0.114s
B3
0.007s
B3
0.015s
B3
0.164s
B3
2.017s
B3
0.032s
B3
0.007s
0.414s
Bank
531
5126
2000
B4
0.114s
B4
0.114s
B4
0.032s
B4
0.032s
B4
0.314s
B4
2.868s
B4
0.164s
B4
0.016s
0.264s
Complex
Benchmarks
Testsuite

Testsuite

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
M1R
0.114s
test1
M1R
0.114s
test1
11
M1R
0.114s
test2
10
22
M2R
0.114s
test2
19
M2R
0.114s
test2
10
20
M2R
0.114s
test3
21
50
88
M3R
12
32
0.314s
test3
27
75
M3R
12
26
0.264s
test3
21
50
89
M3R
0.114s
test4
41
100
176
M4R
0.114s
test4
41
154
M4R
0.114s
test4
41
100
178
M4R
0.114s
test5
201
500
872
M5R
0.114s
test5
199
736
M5R
0.114s
test5
201
500
880
M5R
0.114s
test6
501
1000
2201
M6R
0.114s
test6
499
1885
M6R
0.114s
test6
501
1000
2180
M6R
0.164s
test7
4001
10000
17536
M7R
0.314s
test7
3955
14857
M7R
0.214s
test7
4001
10000
17686
M7R
0.314s
test8
20000
50000
81210
M8R
1.015s
test8
19749
74324
M8R
0.715s
test8
20000
50000
83561
M8R
1.065s
test9
30000
70000
127713
M9R
1.561s
test9
29677
111800
M9R
1.065s
test9
30000
70000
125520
M9R
1.561s
test10
40001
100000
176062
M10R
1.917s
test10
39573
149156
M10R
1.316s
test10
40001
100000
176796
M10R
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
Peopl
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)