forum.opennet.ru - "Инициатива по верификации стандартной библиотеки Rust" (33)

"Инициатива по верификации стандартной библиотеки Rust"

Форум Разговоры, обсуждение новостей
Вариант для распечатки		Пред. тема \| След. тема
Изначальное сообщение		[ Отслеживать ]

"Инициатива по верификации стандартной библиотеки Rust"	+/–
Сообщение от opennews (??), 24-Ноя-24, 11:53
Компания Amazon и организация Rust Foundation представили инициативу, нацеленную на повышение безопасности стандартной библиотеки языка Rust. Целью заявлена проверка надёжности и безопасности функций, в которых используется ключевое слово "unsafe", допускающее операции, небезопасно работающие с памятью, такие как разыменование указателей, изменение статических переменных и обращение к внешним библиотекам на С/C++. Отмечается, что в настоящее время стандартная библиотека Rust насчитывает около 35 тысяч функций, из которых в 7500 встречаются блоки кода, выполняемые в контексте "unsafe". За последние три года в библиотеке было выявлено 57 проблем с корректностью работы, из которых 20 были помечены как уязвимости... Подробнее: https://www.opennet.dev/opennews/art.shtml?num=62286
Ответить \| Правка \| Cообщить модератору

Оглавление

Как же так Ведь Rust должен был обернуть небезопасные части в загончик unsafe, , Аноним (1), 11:53 , 24-Ноя-24, (1) –2

Так они это и сделали Поэтому проблемы если возникают, то именно unsafe блоках , Аноним (-), 11:57 , 24-Ноя-24, (3) +7

А вот это вряд ли, потому что каждое включение unsafe на Rust в 5 раз сложнее пр, Аноним (8), 12:23 , 24-Ноя-24, (8) –2

Как вычислялась эта метрика , Facemaker (?), 12:24 , 24-Ноя-24, (9) +1

Методика Пальцем в небо сертифицированного сотрудника НИИ Кекспертизы и вброс, Аноним (-), 12:37 , 24-Ноя-24, (12) +5

В чем отличие safe rust от обычной сишки , Аноним (35), 14:23 , 24-Ноя-24, (35)

Нет Ровно наоборот Даже если иметь кривые руки, плохую голову и что-то натянуть, erthink_ (?), 13:15 , 24-Ноя-24, (21)

в другом языке есть формально верифицированный компиляторhttps compcert orgа у, Аноним (13), 12:39 , 24-Ноя-24, (13)

Нисколько не хочу принизить ценность проекта и достигнутые там результаты, но вс, erthink_ (?), 13:56 , 24-Ноя-24, (28)

https github com Speykious cve-rs - в фантазиях Нет, это столько же работы, то, 21yosenior (?), 12:52 , 24-Ноя-24, (16)

Вот эпичный тред, где люди в течение недели пытались заставить это работатьht, Аноним (-), 14:21 , 24-Ноя-24, (33)

Не знаю, что ты там компилируешь code cargo install cve-rs cargo bin cve-, Аноним (35), 14:30 , 24-Ноя-24, (36)

Нет ничего иделаьного А результат всяко лучше по сравнению с С C , Аноним (6), 12:03 , 24-Ноя-24, (6) –1
А теперь представим что unsafe нет, и нужно перелопатить 35к функций, вместо 750, proninyaroslav (ok), 12:04 , 24-Ноя-24, (7)

Там и так нужно перелопатить 35к, уб в расте есть везде Не говоря о том, что мн, 21yosenior (?), 12:48 , 24-Ноя-24, (15)

UB в расте не может быть за пределами unsafe блока Это гарантированно Все оста, proninyaroslav (ok), 12:59 , 24-Ноя-24, (18) +1

Эти гарантии уже умножены на ноль Кидал ссылку ниже , 21yosenior (?), 13:23 , 24-Ноя-24, (22)
Скрыто модератором, Аноним (34), 14:21 , 24-Ноя-24, (34) +1

Unsafe был введён более пяти лет назад https github com rust-lang rust commit, ijuij (?), 12:02 , 24-Ноя-24, (5)

Верифицируют библиотеку, а не unsafe , Аноним (34), 14:15 , 24-Ноя-24, (31)

https github com Speykious cve-rs - там уб в сейфе, толку валидировать ансейф , 21yosenior (?), 12:46 , 24-Ноя-24, (14) +1

