| 1.3, Аноним (3), 11:39, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +17 +/– |
Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать их надёжность надо доказать, что P != NP)), а что в реализации сишники за границы буферов не вышли и что реализация соответствует спецификации, которую именно под неё написали ресёрчеры.
| | |
| |
| 2.11, Аноним (11), 12:32, 19/04/2025 [^] [^^] [^^^] [ответить]
| –4 +/– | |
> чтобы доказать их надёжность надо доказать, что P != NP
есть квантовые компы, при чём тут надёжность и П != НП?
| | |
| 2.21, Аноним (-), 15:55, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать
> их надёжность надо доказать, что P != NP)),
Э, на минуточку, зачем это доказывать для вычислений хешей? Это ж не публичная криптография.
| | |
| |
| 3.24, Аноним (24), 16:15, 19/04/2025 [^] [^^] [^^^] [ответить] | +3 +/– | Эмм, вообще-то все реальные схемы с публичной криптографией опираются на коллизи... большой текст свёрнут, показать | | |
|
| 2.26, Аноним (26), 16:47, 19/04/2025 [^] [^^] [^^^] [ответить]
| +4 +/– | |
> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов
Заголовок не хайповый - это просто нелепая отсебятина от переводчика. В оригинальных текстах слово "математика" даже близко нигде не упоминается.
Это зовется "формальная верификация".
| | |
| |
| 3.67, Fyjy (?), 10:17, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
А что по вашему такое "формальная верификация"? Чистое математическое моделирование.
Первое попавшееся определение: "Формальная верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ."
| | |
| 3.68, Fyjy (?), 10:31, 20/04/2025 [^] [^^] [^^^] [ответить] | +/– | Из википедии https ru wikipedia org wiki D0 A4 D0 BE D1 80 D0 BC D0 B0 D0 BB ... большой текст свёрнут, показать | | |
| 3.69, Fyjy (?), 10:37, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
И, кстати, в описании самого HACL∗ сказано "First, we describe HACL∗, an efficient library of cryptographic primitives that are verified to be memory safe, side-channel resistant, and, where there exists a simple mathematical specification, functionally correct"
| | |
|
| 2.27, Аноним (-), 16:50, 19/04/2025 [^] [^^] [^^^] [ответить] | –1 +/– | Они доказали следующее The Low source code for each primitive is verified for ... большой текст свёрнут, показать | | |
| |
| 3.47, Аноним (47), 18:40, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
> (мне кажется, проблема останова хуже, чем любая NP проблема).
ну вот это что такое? как можно понятие неразрешимости мешать с понятием сложности? Ну вот на днях была статья под заголовком "The Halting Problem is a terrible example of NP-Harder", что простите? пример нп-сложной? это что за ересь?
//buttondown.com/hillelwayne/archive/the-halting-problem-is-a-terrible-example-of-np/
| | |
| 3.49, Аноним (49), 18:55, 19/04/2025 [^] [^^] [^^^] [ответить]
| –1 +/– | |
> фишка в том, что когда rust загнал программиста в клетку shared^mutable, то после этого отсутствие датарейсов легко доказывается
Этот kremlin (переименнованный согласно повестке в karamel) загоняет более жесткие ограничения чем раст.
| | |
|
| 2.32, Аноним (32), 17:11, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
А где там сишники? Онм вам уже по ночам снятся? В новости сказано, что библиотека написана на F*.
| | |
| |
| 3.45, Аноним (45), 18:09, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Пока этот Ф не лезет в проекты на сишке с нетерпимой необходимостью засунуть этот Ф прямо в проект мотивируя это тем что он там какой-то супер какой а сишка эта ващще (нахрен тогда припёрлись) - всем сишникам включая меня на этот Ф пофик, пусть компилит там себе в питоне что ему надо
| | |
|
| 2.78, Vkni (ok), 19:35, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
 +1
