Если Rust, значит безопасно

Справделивости ради, в данном случае дело не в языке.

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

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

У тебя раст чешется? Во-первых это не раст, а покажи болячку врачу он тебе скажет что это на самом деле. Во-вторых - «Если написано на Rust, значит безопасно» - это только от полоумных хейтерочков можно услышать, крайне позорный демагогический приём, если чо

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

Проблема не в языке, а в адептах языка, которые распускают миф. И уже появляется вопрос, вот откуда решили, что libcrux является формально верифицированной? Только потому что написали её на Rust? Откуда уязвимости, которые нарушают формальную верификацию? А сколько ещё подобных библиотек, которые переписали на Rust и назвали безопасными и формально верифицируемыми, хотя они таковыми не являются?

The formally verified crypto library for Rust
Независимые исследователи нашли 13 уязвимостей, которые нарушают формальную верификацию
меняют формулировку с «libcrux - the formally verified crypto library» на «libcrux - a high-assurance cryptographic library in Rust»

Буквально на днях в соседнем треде один лорчанин фантазировал о формальной верификации и как ЛЛМки будут ее делать, никогда не ошибаясь :)

Неа, а вот ты как раз применил тот же демагогический приём что и ТС. Те 3-4 ржависта которые ещё остались на лоре, шарят и никогда такого не скажут, остальные в ужасе разбежались от уровня лоровской «аналитеги» (

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

В целом, народ сходится в том, что неполезно

Существует общий консенсус, даже среди тех, кто выступает в пользу безопасности через неясность, что принцип «безопасность через неясность» никогда не должен использоваться в качестве основной меры безопасности. Это, в лучшем случае, вторичная мера, и раскрытие информации о неясности не должно приводить к компрометации.

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

Буквально на днях в соседнем треде один лорчанин фантазировал о формальной верификации и как ЛЛМки будут ее делать, никогда не ошибаясь :)

В разговоре о формальной верификации, наиболее существенно то, какие конкретно свойства программы будут подвергнуты верификации. То есть, существенна формулировка теоремы, доказательство которой будут строить и проверять в рамках верификации. Сюда входит формальная семантика языка программирования, формальное описание предусловий, постусловий и инвариантов верифицируемой программы. Это формализация изначально не очень-то формальных вещей, она никак не защищена от ошибок и неверных интерпретаций.

Откуда взялось доказательство теоремы - хоть человек его придумал, хоть LLM, хоть просто из /dev/urandom байтов накачали - на безошибочности верификации вообще никак не сказывается. Потому что доказательство, после того как было построено, должно пройти формальную механическую проверку (ту самую верификацию), которая ни с человеком, ни с llm вообще никак не связана. Если в доказательстве есть изъяны, проверку оно не пройдёт. Только и всего.

В то же время, поиски доказательства весьма трудоемки. Если бы LLM тут мог бы помогать - было бы просто отлично. Мне-то кажется, что в этой сфере у LLM всё должно быть намного грустнее, чем даже в сфере кодинга. Код де-факто спокойно терпит бредятину (компилируется, запускается, кое-как работает иногда), а вот в доказательстве теоремы бредятина не прокатит. Может, LLM мог бы для каких-то промежуточных несложных лемм бойлерплейт расписывать, чтобы человек на это меньше сил и времени тратил бы.

И кстати, половина кода libcrux на сишочке, и ещё 14% на ассемблере, но претензии только к расту. Может, о чудо, дело определяется не одним только языком.

териритически если llmка едет на квантах то можид

По какой-то причине rust и такие разработчикидюже часто идут рука об руку

Среди плюсовиков тоже разные бывают.

По какой-то причине rust и такие разработчикидюже часто идут рука об руку

Причина называется «предвзятость подтверждения». А если аккуратно посчитать, то с любым языком будет примерно одинаково.

Причина называется «предвзятость подтверждения».

Неа. Rust словил очень много хайпа (уж очень значительные вещи он обещал). Ну и раз тема хайповая, то мухи слетелись на мёд инфоцыгане и хайпожоры естественным образом в неё втянулись.

Rust словил очень много хайпа (уж очень значительные вещи он обещал).

Это так.

инфоцыгане и хайпожоры естественным образом в неё втянулись.

Это тоже так.

