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

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

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

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

Оглавление

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

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

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

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

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

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

Больше лишних проверок, которые в си пришлось бы писать руками на каждый чих , Аноним (50), 15:24 , 24-Ноя-24, (50)

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

Язык си необоснованно сложнее и найти там что-то ещё сложнее вывод очевиден Хот, Аноним (50), 15:26 , 24-Ноя-24, (51)

Язык Си сильно проще, а С отягощен поддержкой обратной совместимости с позвол, erthink_ (?), 16:30 , 24-Ноя-24, (88) –1

Может уже пора перестать переписывать и написать что-то новое на самом расте , Аноним (50), 16:51 , 24-Ноя-24, (95)

Лол Кто ты вообще такой чтобы что-то, кому-то указывать Особенно разрабам кото, Аноним (116), 17:59 , 24-Ноя-24, (116)

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

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

там написано вполне ясно без формального описания не может быть никакой верифика, Аноним (13), 14:54 , 24-Ноя-24, (42)

это называется спецификация, в этой же спеке определяется понятие баг , Аноним (44), 15:11 , 24-Ноя-24, (44)

есть один компилятор и никто точно не знает как он работает, только догадываются, Аноним (13), 15:22 , 24-Ноя-24, (48)

На то и спека, где это все описано, и есть механизм верификации и валидации, кот, Аноним (44), 16:10 , 24-Ноя-24, (79)

есть код на языке программирования и есть код исполняемый процессором, вы разниц, Аноним (13), 16:23 , 24-Ноя-24, (82)

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

Ну и как продолжать дискуссию, если нет понимания для чего вообще нужно это все,, Аноним (44), 16:18 , 24-Ноя-24, (81)

Ту там же символьные вычисления и местами абстрактная алгебра Например, можно ве, erthink_ (?), 15:31 , 24-Ноя-24, (54)

в расте есть MIRI, Аноним (93), 16:42 , 24-Ноя-24, (93)

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

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

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

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

Но только в фантазиях опеннетных кекспертов-военов супротив раста, не ходящих по, Аноним (45), 15:12 , 24-Ноя-24, (45) +2

opened on May 28, 2015У меня всё прекрасно, а у вас что с лицом уже почти 10 лет, Аноним (35), 15:18 , 24-Ноя-24, (46)

Их лицо перекашивает из-за того то их Раст шпыняет кто угодно и легко доказывает, Аноним (50), 15:30 , 24-Ноя-24, (52)
Какое ловкое переобувание в прыжке, однако , Аноним (45), 15:33 , 24-Ноя-24, (56)

А ты забавный Тебе показывают, что язык дырявый Ты даешь ссылку, что дыра суще, Аноним (35), 15:44 , 24-Ноя-24, (69)

Не язык, а компилятор Да, нашли в нём недоработку И , Прохожий (??), 15:53 , 24-Ноя-24, (74)

На данном этапе развития rust язык и референсный компилятор неотделимы И повтор, Аноним (35), 16:06 , 24-Ноя-24, (78)

А ты еще забавней, проигнорировал ответ автора cvs-rs, проигнорировал сложность , Аноним (45), 16:14 , 24-Ноя-24, (80)

Ничего я не игнорировал Вам дали ссылку на конкретый баг с полным описанием, ка, Аноним (35), 16:35 , 24-Ноя-24, (91)

Какая занимательная реальность, в моей - это описание дал я сам, а воены супроти, Аноним (45), 17:24 , 24-Ноя-24, (104)

Только для целевой атаки достаточно одной уязвимости Подумай об этом И про лож, Аноним (50), 15:22 , 24-Ноя-24, (49) –1

О, Воены Супротив Раста подтянули тяжелую артиллерию в виде натягиваемых на гл, Аноним (45), 15:37 , 24-Ноя-24, (60) +1

Нет никаких военов Есть только люди со здравым смыслом и это не ты Кому безопа, Аноним (50), 16:27 , 24-Ноя-24, (86)

Отличается производительностью выполняемого кода в той же когорте, что и C C Р, laindono (ok), 18:38 , 24-Ноя-24, (124)

А Rustonomicon говорит строго обратное, что unsafe - нелокален, и что от него пр, Аноним (77), 16:03 , 24-Ноя-24, (77)

Нет ничего иделаьного А результат всяко лучше по сравнению с С C , Аноним (6), 12:03 , 24-Ноя-24, (6)

Если на стройке носить 10 касок подряд, то будет в 10 раз безопаснее Но почему-, Аноним (90), 16:35 , 24-Ноя-24, (90)

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

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

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

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

Семантика языка, которая гарантирует безопасность, это всего лишь описание Но к, proninyaroslav (ok), 15:20 , 24-Ноя-24, (47) –1

Он демонстрирует что в расте нет никакой необходимости Дешевле писать на нормал, Аноним (50), 15:33 , 24-Ноя-24, (57) +1

Питон на реальных задачах в сотни раз медленее Си Лучше уж Java или C , Аноним (90), 16:36 , 24-Ноя-24, (92)

Куда ты так торопишься задача ты моя Так можно и успеть , Аноним (50), 16:49 , 24-Ноя-24, (94)

Скрыто модератором, Аноним (-), 18:08 , 24-Ноя-24, (120)

Скрыто модератором, Аноним (34), 14:21 , 24-Ноя-24, (34) +1

Почему нельзя сразу написать безопасно Если есть ансейф то язык уже небезопасен, Аноним (50), 15:32 , 24-Ноя-24, (55)

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

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

Но ведь адепты говорили что факт написания ансейфа будет помогать программисту с, Аноним (50), 15:36 , 24-Ноя-24, (58)

А гугол-то в курсе https www opennet ru opennews art shtml num 61933 ---Опят, Аноним (45), 15:43 , 24-Ноя-24, (68) +1

