Mathematically proven security of Rust

F

First Name Last Name2019-01-19 00:22:50

Rust

First Name Last Name, 2019-01-19 00:22:50

Mathematically proven security of Rust - how is it?

Hello.
Recently I saw a maxim, they say, "Rust's security has a mathematical justification." Can anyone suggest what is it about?

Reply

Answer the question

In order to leave comments, you need to log in

2 answer(s)

T

Tyranron, 2019-01-19
@tommygain

To quote humbug from the comments on a recent article :

Specifically, https://people.mpi-sws.org/~dreyer/papers/rustbelt... formally proves that Rust's type system, ownership, borrowing, etc. are correct. It is proved that the program is secure if it is written in a secure subset of Rust. It is proved that a program is safe if it contains unsafe inclusions in which the programmer did not make a mistake, UB.
In addition, the RustBelt project is currently formally verifying the std library, but full verification takes time. Therefore, the library is checked piece by piece. Yes, 2 errors were found and fixed in the unsafe code (which shows that the guys were doing their job), nevertheless, all these threads, mutex, Arc / Rc are formally safe.

Actually, see the mathematical proofs themselves in scientific publications:
RustBelt: Securing the Foundations of the Rust Pro...
KRust: A Formal Executable Semantics of Rust
K-Rust: An Executable Formal Semantics for Rust
RustBelt project site: plv.mpi-sws. org/rustbelt

Y

Yo JLa, 2019-07-27
@blanger

There is a working group, when will the results be available? Probably not
fast .