Message-ID: <CACYkzJ6hduH4X1wZywodNa3c13QVV=68CmxbpLK1MonuPwPtqw@mail.gmail.com>
Date: Wed, 14 May 2025 20:35:52 +0200
From: KP Singh <kpsingh@...nel.org>
To: James Bottomley <James.Bottomley@...senpartnership.com>
Cc: Paul Moore <paul@...l-moore.com>, bboscaccy@...ux.microsoft.com, bpf@...r.kernel.org, 
	code@...icks.com, corbet@....net, davem@...emloft.net, dhowells@...hat.com, 
	gnoack@...gle.com, herbert@...dor.apana.org.au, jarkko@...nel.org, 
	jmorris@...ei.org, jstancek@...hat.com, justinstitt@...gle.com, 
	keyrings@...r.kernel.org, linux-crypto@...r.kernel.org, 
	linux-doc@...r.kernel.org, linux-kbuild@...r.kernel.org, 
	linux-kernel@...r.kernel.org, linux-kselftest@...r.kernel.org, 
	linux-security-module@...r.kernel.org, llvm@...ts.linux.dev, 
	masahiroy@...nel.org, mic@...ikod.net, morbo@...gle.com, nathan@...nel.org, 
	neal@...pa.dev, nick.desaulniers+lkml@...il.com, nicolas@...sle.eu, 
	nkapron@...gle.com, roberto.sassu@...wei.com, serge@...lyn.com, 
	shuah@...nel.org, teknoraver@...a.com, xiyou.wangcong@...il.com, 
	kysrinivasan@...il.com, Linus Torvalds <torvalds@...ux-foundation.org>
Subject: Re: [PATCH v3 0/4] Introducing Hornet LSM

On Wed, May 14, 2025 at 8:35 PM KP Singh <kpsingh@...nel.org> wrote:
>
> On Wed, May 14, 2025 at 7:45 PM James Bottomley
> <James.Bottomley@...senpartnership.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@...senpartnership.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.
>
> >
> > >
> > > > 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
> 2. Your typical user does not want to do formal verification and
> extract signatures etc.
>
> [1] alone is enough.
>
> The key user journey is:
>
> * Build the program and the metadata
> * Sign the blob once (as explained)
> * A simple API to verify the sequence of operations.
>
> The user builds a program and signs the blob, they sign it because it
> contains the hash of the metadata. It seems like you are optimizing
> for the formal researcher but not for the tooling. The user just needs

I meant not for the user.

> good tooling and a simple API which is exactly what was proposed.
>
> - KP
>
> > Regards,
> >
> > James
> >
> >

Powered by blists - more mailing lists