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:
> [...]
> > >
> > For this specific BPF case, we will directly sign a composite of the
> > first message and the hash of the second. Let H_meta = H(M_metadata).
> > The block to be signed is effectively:
> >
> > B_signed = I_loader || H_meta
> >
> > The signature generated is Sig(B_signed).
> >
> > The process then follows a similar pattern to the Alice and Bob
> > model,
> > where the kernel (Bob) verifies I_loader and H_meta using the
> > signature. Then, the trusted I_loader is responsible for verifying
> > M_metadata against the trusted H_meta.
> >
> > From an implementation standpoint:
> >
> > # Build
> >
> > bpftool (or some other tool in the user's build environment) knows
> > about the metadata (M_metadata) and the loader program (I_loader). It
> > first calculates H_meta = H(M_metadata). Then it constructs the
> > object
> > to be signed and computes the signature:
> >
> > Sig(I_loader || H_meta)
> >
> > # Loader
> >
> > bpftool generates the loader program. The initial instructions of
> > this loader program are designed to verify the SHA256 hash of the
> > metadata (M_metadata) that will be passed in a map. These
> > instructions effectively embed the precomputed H_meta as immediate
> > values.
> >
> > ld_imm64 r1, const_ptr_to_map // insn[0].src_reg ==
> > BPF_PSEUDO_MAP_IDX
> > r2 = *(u64 *)(r1 + 0);
> > ld_imm64 r3, sha256_of_map_part1 // constant precomputed by
> > bpftool (part of H_meta)
> > if r2 != r3 goto out;
> >
> > r2 = *(u64 *)(r1 + 8);
> > ld_imm64 r3, sha256_of_map_part2 // (part of H_meta)
> > if r2 != r3 goto out;
> >
> > r2 = *(u64 *)(r1 + 16);
> > ld_imm64 r3, sha256_of_map_part3 // (part of H_meta)
> > if r2 != r3 goto out;
> >
> > r2 = *(u64 *)(r1 + 24);
> > ld_imm64 r3, sha256_of_map_part4 // (part of H_meta)
> > if r2 != r3 goto out;
> > ...
> >
> > 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 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.
> easily verified without having to disassemble ebpf code. So we get the
> formal provability benefits of using a real hash chain while still
> keeping your verification in BPF.
>
> Regards,
>
> James
>
>