Опять повысились надои А новость сабжевую ты прочитать не хочешь Чтобы найти в, Аноним (50), 16:25 , 24-Ноя-24, (84)

Опять альтернативная реальность А то в нашей гугол платит нехилые бабки за кажд, Аноним (45), 17:32 , 24-Ноя-24, (106)

Что та скоростью разработки в 10 раз медленнее Серво уже дописали Или может ре, Аноним (50), 17:40 , 24-Ноя-24, (108)

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

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

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

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

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

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

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

Следует отличать хак, найденный в компиляторе, от намеренного UB в стандарте si, Прохожий (??), 15:31 , 24-Ноя-24, (53)

У раста нет стандарта Ты с логикой поссорился ещё очень много лет назад , Аноним (50), 15:37 , 24-Ноя-24, (61)

Я про стандарты в таких языках, как Си, Си , Прохожий (??), 15:39 , 24-Ноя-24, (63)

ниже - ранее, Прохожий (??), 15:38 , 24-Ноя-24, (62)

21yoseniorУ Rust нет спецификации, но есть RFC Принципиальной разницы на вижу, , Прохожий (??), 15:52 , 24-Ноя-24, (73)

Скрыто модератором, 21yosenior (?), 16:26 , 24-Ноя-24, (85)

Скрыто модератором, 21yosenior (?), 15:44 , 24-Ноя-24, (70)

Скрыто модератором, Аноним (-), 17:12 , 24-Ноя-24, (101)

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

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

Вопрос не праздный Вспомним Ada, созданный МО Да, он есть, но связываться с ни, Аноним (20), 14:40 , 24-Ноя-24, (39)

Но не оно является создателем языка, и не оно создаёт компилятор Например, каки, Прохожий (??), 15:47 , 24-Ноя-24, (71) –1

Экспортные ограничения , Аноним (20), 16:32 , 24-Ноя-24, (89)

МО не занимается вопросами экспорта , Аноним (98), 17:03 , 24-Ноя-24, (98)

Скрыто модератором, Аноним (50), 18:07 , 24-Ноя-24, (119)

Инициатива наказуема , Аноним (29), 13:59 , 24-Ноя-24, (29) +1

Ты так говоришь как будто это что то плохое , Аноним (50), 15:41 , 24-Ноя-24, (66)

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

В суверенных проектах его использовать нельзя , Аноним (34), 14:48 , 24-Ноя-24, (41) +1
Пишите свой хлам, размещайте на госуслугах Cargo поддерживает такое , Страдивариус (?), 15:06 , 24-Ноя-24, (43)

пишите-немышите, Аноним (8), 15:40 , 24-Ноя-24, (65) –1
Это ты сейчас смеёшься, а когда всех пересдачи принудителтно на OneScript я на т, Аноним (50), 16:29 , 24-Ноя-24, (87)

Не могу я понять растохейтеров Впервые появился инструмент, позволяющий безопас, Аноним (59), 15:37 , 24-Ноя-24, (59) +1

Скрыто модератором, Аноним (50), 15:40 , 24-Ноя-24, (64)

Скрыто модератором, Аноним (-), 17:03 , 24-Ноя-24, (97)

Без какой потери производительности Тесты посмотри Магии не бывает , Аноним (8), 15:41 , 24-Ноя-24, (67)

Ну, посмотрел https benchmarksgame-team pages debian net benchmarksgame fastes, Аноним (45), 15:51 , 24-Ноя-24, (72)

О да тесты на домене 4го уровня А самому головой подумать Или как ты делаешь д, Аноним (50), 16:23 , 24-Ноя-24, (83)

Э на этапе компиляции Если у тебя типы провепяются во время компиляции, если э, Аноним (-), 16:56 , 24-Ноя-24, (96)

Скрыто модератором, Аноним (50), 17:48 , 24-Ноя-24, (110)

Других аргументов, полагаю, нет и не будет , Аноним (98), 17:06 , 24-Ноя-24, (99) –2

Читай до полного усвоения https habr com ru articles 598219 , Аноним (50), 17:50 , 24-Ноя-24, (112)

Ты бы сам прочитал, а то вышел неловкий пук в лужу с твоим rustmustdie https w, Аноним (45), 18:06 , 24-Ноя-24, (118)
Кстати, вдогонку насчет рантайма и дабы немного подогреть бедных военов а то зи, Аноним (45), 18:20 , 24-Ноя-24, (123)

О, опоздавший родиться и не слышавший о The Computer Language Benchmarks Game ,, Аноним (45), 17:13 , 24-Ноя-24, (102)

Неофит - новый сторонник какой-либо религии Новыми можно назвать адептов Rust Та, Аноним (34), 17:44 , 24-Ноя-24, (109)

Он ещё даже вуз не окончил, а уже пытается умные слова употреблять , Аноним (50), 17:54 , 24-Ноя-24, (114)

Подгонять что угодно под тесты любимая задача для очковтирателей , Аноним (50), 17:50 , 24-Ноя-24, (111)

А Воены Супротив Раста - это члены древнего и уважаемого Ордена Защиты Вселенной, Аноним (45), 17:57 , 24-Ноя-24, (115) +1

Тебе говорят что тесты сами по себе ничего не значат, а ты говоришь чтобы тебе д, Аноним (50), 18:04 , 24-Ноя-24, (117)

Воены, вы там уже определитесь, что ли Короче, окромя унылого балабольства, Аноним (45), 18:11 , 24-Ноя-24, (121)

Раст стал ещё более безопасен Разве другой язык на это способен , Аноним (100), 17:07 , 24-Ноя-24, (100)

Скрыто модератором, Аноним (13), 17:26 , 24-Ноя-24, (105)

