gh at verify evaluates policy transparently and monotonically #9850

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.