Re: [Rats] Questions about Horn Clauses and CORIM

[Dionna Amalie Glaze <[e-mail]>]

+rats

On Wed, Apr 10, 2024 at 6:11 AM Muhammad Usama Sardar
<[e-mail]> wrote:
>
> Hi Dionna,
>
> I hope you are doing well. We missed you at the EuroProofNet event. Hope we can meet at some future conferences.
>
> At the IETF 119, Ned presented the "Horn Scalability Clauses" which I believe is actually "Scalability of Horn Clauses" but the question is where do Horn Clauses come from. I was informed that Ned is currently on sabbatical until end of April. You seem to be the next most knowledgeable person on the topic. So in the mean time, I was wondering if you have answers to some preliminary questions:
>
>   * How are "Horn clauses" relevant to the CoRIM draft? I don't fully
>     understand the link of the CoRIM draft to Horn clauses.

Let's say we have a Verifier that has access to a database of supply
chain-provided CoRIM documents. Some of these documents include
conditional endorsement triples. The antecedents are stateful
environment maps, so there are specific claims that need to be present
in order to introduce the consequents into the accepted claim set.

[E, x0 ^ .... ^ xn] => [E, y0 ^ ... ^ ym]
[E, y1 ^ y3] => [E, z0 ^ ... ^ zk]

When this is your model, and you need to match your current accepted
claim set against a database of conditionals, is horn clause
resolution. You can match, extend, match more, extend more, etc.

(aside, which is a limitation of the current draft)
Accepted claim sets are only with respect to the profile under which
the claims are made, otherwise vendor-specific indices get
misinterpreted, or digests apply to the wrong context, etc. This makes
it particularly difficult to say that your environment or component of
your environment has been tested against a particular test suite, as
those would be different profiles–one about your test suite claims,
and one about reference values for the attester's form of evidence.
When what is known is for profile X (measured value Y authorized by Z)
can't be used in antecedents for profile W (reference value Y passed
test suite U), it's unclear how we can bind X/Y meaning in the W/Y
antecedent with the current spec.

Binding scope is hard.

>   * How are the Horn clauses generated?

CoRIM issuers create conditional endorsement triples.

>   * What are the assumptions/facts?

Stateful environment maps, which are environments plus claims that
need to be known about those environments.

>   * Which rule engine do you plan to use to analyze the Horn clauses?
>

I don't have any such rule engine in mind, since our use case does not
depend on such a complicated mechanism. I think Andrew Draper has the
endorsement use case. Veraison has its own boolean constraint
propagation system that I haven't inspected myself.

> Thanks in advance,
>
> Usama



-- 
-Dionna Glaze, PhD, CISSP (she/her)