AS & RVPS | Proposal for an attestation applied policy format

[Xynnn007]

Background

During a long time, we use Rego policy to check against parsed claims derived from a TEE evidence. Because of Rego's flexibility we did not talk about the topic so much. Now I raised some limitations of the rego workaround and propose a new format that hopefully could well fit the all typical cases in remote attestation, and also extensible for future profile.

Limitations of Current Rego Policy

1. Does not support mask rule.

For some cases, the claim value is a bitmap. Different bit of the bitmap shows different things of the TEE. Like td_attributes in tdx's claims. Intel's profile for IETF RATS' CoRIM (carrier of reference values) defines similar rules for this. However, in rego it is hard to do bitwise operation.

2. Restrictions upon the writing style of the policy

In current implementation, we assert that the policy would define a bool value named allow to explicit show the result of the policy. In other words, if the policy is not written with an allow value, the enforcement will always fail.

3. Troubles when working together with RVPS

In current implementation, the reference value of a specified claim can be given in two ways:

• Directly in the policy, just like the example rego does
• Provide from RVPS. This is a little tricky. We now couple the code and policy to achieve this. In the policy we use data of OPA to carry reference values from RVPS. In code, we will always query every key inside the parsed claims from RVPS to get reference values, and make the results into a data for OPA.

In a more clear design mode, we should not query any claim keys from RVPS, but rely on some hints in the policy.

There is another topic of "Combined Reference Value" discussed here. This hints that the policy should give a way for users to both a)directly specify the reference value against concrete claims and b) use a TE_id. TE_id here could be linked to a bunch of reference value rules defined in a CoRIM or something else.

Some more information about TE_id. In RATS, we have defined Target Environment to refer to the environment to be attested. Thus some reference value carrier like CoRIM would define a list of values to be matched together against an evidence. it sounds like "hey, if you(the tee) want to match the target environment, you need to match all of the following match rules". The TE_id is the key to index such set of rules.

Proposed Rule Syntax

Based on the observations mentioned before, I want to share a draft of CoCoAS policy design. It support some typical rules.

Numeric Expressions

Syntax

("<claim-key>" <op> <value>)

• <claim-key>: the key of the parsed claims defined in the doc. e.g. sgx.body.isv_svn
• <op>: could be >, >=, ==, <=, <
• <value>: i64 number

Note that once numeric operation is involved, the value of claim-key will be treated as a hex format of an integer number.

For example, ("sgx.body.isv_svn" > 16 means that only if "sgx.body.isv_svn") is greater than 16, this expression will be true.

Set Expressions

We now only define in rule for set.

Syntax

("<claim-key>" <op> <set>)

• <claim-key>: the key of the parsed claims defined in the doc. e.g. sgx.body.isv_svn
• <op>: could be in
• <value>: a list of acceptable values.

For example, ("snp.measurement" in ["aabbcc", "ccbbaa"]) means that only if "snp.measurement" is "aabbcc" or "ccbbaa", the expression will be true.

Naive Assertion Expressions

Syntax

("<claim-key>" is <value>)

• <claim-key>: the key of the parsed claims defined in the doc. e.g. sgx.body.isv_svn
• is: the keyword
• <value>: the expection value for the claim key

For example ("snp.measurement" is "aabbcc") means that only if "snp.measurement" is "aabbcc" the expression will be true.

Mask Expressions

Syntax

("<claim-key>" mask <mask> equ <value>)

• <claim-key>: the key of the parsed claims defined in the doc. e.g. tdx.quote.body.td_attributes
• mask: the keyword
• <mask>: a mask to be applied onto the value of
• equ: the keyword
• <value>: the expected value after applying the mask

For example ("tdx.quote.body.td_attributes" mask "0x0000f0" equ "0x000010") means that only if "tdx.quote.body.td_attributes"'s value does a bitwise-and with 0x0000f0 and gets 0x000010, the expression will be true.

Logic Expressions

Different expressions could be combined using logic expressions.

Syntax

# And
(Expr1 and Expr2 [..and Exprn])

