openid / federation

9 stars 5 forks source link

Policy operators: Clarify where the combination rules apply #129

Open vdzhuvinov opened 3 weeks ago

vdzhuvinov commented 3 weeks ago

The current spec (draft 40) says the combination rules apply to a single metadata parameter policy. However, they also apply when statements are merged.

https://openid.net/specs/openid-federation-1_0.html#section-6.1.3

MUST declare what other operators it may be combined within a metadata parameter policy. Combinations that are not allowed MUST result in a policy error.

"Metadata parameter policy" is defined in https://openid.net/specs/openid-federation-1_0.html#section-6.1.2.

Also note, for federation architects and in view of PR #112, that not all allowed combination make sense to be used in a single metadata parameter policy, but to enable the merge of policy statements from different entities.

selfissued commented 3 weeks ago

Agreed that we should clarify this in the spec.

Razumain commented 3 weeks ago

If you choose to clarify this, I would suggest that you could simplify the specification by removing consistency checks altogether and replace this with a very simple validation algorithm when processing metadata.

We do this in our implementation. And it works with 100% consistent end result.

This is our simplified processing order:

  1. Merge all policy operators as specified (ignore any consistency checks) = merged polic
  2. Extract the leaf metadata from the path = leaf metadata
  3. Process leaf metadata against policy modifiers of the merged policy = policy modified metadata
  4. Check policy modified metadata consistency against the complete merged policy

Note: policy modifiers in step 3 are all policy rules that may change the value of the metadata property

If this simple process is used. Any inconsistency in policy values will lead to a failure in step 4. This is simply that it will be impossible to meet the merged policy if it has conflicting values.

This provides much simpler code.

In the end, the standard should only describe the rules that determines what is valid and what is not. Whether an implementation is doing this using our algorithm above, or is doing this using consistency checks should be an implementers choice.

Describing details of how to do a consistency check is therefore redundant in the standard. It should simply be enough to explain why certain combination of policies inevitably will lead to validation failure.

The only rule that MUST be described is the order of value modifiers.

vdzhuvinov commented 1 day ago

@Razumain

If this simple process is used. Any inconsistency in policy values will lead to a failure in step 4. This is simply that it will be impossible to meet the merged policy if it has conflicting values.

Do we have a proof for this?

Last Friday I had a meeting with three researchers from Uni Tübingen, to find out what kind of formal method can be applied to prove the correctness of the policy language spec with respect to the 6 properties / principles. The idea being that if such a proving framework can be established, proposals like this can be run against it, to find out whether they will hold or not. I hope we'll receive a response soon.

The formal analysis that the experts from Uni Stuttgart started has so far been extremely useful in uncovering issues. I wan to find a method or tool that will do the same for the policy language component.