Automated Symbolic Analysis of Security Policies
[ Content | Overview | The Tool: ASASP | Benchmarks | Related Tools ]
Content
This page contains information about the prototype tool ASASP (short for Automated Symbolic Analysis of Security Policies), used for the experimental evaluation of the following papers:
- [AAR11b] F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Security Policies. In Proc. of the 23rd Conference on Automated Deduction (CADE), 2011. To appear in LNCS.
- [AAR11a] F. Alberti, A. Armando, and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies. In Proc. of ASIACCS 2011 , 6th ACM Symposium on Information, Computer and Communications Security, March 22-24, 2011 (Hong Kong).
A companion paper presenting more of the formal framework underlying ASASP is the following:
- [AR10] A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proc. of 6th Int. Workshop on Security and Trust Management, STM'10, Athens, September 23-24, 2010.
Overview
Automated techniques for the security analysis of Role-Based Access Control (RBAC) access control policies are crucial for their design and maintenance. The definition of administrative domains by means of attributes attached to users makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains.
In [AAR11], we describe an automated symbolic security analysis technique for administrative attribute-based RBAC policies. A class of formulae of first-order logic is used as an adequate symbolic representation for the policies and their administrative actions. State-of-the-art automated theorem proving techniques are used (off-the-shelf) to mechanize the security analysis procedure. Besides discussing the assumptions for the effectiveness and termination of the procedure, we demonstrate its efficiency through an extensive empirical evaluation.
In [AR10], we describe the symbolic framework underlying [AAR11] restricted to the case of standard ARBAC and give preliminary experimental evidence of the scalability of our approach.
The tool: ASASP
ASASP is an implementation of the analysis techniques for administrative RBAC policies described in [AR10,AAR11]. It implements a symbolic backward reachability analysis to solve user-role reachability problems, i.e. it is capable of establishing if there exists a coalition of administrators capable of giving a certain set of priviliges to a certain (untrusted) user.
ASASP is based on a client-server architecture.
- The client performs the symbolic manipulations required to compute the pre-images of a set of RBAC policies with respect to two kinds of administrative actions: assignments and revocations of roles to users.
- The server solves logical problems implying that a fix-point has been reached or that there exists a sequence of administrative actions leading from an initial RBAC policy to a policy where the given (untrusted) user has been assigned a certain set of roles.
In order to exploit the cornucopia of available well-engineered theorem proving techniques, ASASP invokes an external tool. So, before being able to run ASASP, you need to install on your machine at least one (better all, as ASASP can use them in combination) of the following provers:
After installing these tools and making sure you have a standard C compiler on your machine, follow these steps:
- Download and save the zip file containing the source code
- unzip it
- cd to the folder created at step 2
- run 'make'
- move the executables of the previously installed provers to the bin/ directory in the folder and make sure they have executable permissions
At this point you should be able to run the tool for example on one of the problems included in the set of benchmarks described below. If something went wrong, please, do not hesitate to contact Silvio Ranise (ranise 'at' fbk 'dot' eu). I will be happy to help you.
Before donwloading the tool, please, read the following disclaimer...
BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WAARANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WAARANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WAARANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.
Benchmarks
In [AAR11], we used three classes of benchmarks:
- Class (a): problems from the paper Efficient Policy Analysis for ARBAC by Stoller, Yang, Ramakrishnan, and Gofman (instances of ARBAC without role hierarchies)
- Class (b): problems from class (a) extended with randomly generated role hierarchies
- Class (c): problems from class (b) extended with administrative scopes defined by roles and user attributes
Each zip file contains a brief description of the syntax and the semantics of the class of problems.
Should you have any questions or feedback, please, do not hesitate to contact Silvio Ranise (ranise 'at' fbk 'dot' eu).
