[FEATURE] Rust FFI & C verification boundary

[podhrmic]

Summary

Provide an example of Rust <-> C interface, such that the C portion of the code is verified with CN, and the Rust part is (ideally) verified with Verus (or similar - crux-mir or Kani) (see the use of Verus for seL4 Rust userspace here).

Consider the Rust part trusted while the C portion of code is untrusted. The main issue is marshaling complex datastructures, and tracking their ownership. This example uses vectors.

Ada/SPARK have FFI as well (see docs here), I am expecting that the C code will have similar concerns (ownership and complex data structures).

• add CN specs to the vector example
• consider how would Rust specs (Verus or similar) look like
• document your progress
• explore how (if at all) this approach would be different for Ada/SPARK

Relevant article from google about Rust in Android: https://security.googleblog.com/2024/09/eliminating-memory-safety-vulnerabilities-Android.html?m=1

[spernsteiner]

One interesting candidate for this might be using a Rust implementation of some crypto primitive in the trusted boot or key management component. With crux-mir, it's possible to verify that the Rust implementation is equivalent to a Cryptol spec. We have examples of doing this for SHA256 and ChaCha20/Salsa20 somewhere (though they may be slightly bitrotted at this point).

[podhrmic]

Note to @podhrmic - come up with 3 simple examples, and talk to Satiago about VSPELLs TA3 work