# Or
(Expr1 or Expr2 [..or Exprn])

# Not
(not Expr1)

For example (("tdx.quote.body.td_attributes" mask "0x0000f0" equ "0x000010") and ("tdx.quote.header.version" > 10))

Reference Value Link Expression

This is a special expression rule. This rule will trigger a query to RVPS for a given TE_id, and apply all the reference values upon the current evidence. If the rules of the TE_id all matches, the expression will be true.

Syntax

(with TE <TE_id>)

• <TE_id>: The TE_id of an expected TE.

Full example with different combinations of rules

Here is an example that defines a rule of a combined attestation claim with both GPU and CPU.
It asserts the GPU part should match TE_id gpu-nvidia:123456789 from RVPS. Then, for TDX and SNP it has different rules to check against different fields.

(with TE "gpu-nvidia:123456789")
and
(
  (
    ("tee_type" is "tdx")
    and
    ("tdx.quote.body.mr_td" in ["aa", "bb"])
    and
    ("tdx.quote.body.tcb_svn" > 10)
    and
    ("tdx.quote.body.seam_attributes" mask "0xffffffff" equ "0x00000000")
  )
  or
  (
    ("tee_type" is "snp")
    and
    ("snp.measurement" is "cc")
  )
)

Backup

In RVPS, we could store reference values in such a format too. As reference values are not only simple expected values to directly be matched, but also could involve some rules.

This is still a un-mature draft, please share any suggestions upon this.

[anakrish]

One of the goals we are exploring with Regorus is to use it as a runtime for different policy languages. So, I'd be following the evolution of the language in your proposal closely.

FWIW, the equivalent Rego would be something like

rules["gpu-nvidia:123456789"] if {
  input.tee_type == "tdx"
  input.tdx.quote.body.mr_td in ["aa", "bb"]
  input.tdx.body.tcb_svn > 10
  bits.and(input.tdx.body.seam_attributes, 0xffffffff) == 0x00000000
} else {
  input.tee_type = "snp"
  input.snp.measurement == "cc"
}

allow = rules[input.gpu_part] if {
   reference_values = rvps_get_reference_values(input.gpu_part)
   check_reference_values(reference_values)
}

where rvps_get_reference_values is a custom builtin function that is registered via Engine::add_extension

[fitzthum]

Does not support mask rule.

SNP also has a field that requires bitwise evaluation. Currently the SNP verifier splits this into several different claims.

Here are some things I don't like about the current implementation:

• It is confusing to have a policy for the AS and a policy for the KBS.
• The output of the policy is constrained (as @Xynnn007 mentions, users have to know that the policy should return certain fields).
• No support for EAR. Generating a valid token in OPA is cumbersome and if we require the output of the policy to be EAR, we will have a much more extreme case of the above issue, where users will be required to write a complex policy.
• RVPS interaction is under-defined. We should introduce a level of indirection that allows different reference values to be used in different situations. I'm not sure the best way to do this yet.

Maybe some of these issues would be solved by this proposal but not necessarily.

Another option would be to make use of custom builtins like @anakrish mentions. Maybe we could come up with a nice helper function for reference values and some helpers for EAR.

[Xynnn007]

Hey, @fitzthum shares some very good points also I highly agree with.

• It is confusing to have a policy for the AS and a policy for the KBS.

Yes. Currently they two both share logic to verify evidence. An ideal form should be

• AS has its policy to verify evidence, and get an EAR or some token.
• KBS has its policy. The policy should have two functionalities (probably we need to split KBS into two parts and each has a policy) a) rules to map an EAR to a certificate(This is for authorization) b) client identity and YES/NO to access the resource (authentication and access control)

• The output of the policy is constrained (as @Xynnn007 mentions, users have to know that the policy should return certain fields).

+1

• No support for EAR. Generating a valid token in OPA is cumbersome and if we require the output of the policy to be EAR, we will have a much more extreme case of the above issue, where users will be required to write a complex policy.

Yes. If we ensure the output is an EAR, explicitly the user should at least define "what claims should be related to executables / file-system trustworthiness-vector" and things similar. Hints that once EAR is chosen, the policy should match that. A baby-shape workaround in CoCo, could be

