-
Notifications
You must be signed in to change notification settings - Fork 7
CoRIM core concepts (opinion)
We've worked on this specification for years, and have only begun to scratch the surface of describing what many constructs mean generally.
RFC9334 states
The Verifier appraises Evidence via appraisal policies and creates the Attestation Results to support Relying Parties in their decision process.
Given the responsibility is execution of policy, and RATS does not include policy in its charter, we walk a fine line. The CoRIM specification is a means to inform policy and what different parties consider trustworthy with regards to presented evidence.
Our responsibility as CoRIM specifiers is to produce a useful information model that policy writers can depend on as a pre-processing step before making judgments.
To get an RFC of "base" constructs out the door so we can move the rest to non-normative additions that will be specified in a later RFC, I propose the following notion of what should be base.
The core responsibilities of a Verifier are
- To verify evidence is signed by a trusted party for the purpose of signing that kind of evidence.
- To produce claims about the target environment based on that evidence that can be used by a relying party to made a trust decision.
The most fundamental claims are
- some trusted party stated that a certain claim in a certain kind of environment should be a certain value.
- some trusted party stated that a certain claim in a certain kind of environment is a certain value.
The should be aspect is a form of conditional endorsement. The provider adds their signature to a claim only if the claim value asserted by evidence matches their expectation.
"Matching expectation" has opened a can of worms that has bled the line between a full policy language itself and a simple data model. It might make sense to have signed policy fragments with modular semantics for more complicated distribution of responsibility for attestation appraisal. However, CoRIM is meant for the simplest of statements than any Verifier would need to consider.
In programming languages, we study core calculi that express all the behavior of the language without any of the ergonomics. Any language construct on top of the core is considered "macro-expressible" if you can transform the construct to more fundamental constructs without any surrounding context.
If we can define the core concepts, we can then build the rest of the specification as ergonomic expressions of that core, but leave the description of the semantics to just the core.
To get value out of the abstraction of reference values matching evidence, the CoRIM Verifier theory of operation describes a procedure of ornamentation of who (authorities) said what (triples) about where (environments). The ornamented data model is not normative, but the information model is. This specification is useful only if compliance to this ornamentation procedure produces a form of information that expresses the same intent of the CoRIM signer.
We can then pass this ornamented data structure to a policy engine to approve, reject, add, or subtract claims from before the verifier produces a result. A thin, easy-to-understand policy based on shared understanding of baseline appraisal procedures improves the quality of the attestation ecosystem.
- A concept of "where" claims are about, to be used for either Attester or Target: We have
environment-mapfor this. - A representation of claims specific to an environment.
- A means of endorsing evidence claims at the specificity of class or instance: we have reference value triples for this.
- A means of attaching claims to an environment at the specificity of class or instance: we have endorsed value triples for this.
- Integrity protection of claims in this representation: we have COSE_Sign1-corim for this.
- A means of qualified changes to semantics: we have profiles for this
There's extra information in the base specification that remains from the TCG DICE endorsement architecture's origins that would be preferable to move to either a profile or normative extension RFC.
To allow claims to have specificity about a class of attester without consideration of the instance, the environment-map can "matched" if unspecified fields in CoRIM are treated as wildcards for the actual state that is fully concrete in the ornamented data structure (the ACS).
A condition could potentially reference a "stored procedure" in a policy evaluator, but we don't have a means to tie reference to policy in this way. An extension RFC could very well specify a CoProcedure tag type that a condition can reference to specify complex logic, but that is hypothetical and not considered core.
It's incredibly confusing to reuse the same data type for representing actual values and for representing matching patterns. Very few programming languages make this kind of pun.
let x = 5;
let y = 1;
match y {
x => x + y,
_ => panic("noo")
}
Is this 2, 6, or panic? Generally a variable in pattern position imposes no structure requirements and instead binds that variable to whatever structure it's being matched against. CoRIM doesn't have variables in this way, so this is unfair. We're looking at literal values, or structures with wildcards only, until we start throwing in the Intel TDX expression language.
Only some data structures are allowed to be matched substructurally, like environment-map, but not like mkey. The position of a value changing the sense in which it's compared is unfortunate.
match data {
Foo{y: _, z: Bar{w: 5}} => Endorse{good: true}
}
If data is an mkey, this is ill-formed because _ is not a literal value that can be translated to a CBOR encoding. If data is an environment, then y as instance: is fine. Odd.
I understand we have this condition/value duality due to the condition-addition semantics of reference values, but we ought to have something simpler to represent it in. Ned started doing this with the definition of "relations", but those are internal-only.
It makes sense to me for there to be basic measurement value types, and names of measured components.
What is lost in translation is that "component" can have many different kinds of measurement values, but only one of them unless a profile names a non-normative index to be a certain measurement value type.
We re-added multiplicity of measurement-map with mkey/mval pairs to allow expressing the original intent, which is to name the component and give it the single value it embodies.
So now we have extra encoding overhead of using a map of a key of a value instead of a #6.(value). I guess that's fine.
Raw value mask is indicative that reference values need to be conditional as well. This is the only fuzzy matching that's allowed for reference values. It makes no sense for an attester to produce evidence that is a mask, so it's purely pattern.
In what sense is a reference value not just an endorsement? It appears to only be cm-ind and its hidden use within the theory of operation. The condition for a reference value MUST be for evidence, and not for some other endorsement.
We decided that authorized-by should not be used for tying reference values to the expected attester's RoT.
The only way to ensure that you're not matching a rando's endorsement of the same claims is to make the matching condition require cm-ind: evidence.
We restrict ourselves to monotonically increasing our knowledge. Given the ornamented structure of what we know, we can make an addition to it.
Claims from different parties have different senses: cm-ind.
core-triple-record = [conditions, additions]
conditions = #6.<and>([ condition ]) / [ condition ]
condition = {
cm-ind => $cm-ind-pattern,
env => $environment-pattern,
mkey => $mkey-pattern,
mval => $mval-pattern,
authority => $authority-pattern
}
additions = [ + addition ]
addition = [$cm-ind-expression, $environment-map-expression, [ + $measurement-map-expression ]]
cm-ind = &(evidence: 0, reference: 1, endorsement: 2)
We could say that there are no unconditional triples, as we've required that there be some non-empty environment condition, but that's a design decision that's not fundamental. The unit value of AND is TRUE, so and([]) is a condition that always succeeds.
Patterns and expressions are the core evaluation components, but they're extremely limited in the core to keep their evaluation cost down.
The patterns express the intended matching semantics. The expressions express how to translate pattern matching results into explicit claims that will be added to the ACS.
$cm-ind-pattern /= #6.<equality>(cm-ind) / cm-ind
$environment-pattern /= #6.<map-subeq>(environment-map-pattern) / environment-map
environment-map-pattern = non-empty<{
? class => class-pattern,
? group => group-pattern,
? instance => instance-pattern
}>
class-pattern /= #6.<equality>(class-map) / class-map
group-pattern /= #6.<equality>($group-id-type-choice) / $group-id-type-choice
instance-pattern /= #6.<equality>($instance-id-type-choice) / $instance-id-type-choice
$mkey-pattern /= #6.<equality>($measured-element-type-choice) / $measured-element-type-choice / #6.<wildcard>()
$authority-pattern /= #6.<list-subeq>([ + $crypto-key-type-choice ]) / [ + $crypto-key-type-choice ]
$mval-pattern /= #6.<map-subeq>(measurement-values-pattern) / measurement-values-map / #6.<wildcard>()
The class-group-instance non-empty map treats missing keys as the key mapping to a wildcard. It's harder to express that at least one aspect of the environment must be present in the pattern if we allow the field patterns to contain wildcards.
The cm-ind is not allowed to be a wildcard, though we may consider representing the logical OR of indicators. The mval pattern is allowed to be a wildcard since we have endorsement triples that need only match an environment.
Then we have the big one, for comparing any kind of measured value.
measurement-values-pattern = non-empty<{
? &(version: 0) => $version-pattern
? &(svn: 1) => $svn-pattern
? &(digests: 2) => $digests-pattern
? &(flags: 3) => $flags-pattern
? &(raw-value: 4) => $raw-value-pattern
? &(mac-addr: 6) => $mac-addr-pattern
? &(ip-addr: 7) => $ip-addr-pattern
? &(serial-number: 8) => $serial-number-pattern
? &(ueid: 9) => $ueid-pattern
? &(uuid: 10) => $uuid-pattern
? &(name: 11) => $name-pattern
? &(cryptokeys: 13) => $crypto-key-pattern
? &(integrity-registers: 14) => $integrity-registers-pattern
* $$measurement-values-pattern-extension
}>
$version-pattern /= #6.<equality>(version-map) / version-map
$svn-pattern /= tagged-svn / tagged-min-svn / svn
$digests-pattern /= #6.<digest-downgrade-safe>(digests-type) / digests-type
$flags-pattern /= #6.<map-subeq>(flags-map) / flags-map
$mac-addr-pattern /= #6.<equality>(map-addr-type-choice) / mac-addr-type-choice
$id-addr-pattern /= #6.<equality>(ip-addr-type-choice) / ip-addr-type-choice
$ueid-pattern /= #6.<equality>(ueid-type) / ueid-type
$uuid-pattern /= #6.<equality>(uuid-type) / uuid-type
$serial-number-pattern /= tstr-pattern
$name-pattern /= tstr-pattern
$crypto-key-pattern /= #6.<equality>([ + crypto-key-type-choice ]) / [ + crypto-key-type-choice ]
$integrity-registers-pattern /= #6.<map-subeq>(integrity-register-map-pattern) / integrity-registers
integrity-register-map-pattern = {
+ $integrity-register-id-pattern => $digests-pattern
}
$integrity-register-id-pattern /= tstr-pattern / uint-pattern
uint-pattern = #6.<equality>(uint) / uint
tstr-pattern = #6.<equality>(tstr) / tstr
The raw value pattern is still the topic of PR #294, though it'd be something like
$raw-value-pattern /= #6.<equality>($raw-value-type-choice)
$raw-value-pattern /= #6.<masked-bytes>(bytes, bytes)
Finally given that the base pattern language does not describe any kind of binding, the expression codepoints are the same as the value codepoints
$cm-ind-expression /= cm-ind
$environment-map-expression /= environment-map
$measurement-map-expression /= measurement-map
Metadata without explicit meaning for verifier operation.
- Domain triples (not given a semantics)
- Conditional endorsement series (expressible as multiple conditional endorsements)
- device and attestation key triples
- linked tags (PKI management and knowledge base update API). Should be part of the endorsement API for lifecycle management updates.
- coswid links
What's not core if we only consider keys with certificates that contain metadata:
- validity-map (remit to signing key expiry)
- corim-meta-map (certificate subject)
- entity-map (certificate subject)