static analysis +formal verification of rbpf

[shenghaoyuan]

Hello,
This is not a regular issue but more like some suggestions.

I have some plans to improve the current rbpf vm, I would like to know if the rbpf community is also interested in those topics.

• do some dataflow analysis based on the existing static_analysis.rs (e.g. the verified C Compiler CompCert 's Kildall algorithm), and integrates into the verifier workflow
• or enhance the current verifier.rs following the Linux eBPF verifier (e.g. the value tracking), plus some formal verification efforts on the new verifier.

[Lichtso]

Yes, we are interested in expanding static analysis, especially using BTF (see solana-labs/solana#29863), but never got around implementing it.

Furthermore, there is also interest in porting the program verifier to BPF itself, so that it can be deployed on-chain.

[shenghaoyuan]

thx, I got it. I will feedback here once I make some progress