`gh at verify` evaluates policy transparently and monotonically

[phillmv]

summary

We've been thinking about how gh at verify works. We've realized that gh at verify is in effect used to evaluate policy – and that therefore we have to improve its user experience.

As a result, we've decided that the tool ought to:

1. be more explicit/transparent about what criteria, exactly, are being used to make pass/fail decisions
2. provide meaningful defaults (& that we will begin enforcing provenance predicates unless otherwise specified)
3. evaluate policy monotonically

this issue is our public facing description of these changes. hello!

context

when we originally set out to create gh at verify and the underlying sigstore-go library, we had many conversations about the nature of "policy" and "verification". to wit, where does "verifying crypto materials" end, and "enforcing organization-specific rules and procedures" (aka policy) start?

we wanted to avoid guessing what our users wanted to enforce as a rule or procedure, and as a result gh at verify erred on the "we're verifying the crypto materials" side of things. we imagined that our users would plug the tool's output into a "real" policy evaluation tool.

eventually, we realized that despite this initial intention, gh at verify can and ought to be used to "enforce organization-specific rules" and is actually the first point of entry the vast majority of users will use for dealing with the organization-specific rules and procedures.

outcomes

as a consequence, the tool needs to be able to spell out exactly what is being verified. the tool needs to have a meaningful default for predicate types: it doesn't make sense for an artifact to be "verified" just because there is an SBOM attached when you probably meant to check for its provenance. and finally, the tool should not give up as soon as it encounters a single attestation that fails to verify according to our criteria.

monotonic policy evaluation

this last step we call "monotonicity", as in the monotonicity of entailment.

Adopting the language of formal systems, a command like:

gh at verify -R github/foo artifact.bin

expresses a sentence (“github/foo originated artifact.bin”) that is either true or false, and whose truth value can be deduced from the attestations (i.e. a set of independent propositions) that are associated with the artifact.

In this view, the truth value of the policy statement is monotonic because, once gh at verify evaluates a policy statement to be true, it is not be possible for that statement to become invalid by adding new attestations.

[gillisandrew]

Great to see!

Could the refactor include Rego or CUE policy evaluation like cosign supports?

It would help improve UX on a few fronts:

• Extracts verification logic from the source code for easier testing and audit
• Allows users/orgs to evaluate against their own policies in the same format used by other tools (cosign, k8s admission controllers, etc.)

Reference

https://github.com/sigstore/cosign/pull/641

[phillmv]

@gillisandrew thanks for the note!

We spent some time thinking about this and we feel that users are better off piping the output of the gh at verify command using the --format=json flag into their tool of choice. We've produced some demos with this using OPA, and at a glance it seems to be perfectly cromulent.

Compared to cosign, we face a few constraints:

• gh has a lot of other jobs to fulfill, and we want to keep our dependency bloat low & final binary size small
• gh at verify is more opinionated than cosign. In addition to verifying the cryptographic signatures, we also restrict the issuer field, force the verification of the SAN, and now enforce a default predicate type for attestations. We feel these steps are necessary for reducing friction and enforcing a certain minimum amount of security.