• rootfs verification like dm-verity root hash will always be mapped to file-system trustworthiness-vector.
• verifier verification (almost all tees' verifier plugin only checks the endorsement of the tee evidence) will be mapped to hardware trustworthiness-vector.
• initdata/kernel cmdline will be treated as configuration
• guest fw/td-shim, kernel will be mapped to executables

Or, we could add some extra rules upon the proposed to map specific rule set to specific vector.

• RVPS interaction is under-defined. We should introduce a level of indirection that allows different reference values to be used in different situations. I'm not sure the best way to do this yet.

Only a personal view. After reading some parts of Intel profile for CoRIM, I found that the reference value defined by IETF RATS is beyond simple "value match". It also could include some complex boolean logic. This enlights me to treat reference value inside the RVPS also a defined "policy". This means, although the inputs into the RVPS is some different provenance (CoRIM, in-toto, ...), but the actual thing stored is a id (TE_id, to refer to a reference value) and its related policy/rule set.

If CoCoAS wants to query reference value from RVPS, the actual thing it gets is a part of policy, which shares the same format as CoCoAS' (this is just the inner storage of RVPS, and transparent to users). So please see the Reference Value Link Expression part in the proposal, it could be understood as an "import" statement, "importing" the reference value/rule set marked TE_id from RVPS.

[Xynnn007]

@anakrish Thanks for the pointers and the form of rego looks pretty dry, TBO.

When I tried to use add_extension of regorus and still does not come up with a good solution for Reference Value Link Expression mentioned in the proposal. The translation has almost the same meaning of the original example, apart from the (with TE "gpu-nvidia:123456789") part. That means similar to include for some other languages. It will include extra rules set indexed by gpu-nvidia:123456789 as a key, and use the original parsed claims as a whole to work as the input.

add_extension supports regorus::Values as inputs, such as String, etc. I tried passing TE_id(a string, s.t. the key to rule set) as a parameter, but found that the content of the input json could not be referenced inside the closure function.

Another problem might be from my poor rego experience. Try to think of such a combined logic A or B or (C and (D or E)). If we use rego, we should write as

allow {
   A
}

allow {
   B
}

allow {
   C
   C'
}

C' {
   D
} else {
   E
}

all are flattened and might not be straright forward/friendly enough for most developers. IMOO, I still want the users could have a straightforward way to write policies -- at least or rules could be seen together without defining intermediate variables.

Some ways

way	Pros	Cons
Using existing rego	directly	a) reference value b) or rule writing
Invent a new one, and implement evaluation logic for the DSL	No need to care about translation part	need to write AST parser
Invent a new one, and implement the translation logic from the DSL to rego, and use regorus as runtime	No need to care about evaluation	a) need to write AST parser b) translation part would make trouble

[anakrish]

@Xynnn007

add_extension supports regorus::Values as inputs, such as String, etc. I tried passing TE_id(a string, s.t. the key to rule set) as a parameter, but found that the content of the input json could not be referenced inside the closure function.

I'm not sure if I follow you exactly. One can pass any value including the input to extensions. E.g: rvps_get_reference_values(input).

In case something doesn't work as expected, can you share the code here or create an issue at https://github.com/microsoft/regorus? Since Regorus is being used more and more internally at Microsoft, I'd want to promptly address any issues.

One thing you will not be able to achieve using Regorus extensions is to add rules to the current engine. If we were to allow that, then it will violate Rego semantics - an extension could add an alternative for a rule that has already been evaluated or the added rules could change the outcome of already evaluated rules etc; making policy evaluation harder to reason about and understand.

However, an extension is free to instantiate another engine instance to evaluate rules.

[anakrish]

@Xynnn007 I don't exactly follow your use case, but the following technique of composing policies could be relevant: https://www.styra.com/blog/dynamic-policy-composition-for-opa/

[fitzthum]

Yeah I am still not sure what to do here. Maybe we should talk about this in the next Trustee developer meeting.