On Wed, May 14, 2025 at 10:32 PM James Bottomley <james.bottom...@hansenpartnership.com> wrote: > > On Wed, 2025-05-14 at 20:35 +0200, KP Singh 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. > > As I said, you have a gap in that you not only have to extract the hash > and verify it against the map (which I agree is fairly simple) but also > verify the loader program actually checks it correctly. That latter > operation is not a simple cryptographic one and represents a security > gap between this proposal and the hash linked chains you introduced in > your first email in this thread.
Sure, but I don't see this as being problematic. If it's hard for folks who do theoretical work, then I think it's okay to push this effort on them rather than every user. > > > > > > 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 > > it requires disassembling the first 20 or so BPF instructions and > verifying their operation, so that's harder than simply calculating > hashes and signatures. > > > 2. Your typical user does not want to do formal verification and > > extract signatures etc. > > Users don't want to do formal verification, agreed ... but they do want > to know that security experts have verified the algorithms they're > using. > > That's why I was thinking, since the loader preamble that verifies the > hash is easy to construct, that the scheme could use a real hash linked > chain, which has already been formally verified and is well understood, > then construct the preamble for the loader you want in a trusted > environment based on the hashes, meaning there's no security gap. > > Regards, > > James >
