Skip to content

Appraisal using a Singleton Verifier

Ned Smith edited this page Aug 14, 2023 · 1 revision

Verifier Examples

Staged Verification Example

This example shows Evidence on the left and a first CoRIM as input to stage 1 verifier.

The Stage 1 output is the next rectangle from the left. It becomes the input to the second stage along with a second CoRIM.

The Stage 2 output becomes the input to Stage 3 along with an Appraisal Policy, which produces the Stage 3 output.

The Verifier could add claims that it makes as Attestation Results. For example, the Verifier could add an AR4SI assertion to Stage 3 output (accepted claims). Note: the diagram seems to suggest

Diagrams follow these coloring and formatting conventions.

It may be helpful to read the claims sets according to the Abadi calculus.

Use Case Examples

There are three example use cases that are helpful to understand how Verifier may group sets of claims. A group context determines the set of claims that are evaluated together when determining if there is a match. It is possible for one group of claims to "match" while a different group doesn't.

Use Case 1 - Simple composition with OEM (chassis), 2 ODMs (NIC, MB)

Slide 5: https://drive.google.com/file/d/1ReOO2FIcuZkk7kqAdkSiGdomNMYkvmNM/view?usp=share_link

Verifier Steps:

  1. Use rim-locator to find OEM, MB, and NIC RIMS

  2. Use CoBOM to discard all tags besides Chassis, Board, and Card

  3. Use Domain membership to create Chassis domain (F00) and to include motherboard domain (C00) into working model.

  4. Use Domain membership to include Card domain (E00) and board subdomains (C10, C20).

  5. Use Domain membership to include refv 300 and 301 in subdomains C10, C20 respectively.

  6. Use Domain dependency to record that C20 depends on C10

  7. Use Domain membership to include Card subdomains (E10, E20)

  8. Use Domain dependency to record that E20 depends on E10

  9. Collect Evidence from Board Attester.

    1. Select Cert L0 evidence
    2. Find domain containing class-id=300. (since only C10 has 300 search is deterministic)
    3. Compare Evidence (class-id=300) to refv (class-id=300) (if evidence included domainid=C10 then compare membership domains)
    4. Accept evidence ver=“1.0” and svn=0 in ACCEPTED-CLAIMS (include domain F00, C00, and C10 context)
    5. Select Cert L1 evidence
    6. Find domain containing class-id=301. (since only C20 has 301 search is deterministic)
    7. Compare Evidence (class-id=301) to refv (class-id=301) (if evidence included domainid=C20 then compare membership domains)
    8. Check that there are accepted claims 300 from domain C10, if true, then finalize matching of 301 evidence
    9. Accept evidence digest=9876 in ACCEPTED-CLAIMS (include domain C20 context)
  10. Collect Evidence from Card Attester

    1. Select Cert L0 evidence
    2. Find domain containing class-id=200 and class-id=201.
    3. Compare Evidence (class-id=200) to refv (class-id=200) and class-id=201 to refv 201
    4. Accept evidence ver=“1.0”, svn=0, digest=FEDC, and digest=CDEF in ACCEPTED-CLAIMS (include domain E10 context)
    5. Select Cert L1 evidence
    6. Find domain containing class-id=202
    7. Compare evidence class-id=202 to refv class-id=202
    8. Accept evidence raw=1F0 in ACCEPTED-CLAIMS (include domain E20)
  11. Accept endv label=“PC1” into ACCEPTED-CLAIMS

  12. Exceptions result in ACCEPTED-CLAIMS becoming null. Note: Domain membership includes the domain ID as a member explicitly, but this could be inferred. However, explicit declaration as a class-id allows inclusion of subdomains using membership triple. Consequently, compositional hierarchies can be constructed.

Use Case 2 - Simple composition with versioning

Slide 6: https://drive.google.com/file/d/1A7pZCKxRlmgCSVI73ZQ-W8pxqxAA-xoR/view?usp=share_link The board vendor issues a SW update that produces a second MB RIM with different version number

Verifier Steps:

  1. Use rim-locator to find OEM, MB, and NIC RIMS
  2. Use CoBOM to discard all tags besides Chassis, Board, and Card
  3. Use Domain membership to create Chassis domain (F00) and to include motherboard domain (C00) into working model.
  4. Use Domain membership to include Card domain (E00) and board subdomains (C10, C20).
  5. Use Domain membership to include refv 300 and 301 in subdomains C10, C20 respectively. (Since there are two RIMs for refv 300/301, (ver=“1.0”, digest=9876), and (ver=“2.0”, digest=1234) are grouped by tag-id)
  6. Use Domain dependency to record that C20 depends on C10
  7. Use Domain membership to include Card subdomains (E10, E20)
  8. Use Domain dependency to record that E20 depends on E10
  9. Collect Evidence from Board Attester.
    1. Select Cert L0 evidence
    2. Find domain containing class-id=300. (since only C10 has 2 class-id=300 entries search results are grouped by tag-id)
    3. Compare Evidence (class-id=300) to refv (class-id=300) (if evidence included domainid=C10 then compare membership domains)
    4. Accept evidence ver=“2.0” and svn=0 since both are in second tag-id set; Copy measurements to ACCEPTED-CLAIMS (include domain F00, C00, and C10 context)
    5. Select Cert L1 evidence
    6. Find domain containing class-id=301. (since only C20 has 2 entries for 301, group by tag-id)
    7. Compare Evidence (class-id=301) to refv (class-id=301) within tag-id grouping (if evidence included domainid=C20 then compare membership domains)
    8. Check that there are accepted claims 300 from domain C10 within tag-id grouping and that C20 depends on C10, if true, then finalize matching of 301 evidence
    9. Accept evidence digest=1234 since previous in ACCEPTED-CLAIMS (include domain C20 context)
  10. Collect Evidence from Card Attester
    1. Select Cert L0 evidence
    2. Find domain containing class-id=200 and class-id=201.
    3. Compare Evidence (class-id=200) to refv (class-id=200) and class-id=201 to refv 201
    4. Accept evidence ver=“1.0”, svn=0, digest=FEDC, and digest=CDEF in ACCEPTED-CLAIMS (include domain E10 context)
    5. Select Cert L1 evidence
    6. Find domain containing class-id=202
    7. Compare evidence class-id=202 to refv class-id=202
    8. Check that there are accepted claims 200 and 201 from domain E10 and that E20 depends on E10, if true, then finalize matching of 202 evidence
    9. Accept evidence raw=1F0 in ACCEPTED-CLAIMS (include domain E20)
  11. Accept endv label=“PC1” into ACCEPTED-CLAIMS
  12. Exceptions result in ACCEPTED-CLAIMS becoming null.