Скрыто модератором, Аноним (103), 17:15 , 24-Ноя-24, (103)
Кто тут говорил, что Раст безопасен , Аноним (-), 17:40 , 24-Ноя-24, (107)

Раст небезопасен там есть unsafe, Аноним (50), 17:53 , 24-Ноя-24, (113)

Гендерно-нейтральные сортиры затрещали по швам Дepьмokpaтия ox eвaeт , Аноним (122), 18:14 , 24-Ноя-24, (122)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Больше лишних проверок, которые в си пришлось бы писать руками на каждый чих.

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

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

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

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

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

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

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

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

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

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

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

> Язык си необоснованно сложнее и найти там что-то ещё сложнее вывод очевиден.
Язык Си сильно проще, а С++ отягощен поддержкой обратной совместимости (с позволением всего unsafe что можно в Cи).
> Хотя вывод понятен по отсутствию софта написанного на раст. Особенно в
> областях где хваленая работа с памятью могла бы иметь место.
Так ведь именно активно используется, даже не взирая не упомянутые выше баги.
И переписывается на Rust достаточном много, там где либо высоки риски и в совокупности есть целесообразность для бизнеса, либо где что-то кому-то интересно.
Другое дело, что в условном debian этого не видно, ибо 90% пакетов появились до раста и вся экосистема "сишная".

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

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

Сообщение от Аноним (50), 24-Ноя-24, 16:51

Может уже пора перестать переписывать и написать что-то новое на самом расте?

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

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

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

Лол. Кто ты вообще такой чтобы что-то, кому-то указывать? Особенно разрабам которые свои проекты на Rust перекатывают.Да и нового софта на Rust уже вагон, и игровые движки и редакторы кода, и целая DE с прикладнухой. С разморозкой!

Ответить | Правка | Наверх | 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ообщить модератору

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

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

> Поэтому все подобные верификации всегда с массой уточнений и оговорок
там написано вполне ясно
> Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program.
> Соответственно, отсутствие "формализированной системы типов" им не только не мешает, но и может помогать (сокращать поверхность).
без формального описания не может быть никакой верификации, как это может "помогать" ?

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

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

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

> без формального описания не может быть никакой верификации
это называется спецификация, в этой же спеке определяется понятие "баг".

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

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

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

> это называется спецификация, в этой же спеке определяется понятие "баг"
есть один компилятор и никто точно не знает как он работает, только догадываются. Сомневаюсь что кто-то в своём уме пишет на этом доверенный код.

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

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

Сообщение от Аноним (44), 24-Ноя-24, 16:10

> есть один компилятор и никто точно не знает как он работает, только догадываются.
На то и спека, где это все описано, и есть механизм верификации и валидации, который позволяет проверить с тем, что написано в спеке.
> Сомневаюсь что кто-то в своём уме пишет на этом доверенный код.
У кода, формально верифицируют его корректность. Вы понимаете, что такое корректность?

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

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

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

> У кода, формально верифицируют его корректность. Вы понимаете, что такое корректность?
есть код на языке программирования и есть код исполняемый процессором, вы разницу вообще понимаете ?

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

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

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

>> без формального описания не может быть никакой верификации
> это называется спецификация, в этой же спеке определяется понятие "баг".
Не важно как называется, но суть в определении рамок/границ что верифицируется, а что оставляется за скобками.
И тут всё правильно, ибо по-другому не возможно.
Но нужно понимать что именно верифицировано и в "каких терминах", так как в конечном счете нет большой разницы чем будет вызвана проблема -- багом компилятора, не-верифицированностью каких-то его частей, либо изъяном в правилах/целях/критериях/ограничениях верификации.
Поэтому читая "верифицированный компилятор" всегда хочется понять что имели в виду:
- конкретный exe-шник.
- набор исходников или какое-то их подмножество.
- представление кода и его преобразования описанные в некой формальной системе, для которых доказана их корректность.
- формальная система для описания представления кода и его преобразований, которая позволяет выполнить доказательства корректности.

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

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

Сообщение от Аноним (44), 24-Ноя-24, 16:18

> Не важно как называется, но суть в определении рамок/границ что верифицируется, а что оставляется за скобками.
Ну и как продолжать дискуссию, если нет понимания для чего вообще нужно это все, если изначально не важно как это все называть.
> Поэтому читая "верифицированный компилятор" всегда хочется понять что имели в виду:
Читая где? вот откройте страницу этого компилятора и прочитайте, что там специфицировали, что верифицировали и валидировали, и как это все вам повторить в домашних условиях. Хотя сначала нужно открыть и прочесть теорию данной области (формальной верификации). И все вопросы вида "что имели в виду" сразу отпадут.
> багом компилятора
Ну дайте мне строгое определение этого термина. Правильно ведь, без толку его мне щас давать?

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

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

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

> без формального описания не может быть никакой верификации, как это может "помогать"
> ?
Ту там же символьные вычисления и местами абстрактная алгебра.
Например, можно верифицировать что "компилятор" не нарушает систему типов, без полной формализации и/или верификации самой системы типов.
Конечно, такой "компилятор" может быть не в состоянии генерировать исполнимый код.
Либо всё-таки уметь это, но уже с подмешиванием не-верифицированного функционала и/или не-верифицированной системы типов.
А еще может выясниться, что конкретная система типов может не-покрываться/требовать-большего, чем умеет верифицированная часть компилятора, и/или требовать снятия части ограничений/формулировок введенных для возможности верификации, и т.п.
--
Собственно, хотел обратить внимание, что есть "рамки верификации" и почти всегда практическое применение никак в них не помещается.

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

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

Сообщение от Аноним (93), 24-Ноя-24, 16:42

в расте есть MIRI

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

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

Сообщение от 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ообщить модератору

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

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

