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

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

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.

> > > > 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