Ага, со своей версий transmute Из стандартной библиотеки не подошла https g, Карлос Сношайтилис (ok), 12:58 , 24-Ноя-24, (17) +1

Хоть со своей, хоть с чьей-то ещё Заявляется безопасность кода на языке, а не л, 21yosenior (?), 13:08 , 24-Ноя-24, (19)

Кекспертизм опеннетный, аз изДа и то, что для появления проблем т е чтобы найт, Аноним (23), 13:35 , 24-Ноя-24, (23)

Всё, ответов не будет С одного вопроса потеряться - мощно Молодец, умножил на н, 21yosenior (?), 13:44 , 24-Ноя-24, (26)

Не суметь прочесть три предложения и сразу перейти к папа, где море - намного, Аноним (23), 14:15 , 24-Ноя-24, (32)

Скрыто модератором, 21yosenior (?), 14:36 , 24-Ноя-24, (37)

Только один вопрос Кто им разрешил , Аноним (20), 13:14 , 24-Ноя-24, (20)

А кто запрещал , nume (ok), 13:41 , 24-Ноя-24, (24)
Хороший вопрос Иногда кажется, что разрешение не требуется , ijuij (?), 13:54 , 24-Ноя-24, (27)

Инициатива наказуема , Аноним (29), 13:59 , 24-Ноя-24, (29)
Скрыто модератором, Аноним (34), 14:04 , 24-Ноя-24, (30)
Как насчет верификации хлама, который cargo тащит из-за бугра , Аноним (38), 14:37 , 24-Ноя-24, (38)

Сообщения [Сортировка по времени | RSS]

1. "Инициатива по верификации стандартной библиотеки Rust" –2 +/–

Сообщение от Аноним (1), 24-Ноя-24, 11:53

> При этом за последние три года в библиотеке было выявлено 57 проблем с корректностью работы, из которых 20 были помечены как уязвимости.
Как же так? Ведь Rust должен был обернуть небезопасные части в загончик unsafe, чтобы как раз не было такого.
Выходит, не помогло? А верифицировать любой код можно, не только Rust.

Ответить | Правка | Наверх | Cообщить модератору

3. "Инициатива по верификации стандартной библиотеки Rust" +7 +/–

Сообщение от Аноним (-), 24-Ноя-24, 11:57

> Ведь Rust должен был обернуть небезопасные части в загончик unsafe, чтобы как раз не было такого.
Так они это и сделали. Поэтому проблемы если возникают, то именно unsafe блоках.
Не считая логических багов. От них только формальная верификация и спасет.
> Выходит, не помогло?
Наоборот, помогло. Посмотри сколько функций и в скольки есть unsafe.
> А верифицировать любой код можно, не только Rust.
Можно. Но в расте тебе нужно будет верифицировать 7.5к функция, а не 35 тысяч как в других языках.
А это почти в 5 раз меньше работы.

Ответить | Правка | Наверх | Cообщить модератору

8. "Инициатива по верификации стандартной библиотеки Rust" –2 +/–

Сообщение от Аноним (8), 24-Ноя-24, 12:23

>А это почти в 5 раз меньше работы.
А вот это вряд ли, потому что каждое включение unsafe на Rust в 5 раз сложнее проверять, чем в других языках.

Ответить | Правка | Наверх | Cообщить модератору

9. "Инициатива по верификации стандартной библиотеки Rust" +1 +/–

Сообщение от Facemaker (?), 24-Ноя-24, 12:24

>каждое включение unsafe на Rust в 5 раз сложнее проверять, чем в других языках
Как вычислялась эта метрика?

Ответить | Правка | Наверх | Cообщить модератору

12. "Инициатива по верификации стандартной библиотеки Rust" +5 +/–

Сообщение от Аноним (-), 24-Ноя-24, 12:37

> Как вычислялась эта метрика?
Методика 'Пальцем в небо' сертифицированного сотрудника 'НИИ Кекспертизы и вбросов' им. Опеннета.
Все утверждения истинны на 146%!
Я бы спросил в чем отличие unsafe rust от обычной сишки, но смысла нет - все равно ответа не получим))

Ответить | Правка | Наверх | Cообщить модератору

35. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (35), 24-Ноя-24, 14:23

В чем отличие safe rust от обычной сишки?

Ответить | Правка | Наверх | Cообщить модератору

21. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от erthink_ (?), 24-Ноя-24, 13:15