Он ничего не компилирует, он агитатор который потерялся в ветке ниже.
Если непонятно, почему они так цепляются за "кастомный" трансмут. Это опшн-селект такой. Если трансмут стандартный - орём "там ансейф, поэтому не считается". Если трансмут свой - орём "надо было брать стандартный, поэтому не считается". Система непотопляема, как говорится.

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

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

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

> Нет, это столько же работы, точнее даже больше. Сейф раст ничего не
> гарантирует.
Но только в фантазиях опеннетных кекспертов-военов супротив раста, не ходящих по своим же ссылкам.
https://docs.rs/cve-rs/latest/cve_rs/lifetime_expansion/inde...
> How it works
> There is a soundness hole in the Rust compiler that allows our domain expansion to work.
...
> rustc should infer that one of the lifetimes does not outlive 'static, so that we can’t
> use lifetime_translator; however, for whatever reason, it doesn’t, so this exploit works.
> See https://github.com/rust-lang/rust/issues/25860 for this bug’s bug report.
Воены-кексперты, что с лицом?

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

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

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

>> https://github.com/rust-lang/rust/issues/25860
opened on May 28, 2015
>Воены-кексперты, что с лицом?
У меня всё прекрасно, а у вас что с лицом уже почти 10 лет?

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

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

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

Их лицо перекашивает из-за того то их Раст шпыняет кто угодно и легко доказывает бесполезность раста.

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

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

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

> Сейф раст ничего не гарантирует.
...
> opened on May 28, 2015
>>Воены-кексперты, что с лицом?
> У меня всё прекрасно, а у вас что с лицом уже почти
Какое ловкое переобувание в прыжке, однако ...

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

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

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

А ты забавный. Тебе показывают, что язык дырявый. Ты даешь ссылку, что дыра существует 10 лет. Причем в обсуждении дыры прямо пишут, что у раста проблемы тайпчекером и системой типов. 10 лет.

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:53

Не язык, а компилятор. Да, нашли в нём недоработку. И?

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

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

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

> Не язык, а компилятор.
На данном этапе развития rust язык и референсный компилятор неотделимы. И повторюсь, пишут что есть проблемы с системой типов - это именно про язык. Исправят только в "следующем поколоении".

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

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

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

>> we already had a crate published on crates.io before which used this bug to transmute in safe code, see #25860 (comment).
>> this issue is a priority to fix for the types team and has been so for years now. there is a reason for why it is not yet fixed. fixing it relies on where-bounds on binders which are blocked on the next-generation trait solver. we are actively working on this and cannot fix the unsoundness before it's done.
> А ты забавный. Тебе показывают, что язык дырявый. Ты даешь ссылку, что
> дыра существует 10 лет. Причем в обсуждении дыры прямо пишут, что
> у раста проблемы тайпчекером и системой типов. 10 лет.
А ты еще забавней, проигнорировал ответ автора cvs-rs, проигнорировал сложность абуза этого бага (там "кастуют" и "магичат" с кусом памяти нулевого размера) в реальном коде,
зато обобщил этот баг в компилере как "язык дырявый". Ну да, то ли дело баги в GCC, всплывающие прям в регресс-тестах ядра,
https://lkml.iu.edu/hypermail/linux/kernel/1407.3/00650.html
ага.
Хотя открою тайну: полностью "sound" ЯПы либо остаются маргинальными академическими поделками, на которых никто не пишет, либо строчка кода, для тех же критических систем, обходится в очень нехилую сумму денег, плюс минимум еще столько же за верификацию "взаимодействия" этого кода с реальностю.

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

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

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

> проигнорировал ответ автора cvs-rs, проигнорировал сложность абуза этого бага
Ничего я не игнорировал. Вам дали ссылку на конкретый баг с полным описанием, как этот баг экплуатируется.
"Сложность" и "невозможность" находятся по разную сторону. Евангелистам не надо было распинаться про "невозможность", не тыкали бы этим проектом в лицо.
> Хотя открою тайну: полностью "sound" ЯПы
Я хорошо знаю сложность (NP) верификации алгоритмов, в том числе про сложность работы с памятью (NP). Поэтому резко против евангелистов rust с "безопасной работой с памятью". На данном этапе разития математики, науки и техники (формальную) корректность можно проверить только у небольшой программы.
Жду "следующего поколения"

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

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

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

>> проигнорировал ответ автора cvs-rs, проигнорировал сложность абуза этого бага
> Ничего я не игнорировал. Вам дали ссылку на конкретый баг с полным
> описанием, как этот баг экплуатируется.
Какая занимательная реальность, в моей - это описание дал я сам, а воены супротив раста выдали лишь невнятное "ничего не гарантирует, вот!" ...
> Я хорошо знаю сложность (NP) верификации алгоритмов, в том числе про сложность
> работы с памятью (NP). Поэтому резко против евангелистов rust с "безопасной
> работой с памятью". На данном этапе разития математики, науки и техники
> (формальную) корректность можно проверить только у небольшой программы.
Сложность NP решается ограничением на лишь определенное подмножество операций (ну вон, см. трудности реализации двусвязного списка в расте) и "ручной проверкой" всего остального. Это позволяет задействовать мощности компьюктеров для проверки хотя бы части кода, вместо заката солнца ручками.
Внезапно, да?
А то на идрисах, агдах и коках чей-то не видно программ общего-системного назначения ...

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

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

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

Только для целевой атаки достаточно одной уязвимости. Подумай об этом. И про ложку дегтя в бочке меда. Не имеет смысла размер бочки если любое количество дегтя делает даже самую безопасТную бочку неюзабельной. Можно просто сэкономить на бочке.

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

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

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

