Hacker News Reader

Thanks for your interesting work! I wanted to ask, how are FFI boundaries handled? Are they ignored or is it an error to call FFI functions?

View on HN

Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods.

In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of abstraction might differ. It might be necessary to prove program refinement, for example.

Sounds really exciting! Mir interpreter has the same limitation. Have you examined incorporating mir in your analysis?

Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.

Reply on news.ycombinator.com