Но концентрация багоделов всё равно средняя по больнице. Да и слетелись не только инфоцыгане и хайпожоры, но и просто любители изучения всего нового, или те, кто надеется, что опыт кодинга именно на расте в будущем будет полезен при трудоустройстве. Много кто слетелся. Хайпожоры с инфоцыганами просто заметнее всего: такова уж сама их суть — быть на виду.

То есть, они заметнее, но по количеству они всё равно капля в море. Это примерно как с авиакатастрофами, о которых трубят все СМИ и знает всё население, несмотря на то, что в автомобильных авариях погибает на порядок (или два? не помню) больше людей.

Rust словил очень много хайпа

Не больше чем, в своё время С, С++( и до сих пор жёсткий сектанский культ у обоих ), Java/C#, Go, и сквозь всё это где-то на задворках лисп ), и с соответсвующей поправкой на рост айтешечки

значительные вещи он обещал

То что действительно обещал, вобщем-то, честно выполняет

Плюсовики не бегали по всему гитхабу создавая ишуи «переписать на с++» под всеми проектами

вот откуда решили, что libcrux является формально верифицированной? Только потому что написали её на Rust?

Похоже, слишком многие путают «язык формально гарантирует X и Y» с «программы на языке формально верифицированы».

Разрабы наверняка не путают, но эксплуатируют чужое невежество.

А почему нельзя «The formally verified crypto library for C»?

Ведь речь идет о формальной верификации?

«The formally verified crypto library for Rust»

– Доктор, мой сосед говорит, что может жену три раза за ночь, а ведь ему 90 лет.
– В чём проблема? Вы тоже говорите.

И кстати, половина кода libcrux на сишочке, и ещё 14% на ассемблере, но претензии только к расту.

У меня есть подозрения, что ОП об этом не знал, а также о том, что такое формальная верификация) Но наброс все равно пошел-поехал)

Не больше чем, в своё время С, С++

Это неправда.

То что действительно обещал, вобщем-то, честно выполняет

И снова неправда. Со степенью выполнения есть нестыковочки. Наобещали с три короба, а выполнили как смогли:
1. Для safe-кода (и borrow checker) нет доказательства soundness, за то были (или до сих пор есть? не слежу за темой) примеры, когда safe код проходит проверку borrow checker и при этом осуществляет некорректную работу с памятью;
2. На практике большинство проектов на rust содержат unsafe-код, что аннулирует обещанные мрии о memory-safety.

Претензии тут не по технической части (понятно, что тут best effort и реальный прогресс), а по части инфоцыганства.

Да ладно, при обсуждении любого проекта на си бурление по этому поводу. Из самого громкого гцц, сам линукс.

или до сих пор есть? не слежу за темой

Давно исправили. cve-rs требует античную версию Растишки, на свежих не канпеляется.

А почему нельзя «The formally verified crypto library for C»?

+1

Для си-шки хотя бы есть варианты формальной семантики самого языка (его подмножества). А для растишки есть?

https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

что аннулирует обещанные мрии о memory-safety.

С таким подходом вообще нет языков с memory-safety. Всякие питоны, явы и пхп в пролёте - у них есть ffi, а значит никаких гарантий.

Естественно, если в питоньем процессе работает какая-то левая либа на си-шке, то именно она является слабым звеном, и гарантий тут как у кода на си-шке.

Ни о каком «everyone to build reliable ... software» в ситуации с FFI даже речи идти не может, это автоматически становится упражнением для избранных, с обмазыванием си-шного кода санитайзерами, фаззинг-тестами, и тд. Ну или без обмазывания. Но в любом случае, с принятием соответствующих рисков насчет отсутствия memory safety.

Как будто что-то плохое. И в 90-х не было гитхаба, но вот с сишки на плюсцы, благодоря хоть какой-то совместимости языков всё ещё переписывают.

Давно исправили

Держи свежий 🐽
Thread safe in rust (комментарий)

«Если написано на Rust, значит безопасно».

С точки зрения идиотов недоучек, несомненно.

Это всё то же самое, ошибочный вывод статического лайфтайма, ничего свежего.

Если Rust, значит безопасно...

Три раза «Ха!» 😁

«Глобально-надёжно.» — говорили они...

Где-то я это уже слышал.