> И про ложку дегтя в бочке меда. Не имеет смысла размер бочки если
> любое количество дегтя делает даже самую безопасТную бочку неюзабельной. Можно просто
> сэкономить на бочке.
О, Воены Супротив Раста подтянули "тяжелую артиллерию" в виде натягиваемых на глобус аналогий.
Надеюсь, Воены пилят только ручной пилой (и используют такую же продукцию), а то ведь электро/бензопилу и всякие индустриальные лесопилки легко отыметь простым ломом, что делает их с точки зрения-"логики" Военов неюзабильными ...

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

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

Сообщение от Аноним (50), 24-Ноя-24, 16:27

Нет никаких военов. Есть только люди со здравым смыслом и это не ты. Кому безопасно есть питон, го, хаскель, джаваскрипт. Руст от них ничем в лучшую сторону не отличается.

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

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

Сообщение от laindono (ok), 24-Ноя-24, 18:38

Отличается производительностью выполняемого кода в той же когорте, что и C/C++.
Раньше выбор стоял между крестиками и питоном (условно) и выбор состоял в безопасности против производительности.
Теперь выбор между растом и условным питоном. При этом выбор между скоростью написания кода и производительностью.
Со временем плюсы станут коболом. Куча легаси кода, который никто особо не хочет трогать кроме старичья.

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

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

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

>Поэтому проблемы если возникают, то именно unsafe блоках.
А Rustonomicon говорит строго обратное, что unsafe - нелокален, и что от него проблемы могут возникнуть вообще где угодно.

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

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

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

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

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

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

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

Если на стройке носить 10 касок подряд, то будет в 10 раз безопаснее! Но почему-то в реальности так никто не делает.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Он демонстрирует что в расте нет никакой необходимости. Дешевле писать на нормальных языках. Сейф на питоне, ансейф быстрый код на с++ как модули для питона. Все экономия 1000%

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

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

Сообщение от Аноним (90), 24-Ноя-24, 16:36

Питон на реальных задачах в сотни раз медленее Си. Лучше уж Java или C#.

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

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

Сообщение от Аноним (50), 24-Ноя-24, 16:49

Куда ты так торопишься задача ты моя? Так можно и успеть.


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

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

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

> Он демонстрирует что в расте нет никакой необходимости
Наверное, поэтому правительство штатов приказало предоставить план отказа от C/C++ к 2026 году.

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

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

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

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

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

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

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

Почему нельзя сразу написать безопасно. Если есть ансейф то язык уже небезопасен.

Ответить | Правка | К родителю #7 | Наверх | 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ообщить модератору

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

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

Но ведь адепты говорили что факт написания ансейфа будет помогать программисту сильнее концентрироваться на ошибках в коде, а оказывается не помогает. И хакер все равно выйдет за границы и возьмёт рута. А уязвимость поправят только через 5 лет во время какой-то там верификации. Причем найдут только 1 из 10 уязвимостей.

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

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

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

> Но ведь адепты говорили что факт написания ансейфа будет помогать программисту сильнее
> концентрироваться на ошибках в коде, а оказывается не помогает. И хакер
> все равно выйдет за границы и возьмёт рута.
А гугол-то в курсе?
https://www.opennet.ru/opennews/art.shtml?num=61933
>  Методы безопасной работы с памятью позволили существенно снизить число уязвимостей в Android
...
> Изменения позволили снизить долю связанных с памятью уязвимостей в Android c 76% в 2019 году до 24% в 2024 году
---
> А уязвимость поправят только через 5 лет во время какой-то там верификации. Причем найдут только 1 из 10 уязвимостей.
Опять методика 'Пальцем в небо' сертифицированного сотрудника 'НИИ Кекспертизы и вбросов' им. Опеннета?

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

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

Сообщение от Аноним (50), 24-Ноя-24, 16:25

Опять повысились надои? А новость сабжевую ты прочитать не хочешь? Чтобы найти вульны нужна аш целая инициатива от целого Амазона. Без этого вульны не ищутся.

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

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

Сообщение от Аноним (45), 24-Ноя-24, 17:32

> Опять повысились надои? А новость сабжевую ты прочитать не хочешь? Чтобы найти
> вульны нужна аш целая инициатива от целого Амазона. Без этого вульны
> не ищутся.
Опять альтернативная реальность? А то в нашей гугол платит нехилые бабки за каждый найденый вулн:
https://opennet.ru/opennews/art.shtml?num=60780
> Из потраченной в 2023 году суммы $3.4 млн (в прошлом году $4.8 млн) выплачено за уязвимости в Android. За информацию об уязвимостях в браузере Chrome было выплачено 359 премий на общую сумму $2.1 млн (в прошлом году $3.5 млн).
Че там кстати с твоими чиселками? Я угадал с методикой очередного статистического опеннетного исследования?

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

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

Сообщение от Аноним (50), 24-Ноя-24, 17:40

Что та скоростью разработки в 10 раз медленнее? Серво уже дописали? Или может редокс?

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

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

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

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

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

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

