static analysis +formal verification of rbpf

shenghaoyuan commented 1 month ago

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 commented 4 weeks ago

Yes, we are interested in expanding static analysis, especially using BTF (see https://github.com/solana-labs/solana/issues/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 commented 3 weeks ago

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

solana-labs / rbpf