Нет. Ровно наоборот.
Даже если иметь кривые руки, плохую голову и что-то натянуть против раста, то верификация unsafe в его собственных библиотеках потребует в разы меньше усилий чем верификация сишных библиотек со сравнимым функционалом.
В среднем по больнице, unsafe-код в Rust более регулярен и проще (менее комплексный) чем подобный в сишных библиотеках.
Есть и обратный эффект, в unsafe-функциях концентрация странностей/мутностей больше чем в средней glibc. Но это только потому, что в rust есть возможность и стремление отделять мух от котлет, а в glibc любые unsafe операции могут быть в любом месте (в самом безобидном и неожиданном).
Конечно, можно найти зубодробительные unsafe-сценарии, но тогда и сравнивать их надо с аналогичными сишными случаями.

Ответить | Правка | К родителю #8 | Наверх | Cообщить модератору

13. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (13), 24-Ноя-24, 12:39

> Но в расте тебе нужно будет верифицировать 7.5к функция, а не 35 тысяч как в других языках.
в другом языке есть формально верифицированный компилятор
https://compcert.org
а у раста пока что даже не формализовали ситему типов
https://blog.rust-lang.org/2023/01/20/types-announcement.html

Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

28. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от erthink_ (?), 24-Ноя-24, 13:56

> в другом языке есть формально верифицированный компилятор
> https://compcert.org
Нисколько не хочу принизить ценность проекта и достигнутые там результаты, но всё-таки нужно слегка критично читать написанное с осознанием всего комплекса проблем/задач.
Формальная/математическая верификация покрывает часть функционала, т.е. "не всё".
При этом возникает некая проблема/задача верификации "самого верификатора", т.е. доказательства что сформированного списка свойств достаточно для "верифицированного компилятора".
Например, предположим что у вас есть "верифицированный компилятор". В нём могут быть баги ?
- если "нет, багов быть не может", то упомянутый компилятор нельзя назвать верифицированным.
- если "да, баги могут быть", то верификация перестаёт что-либо гарантировать на практике.
Поэтому все подобные верификации всегда с массой уточнений и оговорок "тут рыбу заворачивали, сюда не смотрим" и "если остальное работает верно".
Соответственно, отсутствие "формализированной системы типов" им не только не мешает, но и может помогать (сокращать поверхность).

Ответить | Правка | Наверх | Cообщить модератору

16. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 12:52

> Поэтому проблемы если возникают, то именно unsafe блоках.
https://github.com/Speykious/cve-rs - в фантазиях.
> А это почти в 5 раз меньше работы.
Нет, это столько же работы, точнее даже больше. Сейф раст ничего не гарантирует.

Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

33. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (-), 24-Ноя-24, 14:21

Вот эпичный тред, где люди в течение недели(!) пытались заставить это работать
https://github.com/Speykious/cve-rs/issues/4
Им пришлось написать самописный null_mute, модифицировать transmute() подменив там crate::null_mut на самописный... и даже после этого получается ошибка компиляции
error[E0133]: dereference of raw pointer is unsafe and requires unsafe function or block
error: could not compile `cve-rs` (lib) due to previous error

Ответить | Правка | Наверх | Cообщить модератору

36. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (35), 24-Ноя-24, 14:30

Не знаю, что ты там компилируешь?

$ cargo install cve-rs
$ ~/.cargo/bin/cve-rs segfault
Segmentation fault (core dumped)

Ответить | Правка | Наверх | Cообщить модератору

6. "Инициатива по верификации стандартной библиотеки Rust" –1 +/–

Сообщение от Аноним (6), 24-Ноя-24, 12:03

Нет ничего иделаьного! А результат всяко лучше по сравнению с С/C++.

Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

7. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от proninyaroslav (ok), 24-Ноя-24, 12:04

А теперь представим что unsafe нет, и нужно перелопатить 35к функций, вместо 7500 если бы unsafe был.

Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

15. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 12:48

Там и так нужно перелопатить 35к, уб в расте есть везде. Не говоря о том, что многие из этих 35к - хэлворды.

Ответить | Правка | Наверх | Cообщить модератору

18. "Инициатива по верификации стандартной библиотеки Rust" +1 +/–

Сообщение от proninyaroslav (ok), 24-Ноя-24, 12:59

UB в расте не может быть за пределами unsafe блока. Это гарантированно. Все остальное он конечно не гарантирует, например утечки памяти.