Сообщение от Карлос Сношайтилис (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" +/–

Сообщение от Аноним (45), 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" +/–

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

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

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

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

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

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

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:31

Следует отличать хак, найденный в компиляторе, от намеренного UB в стандарте (sic!) языка программирования. Вы там чуть ниже про логику говорили...

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

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

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

У раста нет стандарта. Ты с логикой поссорился ещё очень много лет назад.

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:39

Я про стандарты в таких языках, как Си, Си++

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:38

ниже ->  ранее

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:52

21yosenior
У Rust нет спецификации, но есть RFC. Принципиальной разницы на вижу, как и, например, группа разработчиков Gcc,которые работают над своей версией компилятора.
Говоря о стандартах, я имел ввиду не Rust, а C, C++.
Про какое "воровство" вы тут говорите?

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

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

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

> Про какое "воровство" вы тут говорите?
Я написал про какое. Приведены противоречия лозунгов("гарантирует" и прочее) с реальностью(никаких гарантий). Что ты мне отвечаешь? - "а вот в сишке уб". Никто не спрашивал тебя про сишку, тебя спрашивали про враньё. Но ты начал прятаться за сишку, пытаясь съехать с темы.
RFC мусор, который ничего не описывает. Можешь показать мне описание модели памяти в расте. Это принципиальная разница.

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

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

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

Покажешь мне стандарт раста. Иди погугли, вернёшься как найдёшь.
К тому же, в очередной раз заходы уровня "а у вас негров линчуют". Кто-то говорил здесь про сишку и прочие языки? - нет. Но данный пропагандист почему-то начал прятаться за ними.
Это кстати, фундаментальное свойство. Раст состоит из воровства не только по части семантики/компилятора/рантайма/прочего, но также из воровства обоснований своей состоятельности. То есть без пряток за сишку даже сказать никто не смог, что из себя представляет раст и зачем он нужен.

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

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

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

> Это кстати, фундаментальное свойство. Раст состоит из воровства не только по части семантики/компилятора/рантайма/прочего,
ого, ну у тебя бомбануло!
а какой компилятор украли?
его сначала на окалме писали, потом на самом расте..
даже бекенд на самом расте уже есть
> но также из воровства обоснований своей состоятельности.
Ты часом не бухаешь? а то логика как-то хромает.
> То есть без пряток за сишку даже сказать никто не смог, что из себя представляет раст и зачем он нужен.
Для того чтобы сравнить что-то, нужно минимум два операнда.
Раст избавляет от типичных ошибок памяти... в чем?
в си/с++, а аде и фортране такого же нет.

Ответить | Правка | Наверх | 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ообщить модератору

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

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

Вопрос не праздный. Вспомним Ada, созданный МО. Да, он есть, но связываться с ним как-то не хотелось и не хочется. За Rust также топит МО. И это тоже как бы намекает. Последствия будут, если не сейчас, так потом. Смотреть надо не сиюминутные выгоды, а на перспективу.
Наверное, лучше остаться на относительно свободном C/C++, в том числе для новых проектов.

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

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

Сообщение от Прохожий (??), 24-Ноя-24, 15:47

>За Rust также топит МО.
Но не оно является создателем языка, и не оно создаёт компилятор.
>И это тоже как бы намекает. Последствия будут, если не сейчас, так потом.
Например, какие?
>Наверное, лучше остаться на относительно свободном C/C++, в том числе для новых проектов.
Группа разработчиков Gcc работает над компилятором Rust, если вы о вендорлоке.

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

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

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

> Например, какие?
Экспортные ограничения.

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

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

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

МО не занимается вопросами экспорта.

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

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

Сообщение от Аноним (50), 24-Ноя-24, 18:07

А ещё она медицинскую помощь нелегальным мигрантам не оказывает. Давай больше бессвязных фактов.

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

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

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

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

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

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

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

Ты так говоришь как будто это что то плохое.

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

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

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

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

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

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

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

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

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

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

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

В суверенных проектах его использовать нельзя.

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

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

Сообщение от Страдивариус (?), 24-Ноя-24, 15:06

Пишите свой хлам, размещайте на госуслугах. Cargo поддерживает такое.

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

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

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

пишите-немышите

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

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

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

Это ты сейчас смеёшься, а когда всех пересдачи принудителтно на OneScript я на тебя посмотрю.

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

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

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

Не могу я понять растохейтеров. Впервые появился инструмент, позволяющий безопасно работать с памятью без ГЦ, без потери производительности, а они только критикуют. Самое смешное, что они критикуют Раст за то, что он не спасает от всех ошибок. "Что ж за безопасность, от всего не защищает, поэтому лучше останусь на Си". Логика классная, да, чем получить хоть какую-то защиту, буду шпарить дальше на абсолютно незащищённым Си.

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

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

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

Таких языков поделок куча. Даже в институтах учат писать компиляторы. И все они не спасают ни от чего. Не понимаю растофанатиков они транслируют только лозунги, но не могут посмотреть в реальный пподукт, не то что в свой холодильник.

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

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

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

> Таких языков поделок куча. Даже в институтах учат писать компиляторы. И все они не спасают ни от чего.
Сразу видно что в университетах ты не учился.
Сколько классов церковно приходской школы осилил?
> не могут посмотреть в реальный пподукт, не то что в свой холодильник.
у тебя телефон с какой системой?
Если это не петухофон, или кнопочная звонилка, но в нем раст уже может работать (если это не андроид 8)))

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

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

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

Без какой потери производительности? Тесты посмотри. Магии не бывает.

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

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

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

> Без какой потери производительности? Тесты посмотри. Магии не бывает.
Ну, посмотрел https://benchmarksgame-team.pages.debian.net/benchmarksgame/...
что дальше? "Неправильные тесты, нещитаица!"?

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

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

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

О да тесты на домене 4го уровня. А самому головой подумать? Или как ты делаешь дополнительную работу не задействуя дополнительных команд процессора?

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

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

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

Э.. на этапе компиляции?
Если у тебя типы провепяются во время компиляции, если элемент Enum у тебя можно отличить от другого перечисления (и это не задекорированный int как в других языках), если у тебя есть проверки инвариантов, если проверки на null...
Да скорость сборки у тебя замедлится, но выполнение может быть на том же уровне.

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

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

Сообщение от Аноним (50), 24-Ноя-24, 17:48

А Раст рантайм? Я конечно понимаю что мозг твой туго промыт но даже у знающих растофанатиков не получилось отделить Раст на столько чтобы поравняться с Си https://habr.com/ru/articles/598219/

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

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

Сообщение от Аноним (98), 24-Ноя-24, 17:06

> тесты на домене 4го уровня
Других аргументов, полагаю, нет и не будет.

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

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

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

