Trying to prove properties about eBPF programs (Clightgen issue)

[swarnpriya]

Hello,

I am a new user and want to use VST to prove properties about eBPF programs (programs written in C that can be used to interact with Linux kernel from user space). Before diving into the actual proofs, I am facing challenges on using Clightgen. As I want to write my own C program and transform them to Clight, I want to use the tool Clightgen. But I am not sure how to install Clightgen tool inside VST. Also, in the coming future I want to use my own version of CompCert (targeting BPF bytecode) instead of the default one (compcert or compcert_new). I would appreciate if someone could share their thoughts of on how to install Clightgen inside VST.

Thanks.

[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: ***@***.***>

[mansky1]

There's been some work on proving termination in the Iris separation logic framework: see for instance https://iris-project.org/pdfs/2019-esop-time.pdf and https://dl.acm.org/doi/pdf/10.1145/3453483.3454031. VST 3.0 is built on Iris, so we might be able to integrate some of these developments, though it'll definitely take some effort!