Re: [PATCH v3 0/4] Introducing Hornet LSM

[James Bottomley <James.Bottomley@HansenPartnership.com>]

On Wed, 2025-05-14 at 19:17 +0200, KP Singh wrote:
> On Wed, May 14, 2025 at 5:39 PM James Bottomley
> <James.Bottomley@hansenpartnership.com> wrote:
> > On Sun, 2025-05-11 at 04:01 +0200, KP Singh wrote:
[...]
> > > This implicitly makes the payload equivalent to the signed block
> > > (B_signed)
> > > 
> > >     I_loader || H_meta
> > > 
> > > bpftool then generates the signature of this I_loader payload
> > > (which now contains the expected H_meta) using a key (system or
> > > user) with new flags that work in combination with bpftool -L
> > 
> > Could I just push back a bit on this.  The theory of hash chains
> > (which I've cut to shorten) is about pure data structures.  The
> > reason for that is that the entire hash chain is supposed to be
> > easily independently verifiable in any environment because anything
> > can compute the hashes of the blocks and links.  This independent
> > verification of the chain is key to formally proving hash chains to
> > be correct.  In your proposal we lose the easy verifiability
> > because the link hash is embedded in the ebpf loader program which
> > has to be disassembled to do the extraction of the hash and verify
> > the loader is actually checking it.
> 
> I am not sure I understand your concern. This is something that can
> easily be built into tooling / annotations.
> 
>     bpftool -S -v <verification_key> <loader> <metadata>
> 
> Could you explain what's the use-case for "easy verifiability".

I mean verifiability of the hash chain link.  Given a signed program,
(i.e. a .h file which is generated by bpftool) which is a signature
over the loader only how would one use simple cryptographic operations
to verify it?


> 
> > I was looking at ways we could use a pure hash chain (i.e.
> > signature over loader and real map hash) and it does strike me that
> > the above ebpf hash verification code is pretty invariant and easy
> > to construct, so it could run as a separate BPF fragment that then
> > jumps to the real loader.  In that case, it could be constructed on
> > the fly in a trusted environment, like the kernel, from the link
> > hash in the signature and the signature could just be Sig(loader ||
> > map hash) which can then be
> 
> The design I proposed does the same thing:
> 
>     Sig(loader || H_metadata)
> 
> metadata is actually the data (programs, context etc) that's passed
> in the map. The verification just happens in the loader program and
> the loader || H_metadata is implemented elegantly to avoid any
> separate payloads.

OK, so I think this is the crux of the problem:  In formal methods
proving the validity of a data based hash link is an easy set of
cryptographic operations.  You can assert that's equivalent to a
signature over a program that verifies the hash, but formally proving
it requires a formal analysis of the program to show that 1) it
contains the correct hash and 2) it correctly checks the hash against
the map.  That makes the task of someone receiving the .h file
containing the signed skeleton way harder: it's easy to prove the
signature matches the loader instructions, but they still have to prove
the instructions contain and verify the correct map hash.

Regards,

James