-
Notifications
You must be signed in to change notification settings - Fork 0
Tools
Quantification of permissions of policies. Translation of the policies to SMT (complying to SMTLIB2) and uses a model-conting solver (ABC). Targets AWS, GCP and Azure.
The most interesting feature for our solution might be the relative permissiveness of policies. For instance, when updating a policy, it is possible to get how many more (or less) requests would be authorized:
$ python3 quacky.py -p1 ../samples/iam/exp_multiple/iam_policy_allow_adding_deleting_users/initial.json -p2 ../samples/iam/exp_multiple/iam_policy_allow_adding_deleting_users/fixed.json -b 100 -c
Policy 1 ⇏ Policy 2
╒═════════════════╤════════════════════╕
│ Solve Time (ms) │ 2643.81 │
├─────────────────┼────────────────────┤
│ satisfiability │ sat │
├─────────────────┼────────────────────┤
│ Count Time (ms) │ 22030.9 │
├─────────────────┼────────────────────┤
│ lg(requests) │ 1281.5063376238318 │
╘═════════════════╧════════════════════╛
Policy 2 ⇏ Policy 1
╒═════════════════╤════════════════════╕
│ Solve Time (ms) │ 886.112 │
├─────────────────┼────────────────────┤
│ satisfiability │ sat │
├─────────────────┼────────────────────┤
│ Count Time (ms) │ 8414.03 │
├─────────────────┼────────────────────┤
│ lg(requests) │ 1121.8519782898493 │
╘═════════════════╧════════════════════╛
Policy 1 and Policy 2 do not subsume each other.
The result above means that Policy 1 and Policy 2 are incomparable, which happens if both formulas, i.e. Policy 1 ⇏ Policy 2 and Policy 2 ⇏ Policy 1, are satisfiable. In this case, the individual results "can be used to determine which policy is objectively more permissive (total requests allowed)", i.e. Policy 1 is more permissive than Policy 2.
Important notes:
- Quacky: Always uses
abc -bs <values>, i.e. model count string length bound. - ABC: Regular constraints result in precise solution; Otherwise, in overapproximation. Moreover, overapproximation may happen if ABC needs to convert string to integer variables or integer to string variables. In any case of overapproximation, ABC returns SAT when it is actually UNSAT. One way of overcoming this would be to only use integers, thus avoiding conversions, but Quacky always uses strings. See vlab-cs-ucsb/ABC/issues/10 for more details.
-
Eiers2022: Assumptions over valid characters and lengths for resources (object's Key or user's UserId) do not match all of AWS S3 requirements.
- It is not completely clear how to choose a meaningful value for the bound. The authors often use 100 for objects' Keys and 20 for users' UserIds, but those number do not correspond to AWS limits and no reasoning for choosing them is given.
In-house AWS analyser aiming to arrive at least-privilege IAM policies.
CloudSec (cloudsecpy on PyPI) is a library and toolkit for formally analyzing security policies in cloud and API systems using Python.
Graph-based verification of access control policies.
Open-source AWS exploitation framework, designed for offensive security testing against cloud environments.
Automatic synthesis of XACML policies.