Читай до полного усвоения https://habr.com/ru/articles/598219/

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

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

Сообщение от Аноним (45), 24-Ноя-24, 18:06

> Читай до полного усвоения https://habr.com/ru/articles/598219/
Ты бы сам прочитал, а то вышел неловкий пук в лужу с твоим rustmustdie:
https://www.opennet.ru/openforum/vsluhforumID3/126424.html#247
https://www.opennet.ru/openforum/vsluhforumID3/126424.html#270
Ну, брать дебаг-релиз и сравнивать с gcc-шным выхлопом -O0, как бы уже намекает на уровень (ламерства) ...

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

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

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

> Читай до полного усвоения https://habr.com/ru/articles/598219/
Кстати, вдогонку насчет рантайма и дабы немного подогреть бедных военов (а то зима,  лужи ведь холодные):
https://www.opennet.ru/openforum/vsluhforumID3/124921.html#322
++++++
> Сколько весит хелло ворд на русте с зависимостями?
500 байт

$ cat hello.rs
#![no_std]
#![no_main]
use core::panic::PanicInfo;
use syscall::syscall;
#[panic_handler]
fn panic(_info: &PanicInfo) -> ! { loop {} }
#[no_mangle]
pub extern fn _start() -> ! {
    let message = "Hello World\n".as_bytes();
    unsafe {
        syscall!(WRITE, 0, message.as_ptr(), message.len());
        syscall!(EXIT,0);
    }
    loop {}
}

$ ./hello
Hello World
$ ll hello
-rwxr-x---   496B 30 Jul. 12:41 hello*
$  readelf -d hello
There is no dynamic section in this file.
$ objdump -d  hello

Disassembly of section .text:
00000000004000b0 <.text>:
  4000b0:    55                       push   %rbp
  4000b1:    48 89 e5                 mov    %rsp,%rbp
  4000b4:    6a 04                    pushq  $0x4
  4000b6:    58                       pop    %rax
  4000b7:    6a 09                    pushq  $0x9
  4000b9:    5a                       pop    %rdx
  4000ba:    be cc 00 40 00           mov    $0x4000cc,%esi
  4000bf:    31 ff                    xor    %edi,%edi
  4000c1:    0f 05                    syscall
  4000c3:    6a 01                    pushq  $0x1
  4000c5:    58                       pop    %rax
  4000c6:    31 ff                    xor    %edi,%edi
  4000c8:    0f 05                    syscall
  4000ca:    eb fe                    jmp    0x4000ca
Приходи, когда найдешь тут рантайм.

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

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

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

> О да тесты на домене 4го уровня.
О, опоздавший родиться и не слышавший о "The Computer Language Benchmarks Game", зато топящий за сишку? Ну, бывает, особенно у неофитов.
> А самому головой подумать? Или как ты делаешь дополнительную работу не задействуя дополнительных команд процессора?
Короче, тестов сравнимых по качеству хотя бы с бенчмарк-геймом не будет, будет лишь вода и "нещитаица".

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

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

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

>зато топящий за сишку? Ну, бывает, особенно у неофитов.
Неофит - новый сторонник какой-либо религии.
Новыми можно назвать адептов Rust.
Так что, как то, неправильное употребление слова.

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

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

Сообщение от Аноним (50), 24-Ноя-24, 17:54

Он ещё даже вуз не окончил, а уже пытается умные слова употреблять.

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

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

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

Подгонять что угодно под тесты любимая задача для очковтирателей.

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

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

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

> Неофит - новый сторонник какой-либо религии.
> Новыми можно назвать адептов Rust.
А Воены Супротив Раста - это члены древнего и уважаемого Ордена Защиты Вселенной от Ржавой Угрозы, ага.
> Без какой потери производительности? Тесты посмотри. Магии не бывает.
> Подгонять что угодно под тесты любимая задача для очковтирателей.
А ты самокритичен! Правда, тесты так и не предоставил.
Ну и не очень понятно, какие именно религиозные обеты не дают написать Военам более правильные тесты на правильных ЯП в Shootout-e?

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

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

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

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

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

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

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

> Без какой потери производительности? Тесты посмотри. Магии не бывает.
...
> Тебе говорят что тесты сами по себе ничего не значат, а ты
> говоришь чтобы тебе дали другие тесты.
Воены, вы там уже определитесь, что ли ...
> Тебя можно бесконечно обманывать, а ты так и будешь верить что тебе говорит кукловод.
Короче, окромя унылого балабольства мы ничего не дождемся.
Этот Воен сломался, вносите следущего!(с)

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

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

Сообщение от Аноним (100), 24-Ноя-24, 17:07

Раст стал ещё более безопасен! Разве другой язык на это способен?

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

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

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

> Раст стал ещё более безопасен!
выращивать крепкие пальмы для вэб-мортышек чтобы с веток не падали сойдёт, для полётов в космос всё равно не годится

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

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

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

Как ты вырвиглазный хлам с ультро токсичными леваками у руля не тестируй, так он хламом и останется.

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

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

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

>За последние три года в библиотеке было выявлено 57 проблем с корректностью работы, из которых 20 были помечены как уязвимости.
Кто тут говорил, что Раст безопасен?

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

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

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

Раст небезопасен там есть unsafe

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

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

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

Гендерно-нейтральные сортиры затрещали по швам. Дepьмokpaтия ox...eвaeт.

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

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

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

Партнёры:

