On Wed, May 14, 2025 at 8:35 PM KP Singh kpsingh@kernel.org 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_metabpftool 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:
- It's not hard
- 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