Ответить | Правка | Наверх | Cообщить модератору

22. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 13:23

Эти гарантии уже умножены на ноль. Кидал ссылку ниже.

Ответить | Правка | Наверх | Cообщить модератору

34. Скрыто модератором +1 +/–

Сообщение от Аноним (34), 24-Ноя-24, 14:21

>Это гарантированно.
Кем или чем?

Ответить | Правка | К родителю #18 | Наверх | Cообщить модератору

5. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от ijuij (?), 24-Ноя-24, 12:02

Unsafe был введён более пяти лет назад (https://github.com/rust-lang/rust/commit/10855a36b53d33aa2e4...), и за это время люди успели использовать этот ключевое слово в множестве проектов. Однако только сейчас они начали заниматься его верификацией. Ну что ж, подход к безопасности действительно "на высшем уровне".

Ответить | Правка | Наверх | Cообщить модератору

31. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (34), 24-Ноя-24, 14:15

Верифицируют библиотеку, а не unsafe.

Ответить | Правка | Наверх | Cообщить модератору

14. "Инициатива по верификации стандартной библиотеки Rust" +1 +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 12:46

https://github.com/Speykious/cve-rs - там уб в сейфе, толку валидировать ансейф.

Ответить | Правка | Наверх | Cообщить модератору

17. "Инициатива по верификации стандартной библиотеки Rust" +1 +/–

Сообщение от Карлос Сношайтилис (ok), 24-Ноя-24, 12:58

Ага, со своей версий transmute. Из стандартной библиотеки "не подошла".
https://github.com/Speykious/cve-rs/blob/main/src/transmute.rs

Ответить | Правка | Наверх | Cообщить модератору

19. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 13:08

Хоть со своей, хоть с чьей-то ещё. Заявляется безопасность кода на языке, а не либы - подучи логику. Ансейфа нет, проблемы есть.

Ответить | Правка | Наверх | Cообщить модератору

23. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (23), 24-Ноя-24, 13:35

>> cve-rs also contains safe reimplementations of:
>> std::mem::transmute
>> std::ptr::null()/null_mut() but for references
>>> pub const unsafe extern "rust-intrinsic" fn transmute<Src, Dst>
>>> Reinterprets the bits of a value of one type as another type.
> Хоть со своей, хоть с чьей-то ещё. Заявляется безопасность кода на языке,
> а не либы - подучи логику. Ансейфа нет, проблемы есть.
Кекспертизм опеннетный, аз из
Да и то, что для появления проблем (т.е. чтобы найти баг в компиляторе - ведь "работатет" оно только с кастомным null/transmute) там целый консилиум корпел не одну неделю (см. обсуждение на гитхабе) - кексперты скромненько умалчивают.
И правда, какая разница: заиметь UB после траха^W написания кастомного null и принудительного каста типа данных - или заиметь UB, просто сложив два числа или забыв пустую строку в конце исходника ...

Ответить | Правка | Наверх | Cообщить модератору

26. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 13:44

Всё, ответов не будет? С одного вопроса потеряться - мощно.
> cve-rs also contains safe reimplementations of
> safe reimplementations
Молодец, умножил на ноль тезисы предыдущего героя. Хоть не зря кучу левого мусора спастил.

Ответить | Правка | Наверх | Cообщить модератору

32. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (23), 24-Ноя-24, 14:15

> Всё, ответов не будет? С одного вопроса потеряться - мощно.
Не суметь прочесть три предложения и сразу перейти к "папа, где море?" - намного уныл^W мощнее.
>> cve-rs also contains safe reimplementations of
>> safe reimplementations
> Молодец, умножил на ноль тезисы предыдущего героя. Хоть не зря кучу левого мусора спастил.
Молодец, обозвал сигнатуру transmute "левым мусором" и не сумел написать ничего по существу ... зато выдал хороший, объемный выхлоп метана - Газпром гордится тобой!

Ответить | Правка | Наверх | Cообщить модератору

37. Скрыто модератором +/–

Сообщение от 21yosenior (?), 24-Ноя-24, 14:36

Ну так что, ты осилишь мне что-то возразить, клоун? Или спастить рандомный мусор и делать вид якобы что-то опроверг - твой потолок?

Ответить | Правка | Наверх | Cообщить модератору

20. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (20), 24-Ноя-24, 13:14

> Компания Amazon и организация Rust Foundation представили инициативу
Только один вопрос. Кто им разрешил?

Ответить | Правка | Наверх | Cообщить модератору

24. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от nume (ok), 24-Ноя-24, 13:41

А кто запрещал?

Ответить | Правка | Наверх | Cообщить модератору

27. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от ijuij (?), 24-Ноя-24, 13:54

Хороший вопрос! Иногда кажется, что разрешение не требуется.

Ответить | Правка | К родителю #20 | Наверх | Cообщить модератору

29. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (29), 24-Ноя-24, 13:59

Инициатива наказуема.

Ответить | Правка | Наверх | Cообщить модератору

30. Скрыто модератором +/–

Сообщение от Аноним (34), 24-Ноя-24, 14:04

Чиновники предлагают поработать за грамотку.

Ответить | Правка | Наверх | Cообщить модератору

38. "Инициатива по верификации стандартной библиотеки Rust" +/–

Сообщение от Аноним (38), 24-Ноя-24, 14:37

Как насчет верификации хлама, который cargo тащит из-за бугра?

Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру

1. "Инициатива по верификации стандартной библиотеки Rust"	–2 +/–
Сообщение от Аноним (1), 24-Ноя-24, 11:53
> При этом за последние три года в библиотеке было выявлено 57 проблем с корректностью работы, из которых 20 были помечены как уязвимости. Как же так? Ведь Rust должен был обернуть небезопасные части в загончик unsafe, чтобы как раз не было такого. Выходит, не помогло? А верифицировать любой код можно, не только Rust.
Ответить \| Правка \| Наверх \| Cообщить модератору


	3. "Инициатива по верификации стандартной библиотеки Rust"	+7 +/–
	Сообщение от Аноним (-), 24-Ноя-24, 11:57
	> Ведь Rust должен был обернуть небезопасные части в загончик unsafe, чтобы как раз не было такого. Так они это и сделали. Поэтому проблемы если возникают, то именно unsafe блоках. Не считая логических багов. От них только формальная верификация и спасет. > Выходит, не помогло? Наоборот, помогло. Посмотри сколько функций и в скольки есть unsafe. > А верифицировать любой код можно, не только Rust. Можно. Но в расте тебе нужно будет верифицировать 7.5к функция, а не 35 тысяч как в других языках. А это почти в 5 раз меньше работы.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	8. "Инициатива по верификации стандартной библиотеки Rust"	–2 +/–
	Сообщение от Аноним (8), 24-Ноя-24, 12:23
	>А это почти в 5 раз меньше работы. А вот это вряд ли, потому что каждое включение unsafe на Rust в 5 раз сложнее проверять, чем в других языках.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	9. "Инициатива по верификации стандартной библиотеки Rust"	+1 +/–
	Сообщение от Facemaker (?), 24-Ноя-24, 12:24
	>каждое включение unsafe на Rust в 5 раз сложнее проверять, чем в других языках Как вычислялась эта метрика?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	12. "Инициатива по верификации стандартной библиотеки Rust"	+5 +/–
	Сообщение от Аноним (-), 24-Ноя-24, 12:37
	> Как вычислялась эта метрика? Методика 'Пальцем в небо' сертифицированного сотрудника 'НИИ Кекспертизы и вбросов' им. Опеннета. Все утверждения истинны на 146%! Я бы спросил в чем отличие unsafe rust от обычной сишки, но смысла нет - все равно ответа не получим))
	Ответить \| Правка \| Наверх \| Cообщить модератору


	35. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (35), 24-Ноя-24, 14:23
	В чем отличие safe rust от обычной сишки?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	21. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от erthink_ (?), 24-Ноя-24, 13:15
	Нет. Ровно наоборот. Даже если иметь кривые руки, плохую голову и что-то натянуть против раста, то верификация unsafe в его собственных библиотеках потребует в разы меньше усилий чем верификация сишных библиотек со сравнимым функционалом. В среднем по больнице, unsafe-код в Rust более регулярен и проще (менее комплексный) чем подобный в сишных библиотеках. Есть и обратный эффект, в unsafe-функциях концентрация странностей/мутностей больше чем в средней glibc. Но это только потому, что в rust есть возможность и стремление отделять мух от котлет, а в glibc любые unsafe операции могут быть в любом месте (в самом безобидном и неожиданном). Конечно, можно найти зубодробительные unsafe-сценарии, но тогда и сравнивать их надо с аналогичными сишными случаями.
	Ответить \| Правка \| К родителю #8 \| Наверх \| Cообщить модератору


	13. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (13), 24-Ноя-24, 12:39
	> Но в расте тебе нужно будет верифицировать 7.5к функция, а не 35 тысяч как в других языках. в другом языке есть формально верифицированный компилятор https://compcert.org а у раста пока что даже не формализовали ситему типов https://blog.rust-lang.org/2023/01/20/types-announcement.html
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	28. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от erthink_ (?), 24-Ноя-24, 13:56
	> в другом языке есть формально верифицированный компилятор > https://compcert.org Нисколько не хочу принизить ценность проекта и достигнутые там результаты, но всё-таки нужно слегка критично читать написанное с осознанием всего комплекса проблем/задач. Формальная/математическая верификация покрывает часть функционала, т.е. "не всё". При этом возникает некая проблема/задача верификации "самого верификатора", т.е. доказательства что сформированного списка свойств достаточно для "верифицированного компилятора". Например, предположим что у вас есть "верифицированный компилятор". В нём могут быть баги ? - если "нет, багов быть не может", то упомянутый компилятор нельзя назвать верифицированным. - если "да, баги могут быть", то верификация перестаёт что-либо гарантировать на практике. Поэтому все подобные верификации всегда с массой уточнений и оговорок "тут рыбу заворачивали, сюда не смотрим" и "если остальное работает верно". Соответственно, отсутствие "формализированной системы типов" им не только не мешает, но и может помогать (сокращать поверхность).
	Ответить \| Правка \| Наверх \| Cообщить модератору


	16. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 12:52
	> Поэтому проблемы если возникают, то именно unsafe блоках. https://github.com/Speykious/cve-rs - в фантазиях. > А это почти в 5 раз меньше работы. Нет, это столько же работы, точнее даже больше. Сейф раст ничего не гарантирует.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	33. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (-), 24-Ноя-24, 14:21
	Вот эпичный тред, где люди в течение недели(!) пытались заставить это работать https://github.com/Speykious/cve-rs/issues/4 Им пришлось написать самописный null_mute, модифицировать transmute() подменив там crate::null_mut на самописный... и даже после этого получается ошибка компиляции error[E0133]: dereference of raw pointer is unsafe and requires unsafe function or block error: could not compile `cve-rs` (lib) due to previous error
	Ответить \| Правка \| Наверх \| Cообщить модератору


	36. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (35), 24-Ноя-24, 14:30
	Не знаю, что ты там компилируешь? $ cargo install cve-rs $ ~/.cargo/bin/cve-rs segfault Segmentation fault (core dumped)
	Ответить \| Правка \| Наверх \| Cообщить модератору


	6. "Инициатива по верификации стандартной библиотеки Rust"	–1 +/–
	Сообщение от Аноним (6), 24-Ноя-24, 12:03
	Нет ничего иделаьного! А результат всяко лучше по сравнению с С/C++.
	Ответить \| Правка \| К родителю #1 \| Наверх \| Cообщить модератору


	7. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от proninyaroslav (ok), 24-Ноя-24, 12:04
	А теперь представим что unsafe нет, и нужно перелопатить 35к функций, вместо 7500 если бы unsafe был.
	Ответить \| Правка \| К родителю #1 \| Наверх \| Cообщить модератору


	15. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 12:48
	Там и так нужно перелопатить 35к, уб в расте есть везде. Не говоря о том, что многие из этих 35к - хэлворды.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	18. "Инициатива по верификации стандартной библиотеки Rust"	+1 +/–
	Сообщение от proninyaroslav (ok), 24-Ноя-24, 12:59
	UB в расте не может быть за пределами unsafe блока. Это гарантированно. Все остальное он конечно не гарантирует, например утечки памяти.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	22. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 13:23
	Эти гарантии уже умножены на ноль. Кидал ссылку ниже.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	34. Скрыто модератором	+1 +/–
	Сообщение от Аноним (34), 24-Ноя-24, 14:21
	>Это гарантированно. Кем или чем?
	Ответить \| Правка \| К родителю #18 \| Наверх \| Cообщить модератору