Хостинг:

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

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

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


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


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


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


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


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


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


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


	51. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (50), 24-Ноя-24, 15:26
	Язык си необоснованно сложнее и найти там что-то ещё сложнее вывод очевиден. Хотя вывод понятен по отсутствию софта написанного на раст. Особенно в областях где хваленая работа с памятью могла бы иметь место.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	88. "Инициатива по верификации стандартной библиотеки Rust"	–1 +/–
	Сообщение от erthink_ (?), 24-Ноя-24, 16:30
	> Язык си необоснованно сложнее и найти там что-то ещё сложнее вывод очевиден. Язык Си сильно проще, а С++ отягощен поддержкой обратной совместимости (с позволением всего unsafe что можно в Cи). > Хотя вывод понятен по отсутствию софта написанного на раст. Особенно в > областях где хваленая работа с памятью могла бы иметь место. Так ведь именно активно используется, даже не взирая не упомянутые выше баги. И переписывается на Rust достаточном много, там где либо высоки риски и в совокупности есть целесообразность для бизнеса, либо где что-то кому-то интересно. Другое дело, что в условном debian этого не видно, ибо 90% пакетов появились до раста и вся экосистема "сишная".
	Ответить \| Правка \| Наверх \| Cообщить модератору


	95. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (50), 24-Ноя-24, 16:51
	Может уже пора перестать переписывать и написать что-то новое на самом расте?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	116. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (116), 24-Ноя-24, 17:59
	Лол. Кто ты вообще такой чтобы что-то, кому-то указывать? Особенно разрабам которые свои проекты на Rust перекатывают.Да и нового софта на Rust уже вагон, и игровые движки и редакторы кода, и целая DE с прикладнухой. С разморозкой!
	Ответить \| Правка \| Наверх \| 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ообщить модератору


	42. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (13), 24-Ноя-24, 14:54
	> Поэтому все подобные верификации всегда с массой уточнений и оговорок там написано вполне ясно > Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. > Соответственно, отсутствие "формализированной системы типов" им не только не мешает, но и может помогать (сокращать поверхность). без формального описания не может быть никакой верификации, как это может "помогать" ?
	Ответить \| Правка \| Наверх \| Cообщить модератору


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


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


	79. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (44), 24-Ноя-24, 16:10
	> есть один компилятор и никто точно не знает как он работает, только догадываются. На то и спека, где это все описано, и есть механизм верификации и валидации, который позволяет проверить с тем, что написано в спеке. > Сомневаюсь что кто-то в своём уме пишет на этом доверенный код. У кода, формально верифицируют его корректность. Вы понимаете, что такое корректность?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	82. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (13), 24-Ноя-24, 16:23
	> У кода, формально верифицируют его корректность. Вы понимаете, что такое корректность? есть код на языке программирования и есть код исполняемый процессором, вы разницу вообще понимаете ?
	Ответить \| Правка \| Наверх \| Cообщить модератору


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


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


	54. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от erthink_ (?), 24-Ноя-24, 15:31
	> без формального описания не может быть никакой верификации, как это может "помогать" > ? Ту там же символьные вычисления и местами абстрактная алгебра. Например, можно верифицировать что "компилятор" не нарушает систему типов, без полной формализации и/или верификации самой системы типов. Конечно, такой "компилятор" может быть не в состоянии генерировать исполнимый код. Либо всё-таки уметь это, но уже с подмешиванием не-верифицированного функционала и/или не-верифицированной системы типов. А еще может выясниться, что конкретная система типов может не-покрываться/требовать-большего, чем умеет верифицированная часть компилятора, и/или требовать снятия части ограничений/формулировок введенных для возможности верификации, и т.п. -- Собственно, хотел обратить внимание, что есть "рамки верификации" и почти всегда практическое применение никак в них не помещается.
	Ответить \| Правка \| К родителю #42 \| Наверх \| Cообщить модератору


	93. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (93), 24-Ноя-24, 16:42
	в расте есть MIRI
	Ответить \| Правка \| К родителю #13 \| Наверх \| Cообщить модератору


	16. "Инициатива по верификации стандартной библиотеки Rust"	+2 +/–
	Сообщение от 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ообщить модератору


	40. Скрыто модератором	+/–
	Сообщение от 21yosenior (?), 24-Ноя-24, 14:42
	Он ничего не компилирует, он агитатор который потерялся в ветке ниже. Если непонятно, почему они так цепляются за "кастомный" трансмут. Это опшн-селект такой. Если трансмут стандартный - орём "там ансейф, поэтому не считается". Если трансмут свой - орём "надо было брать стандартный, поэтому не считается". Система непотопляема, как говорится.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	45. "Инициатива по верификации стандартной библиотеки Rust"	+2 +/–
	Сообщение от Аноним (45), 24-Ноя-24, 15:12
	> Нет, это столько же работы, точнее даже больше. Сейф раст ничего не > гарантирует. Но только в фантазиях опеннетных кекспертов-военов супротив раста, не ходящих по своим же ссылкам. https://docs.rs/cve-rs/latest/cve_rs/lifetime_expansion/inde... > How it works > There is a soundness hole in the Rust compiler that allows our domain expansion to work. ... > rustc should infer that one of the lifetimes does not outlive 'static, so that we can’t > use lifetime_translator; however, for whatever reason, it doesn’t, so this exploit works. > See https://github.com/rust-lang/rust/issues/25860 for this bug’s bug report. Воены-кексперты, что с лицом?
	Ответить \| Правка \| К родителю #16 \| Наверх \| Cообщить модератору


	46. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (35), 24-Ноя-24, 15:18
	>> https://github.com/rust-lang/rust/issues/25860 opened on May 28, 2015 >Воены-кексперты, что с лицом? У меня всё прекрасно, а у вас что с лицом уже почти 10 лет?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	52. "Инициатива по верификации стандартной библиотеки Rust"	+/–
	Сообщение от Аноним (50), 24-Ноя-24, 15:30
	Их лицо перекашивает из-за того то их Раст шпыняет кто угодно и легко доказывает бесполезность раста.
	Ответить \| Правка \| Наверх \| Cообщить модератору