search

dslab-epfl / klint

Repository for the "Automated Verification of Network Function Binaries" paper (NSDI'22).
MIT License
8 stars 5 forks source link

Proper BPF support? #11

Open SolalPirelli opened 1 year ago

SolalPirelli commented 1 year ago

@tharvik in case that's in line with the C4DT's priorities, having Klint work on BPF programs directly (not the hacky stuff from the paper) might be a good showcase.

A student had almost finished BPF ISA support for angr in a semester project with me, but some issues cropped up in the actual PR and I guess there wasn't time after the semester to finish it. Maybe it can be resurrected? https://github.com/angr/angr-platforms/pull/46

tharvik commented 1 year ago

BPF programs might be a good showcase.

Good idea, I'll check with the hierachy :)

Hoo, a bunch of existing programs to try klint on: https://github.com/zoidbergwill/awesome-ebpf#examples Correct me if I'm wrong, there is (or was) support for eBPF Maps in code?

SolalPirelli commented 1 year ago

There was indeed, IIRC the main difference from Klint's map_* stuff is that BPF maps copy keys and values rather than partially owning key poiners.

tharvik commented 1 year ago

quick update: the hierarchy validated :partying_face:

tharvik commented 1 year ago

support for eBPF in angr is in progress at https://github.com/angr/angr-platforms/pull/55

SolalPirelli commented 1 year ago

@tharvik any news on this?

tharvik commented 1 year ago

upstream isn't really proactive, I bumped them, hopefully we'll have some news this week.

anyway, the PR is working (minus relocation & some specials instructions), feel free to use it, I'm happy to help with/fix any issue you might encounter.

SolalPirelli commented 1 year ago

I see the PR was merged 🎉 I guess angr-platforms should become a dependency of klint now? I don't know how the packaging of it works (so that we can point Klint to an ebpf binary and it "just works")

tharvik commented 1 year ago

yeah, it took a while but it finally landed :partying_face:

I guess angr-platforms should become a dependency of klint now?

yep, it's quite easy in fact. as each angr arch register itself on import, you simply have to import angr_platforms.ebpf to support it. and for the dep itself, it seems that it's not available via pip.. but you can depend on its git by adding a "angr-platforms @ git+https://github.com/angr/angr-platforms.git" item in the dependencies' array.