Вообще бесит это вечное «математически доказано» без подробностей. Как будто мы не знаем, что доказывать можно что угодно. Например, что количество символов не превышает полтора миллиарда.
> что реализация соответствует спецификации, которую именно под неё написали ресёрчеры.
Которая просто написана на другом языке программирования, и в которой тоже можно понаделать ошибок.
| | |
|
| |
| 2.22, Аноним (-), 16:02, 19/04/2025 [^] [^^] [^^^] [ответить]
| –1 +/– | |
> Стальная дверь в картонной хижине.
Не понимаю за что ему минус. Этому брейнфаку-2.0 с его pypy и чем там еще и характерными программерами - мало что поможет. Там код обычно пишут - толи скопировав из AI, толи программер сам такое спагетти нагенерил, обработка ошибок и всяких странных действий пользователя? Что вы! Поэтому большей части этих картонных макетов можно CVE навесить одной левой. Но большая их часть даже этого просто не стоит. Много чести для одноразовых картонных шляп с периодом жизни в год.
| | |
| |
| 3.33, Аноним (32), 17:17, 19/04/2025 [^] [^^] [^^^] [ответить]
| –1 +/– |
Не нервничайте так. Реальные программы на ugly Rust, тем более, все будут писаться с помощью этого самого AI.
| | |
| 3.64, Аноним (-), 09:13, 20/04/2025 [^] [^^] [^^^] [ответить]
| –1 +/– |
Сейчас курсы безопасности есть вроде, можно и понять о чем он. Я кстати согласен.
| | |
|
|
| 1.5, Аноним (5), 11:42, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| –1 +/– |
Математическая верификация реализации крипто функций в библиотеке HACL* - это очень круто.
Осталось только верифицировать саму среду исполнения - Python и все будет совсем замечательно.
| | |
| |
| 2.6, Аноним (6), 11:49, 19/04/2025 [^] [^^] [^^^] [ответить]
| –1 +/– |
Зачем? Вон в pyca/cryptography ржавчину запихнули, и вот это уж действительно сбоку припёка. А тут всё в порядке, надёжные алгоритмы должны быть в стандартной библиотеке.
| | |
|
| 1.14, Ivan_83 (ok), 12:56, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| –4 +/– |
 Фигнёй какой то страдают.
Для начала не понятно как вообще можно было так реализовать (скопипастить референсную реализацию на С) чтобы там накосячить.
Потом вместо использования SIMD SHA они опять что то не то сделали.
В общем питон стремительно копит техдолг и пилит важные либы на фриковских языках, видимо очень хочется работать только в убунте на амд64, примерно как опенврт собирается на полутора линуксах.
| | |
| |
| 2.28, Аноним (26), 16:57, 19/04/2025 [^] [^^] [^^^] [ответить] | +/– | Опять Ivan_83 не понимает, что происходит 128557 Очень просто написать на ды... большой текст свёрнут, показать | | |
| 2.36, Аноним (32), 17:23, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
OpenWRT, как бы сама по себе, ОС. Или вы имеете ввиду, полностью кросс-собрать его из исходников под обычным GNU/Linux на компе? Так, вдоде, на любом дистре это возможно сделать.
| | |
| |
| 3.82, Ivan_83 (ok), 23:18, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Да, ага.
Если получится.
У меня ощущение что пилят под убунту или ещё что то попсовое.
На фре/маке собрать можно только помучавшись, как итог мне надоело и я завёл виртуалку с убунтой.
| | |
|
| 2.59, Фрол (?), 04:44, 20/04/2025 [^] [^^] [^^^] [ответить] | –2 +/– | да ваще что может хорошего сказать существо с ником иван сиди ваня и не высов... большой текст свёрнут, показать | | |
| |
| 3.70, Аноним (-), 11:51, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало и с минимальным ущербом для окружающих.
>воспоминание о пыхтящей опе из под стола. да, она реально ковыряла там пилочкой для ногтей дыру для кнопки питания. которая кнопка от ласковой женской руки улетела внутрь корпуса и там повисла.
Сравнил себя с женщиной - офисным работником. Ну ты и херой!
>люди вообще делятся на инженеров и на всех остальных
Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины. Жалкое и убогое зрелище представляют из себя инженеры.
| | |
| |
| 4.75, Фрол (?), 12:57, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
> алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало
...и не туда, куда надо.
> Сравнил себя с женщиной - офисным работником.
ты откуда такой местечковый мачо вылез? у этой дамы походу диплом с примата был. офисный работник, мой асс.
> Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины.
Кнут с Раскиным передают привет и спрашивают, а они тогда - кто?
| | |
| |
| 5.77, Аноним (47), 14:23, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
> Кнут с Раскиным передают привет и спрашивают, а они тогда - кто?
кек, с коих пор они инженера?
| | |
|
|
|
| 2.62, freehck (ok), 08:44, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
 > питон <...> пилит важные либы на фриковских языках
