On Wed, May 14, 2025 at 8:35 PM KP Singh <kpsi...@kernel.org> wrote: > > On Wed, May 14, 2025 at 7:45 PM James Bottomley > <james.bottom...@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.bottom...@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. > > > > > > > > > > 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 > > > >