5. "Инициатива по верификации стандартной библиотеки Rust"	+/–
Сообщение от ijuij (?), 24-Ноя-24, 12:02
Unsafe был введён более пяти лет назад (https://github.com/rust-lang/rust/commit/10855a36b53d33aa2e4...), и за это время люди успели использовать этот ключевое слово в множестве проектов. Однако только сейчас они начали заниматься его верификацией. Ну что ж, подход к безопасности действительно "на высшем уровне".
Ответить \| Правка \| Наверх \| Cообщить модератору


	31. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (34), 24-Ноя-24, 14:15
	Верифицируют библиотеку, а не unsafe.
	Ответить \| Правка \| Наверх \| Cообщить модератору

14. "Инициатива по верификации стандартной библиотеки Rust"	+1 +/–
Сообщение от 21yosenior (?), 24-Ноя-24, 12:46
https://github.com/Speykious/cve-rs - там уб в сейфе, толку валидировать ансейф.
Ответить \| Правка \| Наверх \| Cообщить модератору


	17. "Инициатива по верификации стандартной библиотеки Rust"	+1 +/–
	Сообщение от Карлос Сношайтилис (ok), 24-Ноя-24, 12:58
	Ага, со своей версий transmute. Из стандартной библиотеки "не подошла". https://github.com/Speykious/cve-rs/blob/main/src/transmute.rs
	Ответить \| Правка \| Наверх \| Cообщить модератору


	19. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 13:08
	Хоть со своей, хоть с чьей-то ещё. Заявляется безопасность кода на языке, а не либы - подучи логику. Ансейфа нет, проблемы есть.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	23. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (23), 24-Ноя-24, 13:35
	>> cve-rs also contains safe reimplementations of: >> std::mem::transmute >> std::ptr::null()/null_mut() but for references >>> pub const unsafe extern "rust-intrinsic" fn transmute<Src, Dst> >>> Reinterprets the bits of a value of one type as another type. > Хоть со своей, хоть с чьей-то ещё. Заявляется безопасность кода на языке, > а не либы - подучи логику. Ансейфа нет, проблемы есть. Кекспертизм опеннетный, аз из Да и то, что для появления проблем (т.е. чтобы найти баг в компиляторе - ведь "работатет" оно только с кастомным null/transmute) там целый консилиум корпел не одну неделю (см. обсуждение на гитхабе) - кексперты скромненько умалчивают. И правда, какая разница: заиметь UB после траха^W написания кастомного null и принудительного каста типа данных - или заиметь UB, просто сложив два числа или забыв пустую строку в конце исходника ...
	Ответить \| Правка \| Наверх \| Cообщить модератору


	26. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 13:44
	Всё, ответов не будет? С одного вопроса потеряться - мощно. > cve-rs also contains safe reimplementations of > safe reimplementations Молодец, умножил на ноль тезисы предыдущего героя. Хоть не зря кучу левого мусора спастил.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	32. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (23), 24-Ноя-24, 14:15
	> Всё, ответов не будет? С одного вопроса потеряться - мощно. Не суметь прочесть три предложения и сразу перейти к "папа, где море?" - намного уныл^W мощнее. >> cve-rs also contains safe reimplementations of >> safe reimplementations > Молодец, умножил на ноль тезисы предыдущего героя. Хоть не зря кучу левого мусора спастил. Молодец, обозвал сигнатуру transmute "левым мусором" и не сумел написать ничего по существу ... зато выдал хороший, объемный выхлоп метана - Газпром гордится тобой!
	Ответить \| Правка \| Наверх \| Cообщить модератору


	37. Скрыто модератором	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 14:36
	Ну так что, ты осилишь мне что-то возразить, клоун? Или спастить рандомный мусор и делать вид якобы что-то опроверг - твой потолок?
	Ответить \| Правка \| Наверх \| Cообщить модератору

20. "Инициатива по верификации стандартной библиотеки Rust"	+/–
Сообщение от Аноним (20), 24-Ноя-24, 13:14
> Компания Amazon и организация Rust Foundation представили инициативу Только один вопрос. Кто им разрешил?
Ответить \| Правка \| Наверх \| Cообщить модератору


	24. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от nume (ok), 24-Ноя-24, 13:41
	А кто запрещал?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	27. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от ijuij (?), 24-Ноя-24, 13:54
	Хороший вопрос! Иногда кажется, что разрешение не требуется.
	Ответить \| Правка \| К родителю #20 \| Наверх \| Cообщить модератору