Не-не-не, они не пилят. Эти либы написаны другими людьми, куда более профессиональными. )
> питон стремительно копит техдолг
Ну, если подходить формально, то это -- часть их техдолга. Но питон пилится прикладниками, и следовательно алгоритм приоритезации разработки простой: нашёлся кто-то, кому именно это было нужно, он оплатил и пропихнул задачу вперёд. И только. А фигня она в глобальном плане или не фигня -- вопрос десятый.
| | |
| |
| 3.83, Ivan_83 (ok), 23:21, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Да это всё понятно и питон весь такой в белом пальте.
А виноваты какие то фрики которые py-cryptography пилят.
Только по итогу эта либа глубого и много где в завимостях и без неё питон почти бесполезен, как ОС без программ.
| | |
|
|
| 1.17, Аноним (47), 15:09, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +1 +/– |
Project Everest - название говорит само за себя, все чем занимаются майки - булшит псевдонаучный, чем им TLA+ не понравился, AWS уже свалил с него как только Лемпорта на пенсию отправили?
| | |
| 1.25, zionist (ok), 16:39, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +/– |
 > По производительности библиотека HACL* близка к OpenSSL, но в отличие от последней предоставляет дополнительные гарантии надёжности и безопасности.
Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами? Подозрительно!
| | |
| |
| 2.29, Аноним (26), 16:59, 19/04/2025 [^] [^^] [^^^] [ответить]
| +1 +/– | |
> Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами?
Потому что дядя-работодатель на заплатил за это Тео.
| | |
| 2.31, Аноним (-), 17:04, 19/04/2025 [^] [^^] [^^^] [ответить] | +1 +/– | Ничего подозрительного Математические доказательства кода только сейчас становя... большой текст свёрнут, показать | | |
| 2.37, Аноним (32), 17:28, 19/04/2025 [^] [^^] [^^^] [ответить]
| +1 +/– |
Потому, что INRIA не интересен Тео с его 0.01%-ной ОС? Только его OpenSSL был бы интересен, но, наверное, написанное именно на Сишке математически не верифицировать.
| | |
| |
| 3.92, Ivan_83 (ok), 05:32, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Забавно слышать.
Чтоб вы понимали это именно OpenBSD является апстримом в мире защитных механизмов.
Из него тащат вся и в венду и в линкус и во фрю и хз куда ещё.
К сожалению libressl умирает - его забросили поддерживать меинтейнеры попсовых дистров.
И я забросил - мне надоело постоянно тратить на это время.
| | |
|
|
| 1.30, Аноним (30), 17:03, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +1 +/– |
Направление неплохое, не какое-то раст безобразие. Но мелкософт и инструментарий напрягают.
| | |
| |
| 2.41, Нуину (?), 18:01, 19/04/2025 [^] [^^] [^^^] [ответить]
| +1 +/– | |
> Но мелкософт и инструментарий напрягают
А то, что Гвидо работает в мс и команда ускорения питона (да, такая есть) из мс тебя не напрягает?
| | |
|
| 1.42, yurikoles (ok), 18:03, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +2 +/– |
 >Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами.
