ARBAC role reachability verifier.
Administrative Role Based Access Control (ARBAC) role reachability verifier.
Role reachability is one of the most useful problem to solve for the security verification of ARBAC.
Informally, the ARBAC role reachability problem amounts to checking whether the goal role can be assigned to some user of the system after a number of steps, starting from a certain user-to-role assignment and applying the rules in the ARBAC policy.
This program parses the specification of an ARBAC role reachability problem and returns its solution (true or false). It is meant to analyse small ARBAC policies, and it's not adapt to be used with larger ones. Note that the role reachability problem is PSPACE-complete. This project uses some pruning algorithms (forward slicing, backward slicing, and a combination of both) to simplify the input ARBAC role reachability problem, but pruning it's not sufficient to obtain satisfactory running times for complex policies.
This project was developed for the "Security 2" course of the Computer Science master degree programme of Ca' Foscari University of Venice.
- Python (version >= 3.8)
- A python virtualenv (optional, but recommended)
- Clone the repository:
git clone https://github.com/jackroi/ARBAC-analyser
cd ARBAC-analyser
- Install required packages:
pip3 install -r requirements.txt
python3 arbac-analyser.py [policy.arbac]
python3 arbac-analyser.py ./policies/policy1.arbac
cat ./policies/policy1.arbac | python3 arbac-analyser.py
- Lark - Parsing toolkit
- @jackroi - Implementation
- "Security 2" course professor for the project idea and specifications.