tommygain
@tommygain
D

Математически доказанная безопасность Rust — это как?

Здравствуйте.

Недавно увидел сентенцию, мол, "безопасность Rust имеет математическое обоснование". Кто-нибудь может подсказать, о чем идет речь?
  • Вопрос задан
  • 278 просмотров
Решения вопроса 1
Tyranron
@Tyranron
Процитирую humbug из комментов к недавней статье:

Конкретно в https://people.mpi-sws.org/~dreyer/papers/rustbelt... формально доказывается, что система типов Раста, владение, заимствование и прочее — корректны. Доказывается, что программа безопасна, если написана на безопасном подмножестве Раст. Доказывается, что программа безопасна, если в ней есть вкрапления unsafe, в которых программист не допустил ошибки, UB.

Кроме того, проект RustBelt на текущем этапе занимается формальной верификацией библиотеки std, но полная проверка требует времени. Поэтому библиотеку проверяют по кускам. Да, были найдены и исправлены 2 ошибки в unsafe коде (что показывает, что ребята делом занимались), тем не менее все эти thread, mutex, Arc/Rc формально безопасны.


Собственно, сами математические доказательства смотрите в научных публикациях:
RustBelt: Securing the Foundations of the Rust Pro...
KRust: A Formal Executable Semantics of Rust
K-Rust: An Executable Formal Semantics for Rust

Сайт проекта RustBelt: plv.mpi-sws.org/rustbelt
Ответ написан
Пригласить эксперта
Ваш ответ на вопрос

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы
от 80 000 до 220 000 руб.
Click Санкт-Петербург
от 170 000 до 200 000 руб.
Fundraise Up Санкт-Петербург
от 170 000 руб.
20 мая 2019, в 17:23
3000 руб./за проект
20 мая 2019, в 15:59
300 руб./за проект
20 мая 2019, в 15:24
1300 руб./в час