Мне кажется это слабое звено. Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C, производный от него.
| | |
| |
| 2.48, Аноним (47), 18:49, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
> если реально всё равно используется выхлоп на C
тут по идеи выхлоп то примитивный, с минимальными конструкциями языка которые не гарантируют корректность, то есть всякого рода жонглирование указателями не используется и т.д.
как по мне, все это ересь, на основе спецификации должен генерироваться прямой конкретный машинный код, а не программы на других формальных языках.
| | |
| 2.50, Аноним (26), 19:01, 19/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
> Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C,
Разница в том, что С код в этом случае сгенерирован автоматически, а не написан ручками.
| | |
| 2.53, Аноним (32), 19:17, 19/04/2025 [^] [^^] [^^^] [ответить]
| +3 +/– |
Удивлю вас, но в конечном итоге, выхлоп в машинных кодах. А там нет никаких чекеров боровов.
| | |
| |
| 3.58, Аноним (47), 02:28, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
KaRaMeL (formerly known as KReMLin) is a tool that extracts an F* program to readable C code: K&R meets ML!
If the F* program verifies against a low-level memory model that talks about the stack and the heap; if it is first-order; if it obeys certain restrictions (e.g. non-recursive data types) then KaRaMeL will turn it into C.
перевод с англ. нужен?
| | |
| |
| 4.80, Аноним (56), 21:38, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
Дальше не осилил прочитать?
We state that the compilation of such F* programs to C preserves semantics. We start from Low*, a subset of F*, and relate its semantics to CompCert's Clight.
| | |
| |
| 5.81, Аноним (47), 23:12, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
для вас "доказывается экивалентность" равносильно "preserves semantics"?
Writing in Low*, the programmer enjoys the full power of F* for proofs and specifications. At compile-time, proofs are erased, leaving only the low-level code to be compiled to C. In short:
the code is low-level, but the verification is not.
| | |
| |
| 6.85, Аноним (56), 00:16, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
Читай внимательно
At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.
| | |
| |
| 7.86, Аноним (47), 04:07, 21/04/2025 [^] [^^] [^^^] [ответить] | +/– | Вот вы пишите В карамел доказывается , в карамель ничего не доказывается в смы... большой текст свёрнут, показать | | |
| 7.87, Аноним (47), 04:23, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
//github.com/FStarLang/karamel/blob/master/DESIGN.md
Тут вот по шагам все расписано, что делает конкретно карамель, и я не вижу ни одного "доказывающего" шага.
| | |
|
|
|
|
|
| 2.90, Ivan_83 (ok), 05:26, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Ты смешной.
Тебе не нравится язык который ты не не понимаешь и ты думаешь что какой то магический язык решит все проблемы.
С может транслироватся почти 1в1 к машинному, старые компеляторы в оптимизации не умели и С код легко угадывался по асмовым листингам.
Только вот бывают проблемы и с логикой в коде и с железом, так что если ты решил достичь совершенства (зачем то), то тебе и железо надо особенное какое то, явно не то что у тебя щас, и какие то особенные пейсатели кода, тоже не те что сейчас.
Удачи.
| | |
|
| 1.43, Нуину (?), 18:03, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| –1 +/– | |
Штош... будет крайне забавно, когда в реализации найдут уязвимость)
зы что-то скорости? Медленнее небось?
| | |
| 1.54, нокия (?), 23:23, 19/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +/– | |
Это может быть полезно не только в пайтон, конечно:
Low Subset*
Compiles to C/Wasm via KaRaMeL, enabling verified systems code (e.g., HACL*’s cryptographic primitives)
Очень круто!
| | |
| 1.72, Аноним (72), 11:54, 20/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +1 +/– |
Что такое эти математически доказанные функции? Я пытался разобраться, искал, нашел в итоге видео где человек прочитал математическое заклинание похожее на доказательство из геометрии, и всё, код доказан. Это так работает?
| | |
| |
| 2.74, Аноним (-), 12:48, 20/04/2025 [^] [^^] [^^^] [ответить]
| +1 +/– |
Тут одна тонкость. Математическое заклинание должно 100% подходить к задаче. Иначе волшебство не сработает.
| | |
| 2.76, Аноним (47), 14:16, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
а где ссылка на видео, чтобы хоть как-то это прокомментировать?
| | |
|
| 1.79, Аноним (79), 21:36, 20/04/2025 [ответить] [﹢﹢﹢] [ · · · ]
| +/– |
Между строк читается, что весь накопленный за десятки лет багаж открытого кода будет на перспективе ближайших лет полностью выброшен на помойку из-за того, что нет возможности надежно оценить его безопасность.
OpenSSL ни разу не жалко, но эта же логика будет в конце концов применяться к любому коду. Новый NIH синдром.
| | |
| |
| 2.84, Аноним (84), 23:33, 20/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Не будет. Попытки создать язык с формально доказуемым выводом создавались давно. Coq как средство доказательства теорем, Haskell,... Но так на них и не перешли. Зато развилось нечто под названием Python....
| | |
| 2.88, Ivan_83 (ok), 05:19, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Ничего не будет.
Даже банальное переписывание требует много времени.
Безопасность - ну такое себе, в текущем виде всё более чем годно и проблемы скорее с потерей контроля над зависимостями, притом у новых языков это прям со старта, а у старых по историческим причинам зависисмости в основном руками поштучно и такой проблемы нет.
Переполнения, выходы за границы и прочее - проще починить чем переделывать.
Но есть конечно некоторые проекты где всё совсем плохо в коде, архитектуре и тп, но это обычно нишевые штуки. Вот такое реально лучше переписать с нуля, но желающих особо нет - оно не попсовое.
А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус.
| | |
| |
| 3.94, Аноним (94), 14:17, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
>А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус.
Это просто форки, ничего там почти не переписывали
| | |
| |
| 4.95, Ivan_83 (ok), 15:36, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– | |
Да как же!
libressl Тео сильно переписал.
Боринг я не смотрел, вроде его на кресты перевели, да и оно за пределами хрома особо не юзается, кажется это сделали чтобы ГОСТ и прочие стандарты надёжно огородить от браузера.
| | |
|
|
| 2.89, Ivan_83 (ok), 05:22, 21/04/2025 [^] [^^] [^^^] [ответить]
| +/– |
Даже больше скажу, вот прям за деньги: процесс длительный, тяжёлый и сплошные затраты без профита. Всех желающих просто пошлют в лес, если опять не удастся напилить грантов за счёт каких нибудь налогоплательщиков.
И даже когда начнут и может даже что то перепишут - старй код никуда не денется, всякие девайсы с ним будут ещё десятки лет жить. И отдельные старые системы тоже десятилетия будут использоватся, как кобол вон до сих пор в проде.
| | |
|
|