Notes: tag-id is used as a grouping value because there are multiple TAGs that have identical domain and membership configuration. The rational is that each tag instance has contextual information that doesn’t need to be thrown away. If tag context isn't used, there would need to be some other source of context that describes what was updated. For example, a stateful environment (e.g., stateful-environment-record) that includes version info.

Use Case 3 - Complex composition with multiple instances of same NIC

Slide 7: https://drive.google.com/file/d/1KIeGO6WqXB5TjtLqhdvlkdisdyOgZwUl/view?usp=share_link

Verifier Steps:

  1. Use rim-locator to find OEM, MB, and NIC RIMS
  2. Use CoBOM to discard all tags besides Chassis, Board, and Card
  3. Use Domain membership to create Chassis domain (F00) and to include motherboard domain (C00) into working model.
  4. Use Domain membership to include Card domain (E00) and board subdomains (C10, C20).
  5. Use Domain membership to include refv 300 and 301 in subdomains C10, C20 respectively.
  6. Use Domain dependency to record that C20 depends on C10
  7. Use Domain membership to include Card subdomains (E10, E20)
  8. Use Domain dependency to record that E20 depends on E10
  9. Collect Evidence from Board Attester.
    1. Select Cert L0 evidence
    2. Find domain containing class-id=300. (since only C10 has 300 search is deterministic)
    3. Compare Evidence (class-id=300) to refv (class-id=300) (if evidence included domainid=C10 then compare membership domains)
    4. Accept evidence ver=“1.0” and svn=0 in ACCEPTED-CLAIMS (include domain F00, C00, and C10 context)
    5. Select Cert L1 evidence
    6. Find domain containing class-id=301. (since only C20 has 301 search is deterministic)
    7. Compare Evidence (class-id=301) to refv (class-id=301) (if evidence included domainid=C20 then compare membership domains)
    8. Check that there are accepted claims 300 from domain C10, if true, and that C20 depends on C10 then finalize matching of 301 evidence
    9. Accept evidence digest=9876 in ACCEPTED-CLAIMS (include domain C20 context)
  10. Collect Evidence from Card Attester
    1. Select Cert L0 evidence
    2. Find domain containing class-id=200 and class-id=201.
    3. Compare Evidence (class-id=200) to refv (class-id=200) and class-id=201 to refv 201
    4. Accept evidence ver=“1.0”, svn=0, digest=FEDC, and digest=CDEF in ACCEPTED-CLAIMS (include domain E10 context)
    5. Select Cert L1.a evidence
    6. Find domain containing class-id=202
    7. Compare evidence class-id=202 to refv class-id=202
    8. Check that there are accepted claims 200 and 201 from domain E10, if true, and that E20 depends on E10 then finalize matching of 202 evidence
    9. Accept evidence raw=1F0 in ACCEPTED-CLAIMS indexed by mkey, e.g., “bus=0,port=0”. (include domain E20)
    10. Select Cert L1.b evidence
    11. Find domain containing class-id=202
    12. Compare evidence class-id=202 to refv class-id=202
    13. Check that there are accepted claims 200 and 201 from domain E10, if true, and that E20 depends on E10 then finalize matching of 202 evidence
    14. Accept evidence raw=1F0 in ACCEPTED-CLAIMS using mkey to disambiguate, e.g., “bus=0,port=1”
  11. Accept endv label=“PC1” into ACCEPTED-CLAIMS
  12. Exceptions result in ACCEPTED-CLAIMS becoming null.

Note: If evidence doesn’t have mkey support (eg., concise-evidence ) then conveyance mechanism must supply an mkey equivalent. For example, an SPDM payload could contain bus and port address info. Mkey might still be useful in ACCEPTED-CLAIMS as a way to capture the bus and port configuration information that distinguishes the NIC instances.

Note: Using concise-evidence rather than DiceTcbInfo would allow evidence in L1.a and L1.b to both assert domain membership of E20. The same domain dependency check is valid for both, because they are clonal instances.

All Slides

See: https://drive.google.com/file/d/1uhvv89ZoSxsYd4bbMShZRuHUOlHtCRMN/view?usp=share_link

Clone this wiki locally