3 ms·

I told Yannick at AdaCore that getting parity with Rust's borrow-checker was critical given SPARK was otherwise the champ of highly-assured, system code. He sai

I told Yannick at AdaCore that getting parity with Rust's borrow-checker was critical given SPARK was otherwise the champ of highly-assured, system code. He said someone was working on something like that. I appreciate the tip from touisteur about this work because it's awesome! This is also potentially a boost for my Brute-Force Assurance concept of doing versions of same code in multiple languages to leverage their verification tooling, esp automated. One obstacle was mismatch between Rust's pointers with borrow-checker and SPARK's lack of them. Bringing them closer together might let one use SPARK to model unsafe code in Rust to prove its safety. Other languages, too.

touisteur 9y ago
By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2017-November/001444.html http://lists.forge.open-do.org/pipermail/spark2014-discuss/2... Lots of links to recent stuff, you should look it all... If you have the time :-D.
adrianN 9y ago
Modelling Rust's unsafe code seems pretty hard to me as afaik there are no formal semantics for Rust.
- nickpsecurity 9y ago
  In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
- touisteur 9y ago
  I guess people will try anyway : https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... There's some great work on this front coming from the Rustbelt lab : https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf and http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/

touisteur 9y ago

By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2017-November/001444.html http://lists.forge.open-do.org/pipermail/spark2014-discuss/2... Lots of links to recent stuff, you should look it all... If you have the time :-D.

adrianN 9y ago

Modelling Rust's unsafe code seems pretty hard to me as afaik there are no formal semantics for Rust.

nickpsecurity 9y ago
In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
touisteur 9y ago
I guess people will try anyway : https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... There's some great work on this front coming from the Rustbelt lab : https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf and http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/