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

[KP Singh <kpsingh@kernel.org>]

On Wed, May 14, 2025 at 10:32 PM James Bottomley
<James.Bottomley@hansenpartnership.com> wrote:
>
> On Wed, 2025-05-14 at 20:35 +0200, KP Singh wrote:
> > On Wed, May 14, 2025 at 7:45 PM James Bottomley
> > <James.Bottomley@hansenpartnership.com> wrote:
> > >
> > > 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 literally just said it above the hash can be extracted if you
> > really want offline verification. Are you saying this code is hard to
> > write? or is the tooling hard to write? Do you have some definition
> > of "simple cryptographic operations".  All operations use tooling.
>
> As I said, you have a gap in that you not only have to extract the hash
> and verify it against the map (which I agree is fairly simple) but also
> verify the loader program actually checks it correctly.  That latter
> operation is not a simple cryptographic one and represents a security
> gap between this proposal and the hash linked chains you introduced in
> your first email in this thread.

Sure, but I don't see this as being problematic. If it's hard for
folks who do theoretical work, then I think it's okay to push this
effort on them rather than every user.

>
> > > > > 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.
> > >
> >
> > I don't see this as a problem for 2 reasons:
> >
> > 1. It's not hard
>
> it requires disassembling the first 20 or so BPF instructions and
> verifying their operation, so that's harder than simply calculating
> hashes and signatures.
>
> > 2. Your typical user does not want to do formal verification and
> > extract signatures etc.
>
> Users don't want to do formal verification, agreed ... but they do want
> to know that security experts have verified the algorithms they're
> using.
>
> That's why I was thinking, since the loader preamble that verifies the
> hash is easy to construct, that the scheme could use a real hash linked
> chain, which has already been formally verified and is well understood,
> then construct the preamble for the loader you want in a trusted
> environment based on the hashes, meaning there's no security gap.
>
> Regards,
>
> James
>