On Wed, 2025-05-14 at 19:17 +0200, KP Singh wrote:

On Wed, May 14, 2025 at 5:39 PM James Bottomley
[off-list ref] wrote:

quoted

On Sun, 2025-05-11 at 04:01 +0200, KP Singh wrote:

[...]

quoted

quoted

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?

quoted

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