Те 3-4 ржависта, которые действительно что-то пишут, они именно пишут. А вот так называемые лоровские ржависты они пишут только на лоре и только мантры.

Это я прямо из cve-rs накопипастил, чтобы в одном файле было. Не знаю, чего у него там не канпеляется

Независимые исследователи нашли 13 уязвимостей, которые нарушают формальную верификацию,

И причём тут Rust, когда ошибка в логике? Ты хоть пруф-то читал?

Ну неееет. Это конечно фишка растовиков.

Те 3-4 ржависта, которые действительно что-то пишут, они именно пишут. А вот так называемые лоровские ржависты они пишут только на лоре и только мантры.

Да как-то мантры в основном от хейтеров идут. Сами выдумали каких-то фанатиков, у которых «на Rust, значит безопасно», сами подписались везде на тег rust и жадно выискивают баги в софте на нём, чтобы затем сказать «ага, не безопасно!», хотя никто и не заявлял, что Rust даёт все возможные гарантии — только вполне конкретные. Нет, может и были 1–2 сумасшедших (и то не факт, что не тролли), которые несли бред, но теперь этот миф на всех программистов на Rust распространяют, потому что так жить проще. Ну или на «большинство». Хотя это такой же бред, как «арч ломается при каждом обновлении», или «все маководы — геи». Больше таких мифов и приписываний оппонентам заведомо идиотской позиции только в политических дискуссиях (с обеих сторон причём), но их примеров я тут приводить не буду, дабы не разжигать.

Казалось бы, вроде среди линуксоидов должно быть больше людей с критическим мышлением и умением не делить мир на только чёрное и белое. Но нет, есть вопросы, в которых эмоции давлеют над любым здравым смыслом. Наблюдать за этим иногда смешно, но всё чаще — стыдно как-то (испанский стыд).

Буквально на днях в соседнем треде один лорчанин фантазировал о формальной верификации и как ЛЛМки будут ее делать, никогда не ошибаясь :)

я там же и прокомментировал ситуацию с libcrux: там дело не в формальной верификации, а в том что кое кто (а именно ребята из криспен) прибили себе вывеску «формально верифицированное» на то что по факту таким не являлось. И ещё и забанили тех кто сообщил о проблемах (позже втихаря применив забаненные патчи от своего имени.. скромняги). Ну теперь вводящую в заблуждение вывеску убрали. И это не может не радовать.

я приводил пример, в прошлом месяце эксперементальная нейросетка (вроде Аристотеля,но чуть поинтереснее) доказала лемму Полищука-Шпильмана. Получилось около 2000 строк , она повыносила леммы, в целом весьма неплохой код. У неё ушло около 8 часов и стоило это порядка 250 долларов. Понятно, что инженер 2000 строк за 8 часов не напишет.

Уже давненько перешли к принципу responsible disclosure. Т.е. проблема сообщается приватно и даётся 3-6 месяцев на её устранение, потом идёт публикация. По взаимному согласию можно и раньше, или если это принципиальная уязвимость в железе, то и позже.

Но некоторые до сих пор не в курсе, и вместо вознаграждения присылают письмо с угрозами. Вот недавно: Я нашёл уязвимость, а они - адвоката.

Еще как только раст появился, уже 10 лет назад, на лорчике @tailgunner развенчивал straw man, что раст защищает не от всего, а только от определенного класса ошибок, с тех пор ничего не поменялось)

Казалось бы, какая-то команда сделала опенсорсные криптографические либы, старались сделать их безопасными, писали на раст, делали формальную верификацию, хоть и налажали с ней, нет, нужно все обосрать, и, самое главное, раст заодно)

Концентрация багоделов может и средняя, а вот концентрация выдуманной крутости - повышенная.

Выдуманных слов о выдуманной крутости от хейторов — точно повышенная.

Фанатизм по формальным верификациям - такая же глупость, как и фанатизм по расту.

Да нет, много переписывателей на раст шумят что «мы сделаем код безопасным в отличие от Си». Даже в каких-то странах гос органы на эту тему высказываются.

много переписывателей на раст шумят

А по-моему, совсем не много. Было несколько переписывателей, которые шумели очень громко. Но громкость не равна количеству.

вот концентрация выдуманной крутости - повышенная

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