-
Notifications
You must be signed in to change notification settings - Fork 0
Ideas
-
Policies and Policy sets. We assume that a system (whole of or a part of it) is protected
by a set of security policies combined into a set (policy-set) comprising individual policies
(such as permit or forbid rules). - Closed-world analysis. An analysis where the entity set is known and finite. This should make analysis more practical and scalable. A drawback of the approach is that the analysis result becomes invalid with the introduction of new principals or resources.
- Established security boundaries. For a system under analysis the set of security-related invariants (that should hold during execution regardless of configurations) are known and available.
- Available monitoring results. RSVP does not tackle the question of monitoring. Instead, it is assumed that system events (potentially tagged positive or negative) are available as input.
- Policy set available. It is assumed that the initial set of policies is available for analysis. This is a soft assumption, however, in the absence of policies it can be assumed that the system either forbids any behaviours or allows everything. Policies can be synthesised from observed behaviours.
- Development language: Java 21+
- Target Policy Language: Cedar
- SMT: Z3
- SAT: Sat4J
- Datalog: Souffle
- Answer-set Programming: Potasco
- Relational Model Finder: Kodkod
- Prolog: SWI-Prolog
Given a set of security policies P we can identify and flag conflicts and redundancies within P. For instance, a policy subsuming other policy can be removed. Since redundancy can be intentional the tool should allow annotating decisions and exclude exceptions from future analysis. Prior work established and classified different types of inconsistencies (also known as anomalies).
We can also establish general well-formedness criteria for a set of policies. For instance: all resources should be covered by policies. Yet another question is consistency: two logically equivalent queries (as well as logical derivations) should produce equivalent result. E.g., if a request is allowed, then the negation of the request should be denied. I have not come across a convincing example of this kind of inconsistency (and I do not know whether that could apply to Cedar policies), but this paper indicates that such inconsistencies could potentially arise due to inheritance relationships between attributes.
For policy anomaly detection we can consider two broad cases:
- Intra-policy anomalies (anomalies within a policy set). Cedar has clear semantics with respect to evaluating requests. In this regard we can only reason about properties such as redundancy or inclusion. Permit/forbid conflicts are always resolved in favour of forbid, and as such can be considered part of the policy design.
- Inter-policy anomalies (anomalies arising due to a join of several policy set). In addition to redundancy and inclusion, we can consider policy conflicts as different decisions of different policy set for some request. In a simple scenario, some request r can be explicitly allowed by the policy set P1 but forbidden by the policy set P2.
A few years back an interesting and quite compelling case of using answer-set programming has been put forward (for XACML). Given that ASP can reason about sets of answers (rather than individual solution) makes this approach quite relevant for encoding policy consistency problems. With some modification this can probably be adopted for Datalog or SMT.
Given a set of security bounds (invariants) A a tool can identify whether the existing policy set P is compliant with A. One way to accomplish such compliance checks is via an SMT encoding akin to Zelkova and an off-the-shelf SMT solver. While widely used at Amazon (based on publications), it is still unclear whether this approach scales for the large policy sets or complex conditions. Further, it may not be cross-platform, e.g., whether other cloud providers have similar functionality it is unclear.
Another approach is a reachability-style analysis, where the system is represented as an annotated graph or a collection of relations that can be queried. This is useful when reasoning about networking properties (e.g., is database reachable, can an attacker connect to a private subnet) and it can be extended to reason about more complex properties that go beyond reachability queries. Some of these ideas has been explored here and here.
Since we are considering closed-world, that operates on a given set of facts, it should be possible to encode these problems using datalog or answer-set programming. I have seen techniques to analyse policy anomalies using ASP, but I have not yet seen techniques leveraging datalog for verification-like tasks. The attractive side of this kind of analysis is that it can produce a collection of answers (rather than a single counter-example). In addition tools such as Souffle are known to scale to large problem sizes.
A security policy set in a cloud environment typically includes inter-policy dependencies. For instance, permissiveness of a permit policy can be reduced using a forbid policy. Furthermore, policies describing orthogonal sets of permissions can have resource-based dependencies (detailed example here). Altering a security policy, thus, can have unintended consequences. A tool can, for instance list/visualise such dependencies and effects on policy changes.
Counting SMT solvers can be used to quantify requests allowed or forbidden by a policy. Request count is useful in measuring effects of the policy, but it might be misleading because there could be many equivalent requests that obscure the overall picture. Rather than computing the number of requests we can consider breaking down requests into the equivalence classes (similar to this) or consider reasoning about the allowed requests in terms of relevant predicates. In either case such qualification can help with (1) understanding policy effects (change-impact analysis) and (2) evaluating consequences of policy modification.
It is fairly typical for cloud security policies to be overly permissive. One approach to tighten security bounds is to take into account a set of positive and negative requests, and update policy such that it accepts all positive examples and rejects all negative. This work can be extended by synthesising security policy from scratch based on the examples (if the set of initial policies is missing). There has been work in this area relating to:
- Reducing permissiveness of policies with minimal changes to their syntactic structures (problem of policy updates is shifted to predicate updates)
- Reducing permissiveness of policies based on quantification
In a typical scenario a cloud system enables security through several (often orthogonal) mechanisms. For example, AWS provides both Cedar and IAM that serve different purposes. One idea is to look at the security posture of a system as a whole by translating different security specification in a unified intermediate representation (we can use Cedar for that).
While this functionality may be replicated by Cloud providers (in one form or another), from the point of view of policy understanding, it might be useful to issue specific queries to understand principal permissions in a given context. E.g., who has access to a particular file, what actions can be performed on a particular resource and so forth. On a similar note, we can reason about the level of protection of similar components, e.g., which policies restrict access to a given resource, are all resources protected etc.