Trying to prove properties about eBPF programs (Clightgen issue)

[swarnpriya]

Trying to prove properties about eBPF programs (Clightgen issue)

[mansky1]

Hi! I'm excited to hear that you're interested in this topic; I've been thinking about looking into eBPF verification myself recently. VST doesn't ship with Clightgen for copyright reasons, so you should install CompCert separately (if you're using OPAM, this is as simple as opam install coq-compcert; otherwise, you can download it from compcert.org and build it from source) to get access to Clightgen. If you just want to apply VST to the generated programs, that's all you need to do; if you're looking at building VST from source or modifying it, see the build instructions for how to build VST on top of an external CompCert installation. Please let me know if you run into any more questions or problems, and more generally, I'd love to hear how your project progresses!

Best,
William

[swarnpriya]

Thank you William @mansky1 for the response. I solved the issue of Clightgen. I still need to figure out how to configure VST with my version of CompCert that targets BPF bytecode instead of x86 or ARM. I will keep you posted about my progress and once I get myself familiar with using VST, we can chat more.
On another note, I have worked with Coq proof assistant in several projects. How difficult is the learning curve for VST and do you have some suggestions about any other good document to follow apart from Software Foundation and the VerifiableC manual.

[mansky1]

VST works on the Clight output of Clightgen, so the question is whether your modified CompCert does something different at the Clight level or only further down the chain.

I think VST is not too bad to learn if you work through the Verifiable C volume of Software Foundations (as distinct from the manual, which is quite hard to learn from if you don't already understand VST). But if you have questions, we do have a VST-user mailing list.

[swarnpriya]

Can we reason about termination in VST? If yes, is there any specific example or papers you have in mind that would give me some better understanding about how it does? I am still wondering that proving functional correctness for eBPF programs won't be enough as we need to deal with helper functions properties and properties like termination, stack usage etc.

[andrew-appel]

We cannot reason about termination in VST.

[Salamari]

Even from a theoretical standpoint, it's not clear the models in VST can reason about termination. The only work that was done in this direction was a paper that Rob Dockins and I wrote many years ago, "Verifying Time Bounds for General Function Pointers", published in MFPS 2012 I believe. We tried to prove total correctness, and ended up proving explicit time bounds (which are really a kind of partial correctness). In any event, it's not an easy problem. Aquinas

…

________________________________ From: Andrew Appel ***@***.***> Sent: Monday, September 2, 2024 7:31 PM To: PrincetonUniversity/VST ***@***.***> Cc: Subscribed ***@***.***> Subject: Re: [PrincetonUniversity/VST] Trying to prove properties about eBPF programs (Clightgen issue) (Issue #792) ⚠ Caution: External sender We cannot reason about termination in VST. — Reply to this email directly, view it on GitHub<#792 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ACAMK5A27FZ4P67VUMFZOQDZUSVHFAVCNFSM6AAAAABNEJ5ZIGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMRVGE4DMMRRHA>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>