forum.opennet.ru - "В Python задействованы криптоалгоритмы с математическим доказательством надёжности" (66)

"В Python задействованы криптоалгоритмы с математическим доказательством надёжности"

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

"В Python задействованы криптоалгоритмы с математическим доказательством надёжности"	+/–
Сообщение от opennews (??), 19-Апр-25, 11:30
Объявлено об успешном завершении инициативы по замене в Python реализаций криптографических алгоритмов, предлагаемых в модулях hashlib и hmac, на варианты с математическим доказательством надёжности, подготовленные проектом "HACL*". Работа по переходу на функции с математическим доказательством надёжности велась с 2022 года и была инициирован после выявления переполнения буфера в реализации алгоритма SHA3, используемой в Python-модуле hashlib... Подробнее: https://www.opennet.dev/opennews/art.shtml?num=63104
Ответить \| Правка \| Cообщить модератору

Оглавление

Заголовок хайповый Математически доказана не надёжность алгоритмов чтобы док, Аноним (3), 11:39 , 19-Апр-25, (3) +16

есть квантовые компы, при чём тут надёжность и П НП , Аноним (11), 12:32 , 19-Апр-25, (11) –4

https opennet ru 61700-nist, Аноним (16), 15:09 , 19-Апр-25, (16) –1

где в новости про PQC там обычная крипта, Аноним (11), 17:59 , 19-Апр-25, (40)

Э, на минуточку, зачем это доказывать для вычислений хешей Это ж не публичная к, Аноним (-), 15:55 , 19-Апр-25, (21)

Эмм, вообще-то все реальные схемы с публичной криптографией опираются на коллизи, Аноним (24), 16:15 , 19-Апр-25, (24) +2

Заголовок не хайповый - это просто нелепая отсебятина от переводчика В оригинал, Аноним (26), 16:47 , 19-Апр-25, (26) +3

А что по вашему такое формальная верификация Чистое математическое моделирова, Fyjy (?), 10:17 , 20-Апр-25, (67)
Из википедии https ru wikipedia org wiki D0 A4 D0 BE D1 80 D0 BC D0 B0 D0 BB , Fyjy (?), 10:31 , 20-Апр-25, (68)
И, кстати, в описании самого HACL 8727 сказано First, we describe HACL 8727, Fyjy (?), 10:37 , 20-Апр-25, (69)

Они доказали следующее The Low source code for each primitive is verified for , Аноним (-), 16:50 , 19-Апр-25, (27) –1

ну вот это что такое как можно понятие неразрешимости мешать с понятием сложнос, Аноним (47), 18:40 , 19-Апр-25, (47)
Этот kremlin переименнованный согласно повестке в karamel загоняет более жестк, Аноним (49), 18:55 , 19-Апр-25, (49) –1

Да, именно благодаря этому они могут доказывать больше , Аноним (-), 01:42 , 20-Апр-25, (57)

А где там сишники Онм вам уже по ночам снятся В новости сказано, что библиотек, Аноним (32), 17:11 , 19-Апр-25, (32)

Пока этот Ф не лезет в проекты на сишке с нетерпимой необходимостью засунуть это, Аноним (45), 18:09 , 19-Апр-25, (45)

1Вообще бесит это вечное 171 математически доказано 187 без подробностей К, Vkni (ok), 19:35 , 20-Апр-25, (78)

Стальная дверь в картонной хижине , YetAnotherOnanym (ok), 11:42 , 19-Апр-25, (4) +2

с тремя стенами, Омнонном (?), 12:02 , 19-Апр-25, (9)
Не понимаю за что ему минус Этому брейнфаку-2 0 с его pypy и чем там еще и хара, Аноним (-), 16:02 , 19-Апр-25, (22) –1

Не нервничайте так Реальные программы на ugly Rust, тем более, все будут писать, Аноним (32), 17:17 , 19-Апр-25, (33) –1
Сейчас курсы безопасности есть вроде, можно и понять о чем он Я кстати согласен, Аноним (-), 09:13 , 20-Апр-25, (64) –1

Математическая верификация реализации крипто функций в библиотеке HACL - это оч, Аноним (5), 11:42 , 19-Апр-25, (5) –1

Зачем Вон в pyca cryptography ржавчину запихнули, и вот это уж действительно сб, Аноним (6), 11:49 , 19-Апр-25, (6) –1

Фигнёй какой то страдают Для начала не понятно как вообще можно было так реализо, Ivan_83 (ok), 12:56 , 19-Апр-25, (14) –4

Опять Ivan_83 не понимает, что происходит 128557 Очень просто написать на дыр, Аноним (26), 16:57 , 19-Апр-25, (28)
OpenWRT, как бы сама по себе, ОС Или вы имеете ввиду, полностью кросс-собрать е, Аноним (32), 17:23 , 19-Апр-25, (36)

Да, ага Если получится У меня ощущение что пилят под убунту или ещё что то попсо, Ivan_83 (ok), 23:18 , 20-Апр-25, (82)

да ваще что может хорошего сказать существо с ником иван сиди ваня и не высов, Фрол (?), 04:44 , 20-Апр-25, (59) –2

алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит используя, Аноним (-), 11:51 , 20-Апр-25, (70)

и не туда, куда надо ты откуда такой местечковый мачо вылез у этой дамы похо, Фрол (?), 12:57 , 20-Апр-25, (75)

кек, с коих пор они инженера , Аноним (47), 14:23 , 20-Апр-25, (77)

Не-не-не, они не пилят Эти либы написаны другими людьми, куда более профессиона, freehck (ok), 08:44 , 20-Апр-25, (62)

Да это всё понятно и питон весь такой в белом пальте А виноваты какие то фрики к, Ivan_83 (ok), 23:21 , 20-Апр-25, (83)

Project Everest - название говорит само за себя, все чем занимаются майки - булш, Аноним (47), 15:09 , 19-Апр-25, (17) +1
Интересно, почему Тео, до сих пор, не озаботился математическими доказательствам, zionist (ok), 16:39 , 19-Апр-25, (25)

Потому что дядя-работодатель на заплатил за это Тео , Аноним (26), 16:59 , 19-Апр-25, (29) +1
Ничего подозрительного Математические доказательства кода только сейчас становя, Аноним (-), 17:04 , 19-Апр-25, (31) +1
Потому, что INRIA не интересен Тео с его 0 01 -ной ОС Только его OpenSSL был бы, Аноним (32), 17:28 , 19-Апр-25, (37) +1

Забавно слышать Чтоб вы понимали это именно OpenBSD является апстримом в мире за, Ivan_83 (ok), 05:32 , 21-Апр-25, (92)

Направление неплохое, не какое-то раст безобразие Но мелкософт и инструментарий, Аноним (30), 17:03 , 19-Апр-25, (30) +1

А то, что Гвидо работает в мс и команда ускорения питона да, такая есть из мс , Нуину (?), 18:01 , 19-Апр-25, (41) +1

Мне кажется это слабое звено Непонятно какая разница на сколько надёжен оригина, yurikoles (ok), 18:03 , 19-Апр-25, (42) +2

тут по идеи выхлоп то примитивный, с минимальными конструкциями языка которые не, Аноним (47), 18:49 , 19-Апр-25, (48)
Разница в том, что С код в этом случае сгенерирован автоматически, а не написан , Аноним (26), 19:01 , 19-Апр-25, (50)
Удивлю вас, но в конечном итоге, выхлоп в машинных кодах А там нет никаких чеке, Аноним (32), 19:17 , 19-Апр-25, (53) +3
В карамел доказывается экивалентность семантики кода на F и С, Аноним (56), 01:05 , 20-Апр-25, (56)

KaRaMeL formerly known as KReMLin is a tool that extracts an F program to rea, Аноним (47), 02:28 , 20-Апр-25, (58)

Дальше не осилил прочитать We state that the compilation of such F programs to , Аноним (56), 21:38 , 20-Апр-25, (80)

для вас доказывается экивалентность равносильно preserves semantics Writing , Аноним (47), 23:12 , 20-Апр-25, (81)

Читай внимательноAt extraction time, specifications and proofs are erased, and t, Аноним (56), 00:16 , 21-Апр-25, (85)

Вот вы пишите В карамел доказывается , в карамель ничего не доказывается в смы, Аноним (47), 04:07 , 21-Апр-25, (86)
github com FStarLang karamel blob master DESIGN mdТут вот по шагам все расписа, Аноним (47), 04:23 , 21-Апр-25, (87)

Ты смешной Тебе не нравится язык который ты не не понимаешь и ты думаешь что как, Ivan_83 (ok), 05:26 , 21-Апр-25, (90)

Штош будет крайне забавно, когда в реализации найдут уязвимость зы что-то ско, Нуину (?), 18:03 , 19-Апр-25, (43) –1
Это может быть полезно не только в пайтон, конечно Low Subset Compiles to C Wasm, нокия (?), 23:23 , 19-Апр-25, (54)
Что такое эти математически доказанные функции Я пытался разобраться, искал, на, Аноним (72), 11:54 , 20-Апр-25, (72) +1

Тут одна тонкость Математическое заклинание должно 100 подходить к задаче Ина, Аноним (-), 12:48 , 20-Апр-25, (74) +1
а где ссылка на видео, чтобы хоть как-то это прокомментировать , Аноним (47), 14:16 , 20-Апр-25, (76)

Между строк читается, что весь накопленный за десятки лет багаж открытого кода б, Аноним (79), 21:36 , 20-Апр-25, (79)

Не будет Попытки создать язык с формально доказуемым выводом создавались давно , Аноним (84), 23:33 , 20-Апр-25, (84)
Ничего не будет Даже банальное переписывание требует много времени Безопасность , Ivan_83 (ok), 05:19 , 21-Апр-25, (88)

Это просто форки, ничего там почти не переписывали, Аноним (94), 14:17 , 21-Апр-25, (94)

Да как же libressl Тео сильно переписал Боринг я не смотрел, вроде его на кресты, Ivan_83 (ok), 15:36 , 21-Апр-25, (95)

Даже больше скажу, вот прям за деньги процесс длительный, тяжёлый и сплошные за, Ivan_83 (ok), 05:22 , 21-Апр-25, (89)

Там в новом пистоне еще t-strings будут шаблонные строки, также известные как t, Аноним (96), 21:21 , 21-Апр-25, (96)

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

3. "В Python задействованы криптоалгоритмы с математическим дока..." +16 +/–

Сообщение от Аноним (3), 19-Апр-25, 11:39

Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать их надёжность надо доказать, что P != NP)), а что в реализации сишники за границы буферов не вышли и что реализация соответствует спецификации, которую именно под неё написали ресёрчеры.

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

11. "В Python задействованы криптоалгоритмы с математическим дока..." –4 +/–

Сообщение от Аноним (11), 19-Апр-25, 12:32

> чтобы доказать их надёжность надо доказать, что P != NP
есть квантовые компы, при чём тут надёжность и П != НП?

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

16. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (16), 19-Апр-25, 15:09

https://opennet.ru/61700-nist

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

40. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (11), 19-Апр-25, 17:59

где в новости про PQC? там обычная крипта

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

21. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (-), 19-Апр-25, 15:55

> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать
> их надёжность надо доказать, что P != NP)),
Э, на минуточку, зачем это доказывать для вычислений хешей? Это ж не публичная криптография.

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

24. "В Python задействованы криптоалгоритмы с математическим дока..." +2 +/–

Сообщение от Аноним (24), 19-Апр-25, 16:15

Эмм, вообще-то все реальные схемы с публичной криптографией опираются на коллизионную стойкость. Это такое фундаментальное свойство криптографических хеш-функций - стойкость к коллизиям: для заданной функции очень трудно вычислительно подобрать коллизию. Иначе делается такая атака: подбирается коллизия, тебе даётся документ "получите миллион баксов, распишитесь", ты его радостно подписываешь. А второй документ с таким же хешом (благодаря чему твоя подпись из первого документа элементарно перешлёпывается на второй), что "ты подарил всё имущество мошеннику, и подписался на разбор на органы" -- с ним идётся в суд "вот тут товарищ договор подписал, а не исполняет".
А если P=NP, то сложных задач в принципе не бывает и все хеши не коллизионно стойкие. А публичная криптография не существует в принципе.  Ежели хеши существуют, то как минимум будут подписи Лэмпорта.

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

26. "В Python задействованы криптоалгоритмы с математическим дока..." +3 +/–

Сообщение от Аноним (26), 19-Апр-25, 16:47

> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов
Заголовок не хайповый - это просто нелепая отсебятина от переводчика. В оригинальных текстах слово "математика" даже близко нигде не упоминается.
Это зовется "формальная верификация".

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

67. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Fyjy (?), 20-Апр-25, 10:17

А что по вашему такое "формальная верификация"? Чистое математическое моделирование.
Первое попавшееся определение: "Формальная верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ."

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

68. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Fyjy (?), 20-Апр-25, 10:31

Из википедии https://ru.wikipedia.org/wiki/%D0%A4%D0%...
формальными методами  называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем.
Ну и первоисточники:
https://shemesh.larc.nasa.gov/fm/fm-what.html
"Formal Methods" refers to mathematically rigorous techniques... The phrase "mathematically rigorous" means that the specifications used in formal methods are well-formed statements in a mathematical logic.

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

69. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Fyjy (?), 20-Апр-25, 10:37

И, кстати, в описании самого  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"

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

27. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (-), 19-Апр-25, 16:50

Они доказали следующее: The Low* source code for each primitive is verified for memory safety, functional correctness, and secret independence. Я не совсем уверен, но всё же думаю, что functional correctness гарантирует, что код считает именно то, что у математиков в статьях написано формулами. А secret independence для меня выглядит чем-то охрененно важным, я правда не могу объяснить почему, потому что не криптограф и очень смутно понимаю о чём речь. Как секрет может быть независим, если он зависит как минимум от того, кто его генерирует?
> чтобы доказать их надёжность надо доказать, что P != NP
_В общем случае_. Чтобы доказать отсутствие data race в общем случае придётся доказывать P != NP, или даже хуже (мне кажется, проблема останова хуже, чем любая NP проблема). Но rust ведь как-то доказывает, так? Как он это делает?
Видимо сейчас я раскрою тебе грязный секрет раста, но фишка в том, что когда rust загнал программиста в клетку shared^mutable, то после этого отсутствие датарейсов легко доказывается. Программисты на C могут загнать себя в эту клетку усилием воли, не дожидаясь когда раст придёт и их туда пинками загонит, и если сишники так сделают, то они тоже про свой код смогут доказывать, что у них нет датарейсов. И про отсутствие use-after-free и double-free они тоже смогут доказывать. Правда им эти доказательства придётся писать руками, но я думаю, что хотя бы отчасти их можно будет автоматизировать. С выходом за границы буфера сложнее, но там и раст читерит, он не доказывает ничего, в рантайм выносит проверки.

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

47. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (47), 19-Апр-25, 18:40

> (мне кажется, проблема останова хуже, чем любая NP проблема).
ну вот это что такое? как можно понятие неразрешимости мешать с понятием сложности? Ну вот на днях была статья под заголовком "The Halting Problem is a terrible example of NP-Harder", что простите? пример нп-сложной? это что за ересь?
//buttondown.com/hillelwayne/archive/the-halting-problem-is-a-terrible-example-of-np/

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

49. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (49), 19-Апр-25, 18:55

> фишка в том, что когда rust загнал программиста в клетку shared^mutable, то после этого отсутствие датарейсов легко доказывается
Этот kremlin (переименнованный согласно повестке в karamel) загоняет более жесткие ограничения чем раст.

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

57. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (-), 20-Апр-25, 01:42

Да, именно благодаря этому они могут доказывать больше.

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

32. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (32), 19-Апр-25, 17:11

А где там сишники? Онм вам уже по ночам снятся? В новости сказано, что библиотека написана на F*.

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

45. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Аноним (45), 19-Апр-25, 18:09

Пока этот Ф не лезет в проекты на сишке с нетерпимой необходимостью засунуть этот Ф прямо в проект мотивируя это тем что он там какой-то супер какой а сишка эта ващще (нахрен тогда припёрлись) - всем сишникам включая меня на этот Ф пофик, пусть компилит там себе в питоне что ему надо

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

78. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Vkni (ok), 20-Апр-25, 19:35

+1
Вообще бесит это вечное «математически доказано» без подробностей. Как будто мы не знаем, что доказывать можно что угодно. Например, что количество символов не превышает полтора миллиарда.
> что реализация соответствует спецификации, которую именно под неё написали ресёрчеры.
Которая просто написана на другом языке программирования, и в которой тоже можно понаделать ошибок.

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

4. "В Python задействованы криптоалгоритмы с математическим дока..." +2 +/–

Сообщение от YetAnotherOnanym (ok), 19-Апр-25, 11:42

Стальная дверь в картонной хижине.

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

9. "В Python задействованы криптоалгоритмы с математическим дока..." +/–

Сообщение от Омнонном (?), 19-Апр-25, 12:02

с тремя стенами

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

22. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (-), 19-Апр-25, 16:02

> Стальная дверь в картонной хижине.
Не понимаю за что ему минус. Этому брейнфаку-2.0 с его pypy и чем там еще и характерными программерами - мало что поможет. Там код обычно пишут - толи скопировав из AI, толи программер сам такое спагетти нагенерил, обработка ошибок и всяких странных действий пользователя? Что вы! Поэтому большей части этих картонных макетов можно CVE навесить одной левой. Но большая их часть даже этого просто не стоит. Много чести для одноразовых картонных шляп с периодом жизни в год.

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

33. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (32), 19-Апр-25, 17:17

Не нервничайте так. Реальные программы на ugly Rust, тем более, все будут писаться с помощью этого самого AI.

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

64. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (-), 20-Апр-25, 09:13

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

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

5. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (5), 19-Апр-25, 11:42

Математическая верификация реализации крипто функций в библиотеке HACL* - это очень круто.
Осталось только верифицировать саму среду исполнения - Python и все будет совсем замечательно.

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

6. "В Python задействованы криптоалгоритмы с математическим дока..." –1 +/–

Сообщение от Аноним (6), 19-Апр-25, 11:49

Зачем? Вон в pyca/cryptography ржавчину запихнули, и вот это уж действительно сбоку припёка. А тут всё в порядке, надёжные алгоритмы должны быть в стандартной библиотеке.

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

14. "В Python задействованы криптофункции с математическим доказа..." –4 +/–

Сообщение от Ivan_83 (ok), 19-Апр-25, 12:56

Фигнёй какой то страдают.
Для начала не понятно как вообще можно было так реализовать (скопипастить референсную реализацию на С) чтобы там накосячить.
Потом вместо использования SIMD SHA они опять что то не то сделали.
В общем питон стремительно копит техдолг и пилит важные либы на фриковских языках, видимо очень хочется работать только в убунте на амд64, примерно как опенврт собирается на полутора линуксах.

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

28. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (26), 19-Апр-25, 16:57

> Фигнёй какой то страдают.
Опять Ivan_83 не понимает, что происходит 😭
> как вообще можно было так реализовать (скопипастить референсную реализацию на С) чтобы там накосячить.
Очень просто: написать на дырявом недоязыке из семидесятых годов.
Да, да, я уже от тебя слышал "у меня такого никогда не происходило". Но, к сожалению, CPython и весь остальной серьезный софт пишут не такие крутые спецы, как Ivan_83.
> В общем питон стремительно копит техдолг
Ты хоть понимаешь, что значит понятие "техдолг"? В новости черным по белому написано, что они от него избавились, ибо в верифицированном коде нет и не никогда будет сишочных сюрпризов.
> пилит важные либы на фриковских языках
Это ты о Сишочке их 70-х с ее выходами за пределы буфера и переполнениями интов? Да, это идеальный, блждад, язык для важных либ.

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

36. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (32), 19-Апр-25, 17:23

OpenWRT, как бы сама по себе, ОС. Или вы имеете ввиду, полностью кросс-собрать его из исходников под обычным GNU/Linux на компе? Так, вдоде, на любом дистре это возможно сделать.

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

82. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 20-Апр-25, 23:18

Да, ага.
Если получится.
У меня ощущение что пилят под убунту или ещё что то попсовое.
На фре/маке собрать можно только помучавшись, как итог мне надоело и я завёл виртуалку с убунтой.

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

59. "В Python задействованы криптофункции с математическим доказа..." –2 +/–

Сообщение от Фрол (?), 20-Апр-25, 04:44

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

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

70. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (-), 20-Апр-25, 11:51

алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало и с минимальным ущербом для окружающих.
>воспоминание о пыхтящей опе из под стола. да, она реально ковыряла там пилочкой для ногтей дыру для кнопки питания. которая кнопка от ласковой женской руки улетела внутрь корпуса и там повисла.
Сравнил себя с женщиной - офисным работником. Ну ты и херой!
>люди вообще делятся на инженеров и на всех остальных
Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины. Жалкое и убогое зрелище представляют из себя инженеры.

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

75. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Фрол (?), 20-Апр-25, 12:57

> алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало
...и не туда, куда надо.
> Сравнил себя с женщиной - офисным работником.
ты откуда такой местечковый мачо вылез? у этой дамы походу диплом с примата был. офисный работник, мой асс.
> Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины.
Кнут с Раскиным передают привет и спрашивают, а они тогда - кто?

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

77. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 20-Апр-25, 14:23

> Кнут с Раскиным передают привет и спрашивают, а они тогда - кто?
кек, с коих пор они инженера?

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

62. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от freehck (ok), 20-Апр-25, 08:44

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

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

83. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 20-Апр-25, 23:21

Да это всё понятно и питон весь такой в белом пальте.
А виноваты какие то фрики которые py-cryptography пилят.
Только по итогу эта либа глубого и много где в завимостях и без неё питон почти бесполезен, как ОС без программ.

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

17. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (47), 19-Апр-25, 15:09

Project Everest - название говорит само за себя, все чем занимаются майки - булшит псевдонаучный, чем им TLA+ не понравился, AWS уже свалил с него как только Лемпорта на пенсию отправили?

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

25. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от zionist (ok), 19-Апр-25, 16:39

> По производительности библиотека HACL* близка к OpenSSL, но в отличие от последней предоставляет дополнительные гарантии надёжности и безопасности.
Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами? Подозрительно!

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

29. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (26), 19-Апр-25, 16:59

> Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами?
Потому что дядя-работодатель на заплатил за это Тео.

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

31. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (-), 19-Апр-25, 17:04

Ничего подозрительного. Математические доказательства кода только сейчас становятся плюс-минус практичными, но всё ещё они большинству недоступны. Лет через дцать, когда будут готовые инструменты, и туториалы на каждом программерском сайте, у Тео не останется выбора. Либо его код будет выглядеть копролитом и никто не будет им пользоваться, либо он будет срочно читать туториалы, и следуя им доказывать свой код.
Хотя с другой стороны, к тому моменту чатботы научатся. Туториалы будут не нужны. Я сейчас-то уже практически их не читаю -- куча воды в каком-то странном авторском порядке... если же начать прессовать чатбота вопросами, и читать про новые для себя слова и понятия умныя статьи, чтобы потом доказывать чатботу что тот несёт бред, это гораздо забавнее, интерактивнее, и главное ты концентрируешься на том, что тебе непонятно, а не на том, что непонятно было автору туториала, когда тот изучал предмет.

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

37. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (32), 19-Апр-25, 17:28

Потому, что INRIA не интересен Тео с его 0.01%-ной ОС? Только его OpenSSL был бы интересен, но, наверное, написанное именно на Сишке математически не верифицировать.

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

92. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 21-Апр-25, 05:32

Забавно слышать.
Чтоб вы понимали это именно OpenBSD является апстримом в мире защитных механизмов.
Из него тащат вся и в венду и в линкус и во фрю и хз куда ещё.
К сожалению libressl умирает - его забросили поддерживать меинтейнеры попсовых дистров.
И я забросил - мне надоело постоянно тратить на это время.

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

30. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (30), 19-Апр-25, 17:03

Направление неплохое, не какое-то раст безобразие. Но мелкософт и инструментарий напрягают.

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

41. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Нуину (?), 19-Апр-25, 18:01

> Но мелкософт и инструментарий напрягают
А то, что Гвидо работает в мс и команда ускорения питона (да, такая есть) из мс тебя не напрягает?

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

42. "В Python задействованы криптофункции с математическим доказа..." +2 +/–

Сообщение от yurikoles (ok), 19-Апр-25, 18:03

>Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами.
Мне кажется это слабое звено. Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C, производный от него.

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

48. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 19-Апр-25, 18:49

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

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

50. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (26), 19-Апр-25, 19:01

> Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C,
Разница в том, что С код в этом случае сгенерирован автоматически, а не написан ручками.

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

53. "В Python задействованы криптофункции с математическим доказа..." +3 +/–

Сообщение от Аноним (32), 19-Апр-25, 19:17

Удивлю вас, но в конечном итоге, выхлоп в машинных кодах. А там нет никаких чекеров боровов.

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

56. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (56), 20-Апр-25, 01:05

В карамел доказывается экивалентность семантики кода на F и С

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

58. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 20-Апр-25, 02:28

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.
перевод с англ. нужен?

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

80. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (56), 20-Апр-25, 21:38

Дальше не осилил прочитать?
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.

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

81. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 20-Апр-25, 23:12

для вас "доказывается экивалентность" равносильно "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.

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

85. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (56), 21-Апр-25, 00:16

Читай внимательно
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.

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

86. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 21-Апр-25, 04:07

Вот вы пишите "В карамел доказывается", в карамель ничего не доказывается (в смысле корректности программы по ее спеке), это делается средствами F*, там только транслируется λow∗ в CompCert Clight, и корректность этой трансляции они (авторы карамель) доказывают, а не сам карамель это делает.
Откройте и на Fig. 1. хоть посмотрите на странице 3.
//arxiv.org/abs/1703.00053
"""
A formal translation from Low∗ to CompCert Clight (§3).
Justifying its dual interpretation as a subset of F∗ and a subset of C, we provide a formal model of Low∗, called λow∗, give a translation from λow∗ to Clight [Blazy and Leroy 2009] and show that it preserves trace equivalence with respect to the original F∗ semantics.
In addition to ensuring that the functional behavior of a program is preserved, our trace equivalence also guarantees that the compiler does not accidentally introduce side-channels due to memory access patterns (as would be the case without the restrictions above) at least until it reaches Clight, a useful sanity check for cryptographic code.
Our theorems cover the translation of standalone λow∗ programs to C, proving that execution in C preserves the original F∗ semantics of the λow∗ program.
"""
Далее из абзаца "Trusted computing base." на странице 4:
"""
Currently, the trusted computing base of our verified libraries includes the implementation of the F∗ typechecker and the Z3 SMT solver [de Moura and Bjørner 2008].
Additionally, we trust the manual proofs of the metatheory relating the semantics of λow∗
to CompCert Clight.
The KreMLin tool is informed by this metatheory, but is currently implemented in unverified OCaml, and is also trusted.
Finally, we inherit the trust assumptions of the C compiler used to compile the code extracted from Low∗.
"""
> We prove that this translation preserves semantics and side-channel resistance.
На странице 17:
"""
Correctness of the λow∗-to-C∗ transformation.
........
In particular, if the source λow∗ program is safe, then so is the target C∗ program. It also follows that the trace equality security property is preserved from λow∗ to C∗ .
We prove this theorem by bisimulation
"""
на странице 36 приложение "D BISIMULATION PROOF"

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

87. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 21-Апр-25, 04:23

//github.com/FStarLang/karamel/blob/master/DESIGN.md
Тут вот по шагам все расписано, что делает конкретно карамель, и я не вижу ни одного "доказывающего" шага.

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

90. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 21-Апр-25, 05:26

Ты смешной.
Тебе не нравится язык который ты не не понимаешь и ты думаешь что какой то магический язык решит все проблемы.
С может транслироватся почти 1в1 к машинному, старые компеляторы в оптимизации не умели и С код легко угадывался по асмовым листингам.
Только вот бывают проблемы и с логикой в коде и с железом, так что если ты решил достичь совершенства (зачем то), то тебе и железо надо особенное какое то, явно не то что у тебя щас, и какие то особенные пейсатели кода, тоже не те что сейчас.
Удачи.

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

43. "В Python задействованы криптофункции с математическим доказа..." –1 +/–

Сообщение от Нуину (?), 19-Апр-25, 18:03

Штош... будет крайне забавно, когда в реализации найдут уязвимость)
зы что-то скорости? Медленнее небось?

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

54. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от нокия (?), 19-Апр-25, 23:23

Это может быть полезно не только в пайтон, конечно:
Low Subset*
Compiles to C/Wasm via KaRaMeL, enabling verified systems code (e.g., HACL*’s cryptographic primitives)
Очень круто!

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

72. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (72), 20-Апр-25, 11:54

Что такое эти математически доказанные функции? Я пытался разобраться, искал, нашел в итоге видео где человек прочитал математическое заклинание похожее на доказательство из геометрии, и всё, код доказан. Это так работает?

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

74. "В Python задействованы криптофункции с математическим доказа..." +1 +/–

Сообщение от Аноним (-), 20-Апр-25, 12:48

Тут одна тонкость. Математическое заклинание должно 100% подходить к задаче. Иначе  волшебство не сработает.

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

76. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (47), 20-Апр-25, 14:16

а где ссылка на видео, чтобы хоть как-то это прокомментировать?

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

79. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (79), 20-Апр-25, 21:36

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

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

84. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (84), 20-Апр-25, 23:33

Не будет. Попытки создать язык с формально доказуемым выводом создавались давно. Coq как средство доказательства теорем, Haskell,... Но так на них и не перешли. Зато развилось нечто под названием Python....

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

88. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 21-Апр-25, 05:19

Ничего не будет.
Даже банальное переписывание требует много времени.
Безопасность - ну такое себе, в текущем виде всё более чем годно и проблемы скорее с потерей контроля над зависимостями, притом у новых языков это прям со старта, а у старых по историческим причинам зависисмости в основном руками поштучно и такой проблемы нет.
Переполнения, выходы за границы и прочее - проще починить чем переделывать.
Но есть конечно некоторые проекты где всё совсем плохо в коде, архитектуре и тп, но это обычно нишевые штуки. Вот такое реально лучше переписать с нуля, но желающих особо нет - оно не попсовое.
А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус.

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

94. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (94), 21-Апр-25, 14:17

>А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус.
Это просто форки, ничего там почти не переписывали

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

95. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 21-Апр-25, 15:36

Да как же!
libressl Тео сильно переписал.
Боринг я не смотрел, вроде его на кресты перевели, да и оно за пределами хрома особо не юзается, кажется это сделали чтобы ГОСТ и прочие стандарты надёжно огородить от браузера.

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

89. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Ivan_83 (ok), 21-Апр-25, 05:22

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

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

96. "В Python задействованы криптофункции с математическим доказа..." +/–

Сообщение от Аноним (96), 21-Апр-25, 21:21

Там в новом пистоне еще t-strings будут: шаблонные строки, также известные как t-strings, были официально приняты в качестве функции в Python 3.14, который выйдет в конце этого года. Более безопасная и гибкая обработка строк и т.д.
https://davepeck.org/2025/04/11/pythons-new-t-strings/

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

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

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

Партнёры:

Хостинг:

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

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

3. "В Python задействованы криптоалгоритмы с математическим дока..."	+16 +/–
Сообщение от Аноним (3), 19-Апр-25, 11:39
Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать их надёжность надо доказать, что P != NP)), а что в реализации сишники за границы буферов не вышли и что реализация соответствует спецификации, которую именно под неё написали ресёрчеры.
Ответить \| Правка \| Наверх \| Cообщить модератору


	11. "В Python задействованы криптоалгоритмы с математическим дока..."	–4 +/–
	Сообщение от Аноним (11), 19-Апр-25, 12:32
	> чтобы доказать их надёжность надо доказать, что P != NP есть квантовые компы, при чём тут надёжность и П != НП?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	16. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (16), 19-Апр-25, 15:09
	https://opennet.ru/61700-nist
	Ответить \| Правка \| Наверх \| Cообщить модератору


	40. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (11), 19-Апр-25, 17:59
	где в новости про PQC? там обычная крипта
	Ответить \| Правка \| Наверх \| Cообщить модератору


	21. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (-), 19-Апр-25, 15:55
	> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов (чтобы доказать > их надёжность надо доказать, что P != NP)), Э, на минуточку, зачем это доказывать для вычислений хешей? Это ж не публичная криптография.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	24. "В Python задействованы криптоалгоритмы с математическим дока..."	+2 +/–
	Сообщение от Аноним (24), 19-Апр-25, 16:15
	Эмм, вообще-то все реальные схемы с публичной криптографией опираются на коллизионную стойкость. Это такое фундаментальное свойство криптографических хеш-функций - стойкость к коллизиям: для заданной функции очень трудно вычислительно подобрать коллизию. Иначе делается такая атака: подбирается коллизия, тебе даётся документ "получите миллион баксов, распишитесь", ты его радостно подписываешь. А второй документ с таким же хешом (благодаря чему твоя подпись из первого документа элементарно перешлёпывается на второй), что "ты подарил всё имущество мошеннику, и подписался на разбор на органы" -- с ним идётся в суд "вот тут товарищ договор подписал, а не исполняет". А если P=NP, то сложных задач в принципе не бывает и все хеши не коллизионно стойкие. А публичная криптография не существует в принципе. Ежели хеши существуют, то как минимум будут подписи Лэмпорта.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	26. "В Python задействованы криптоалгоритмы с математическим дока..."	+3 +/–
	Сообщение от Аноним (26), 19-Апр-25, 16:47
	> Заголовок хайповый. Математически доказана не "надёжность" алгоритмов Заголовок не хайповый - это просто нелепая отсебятина от переводчика. В оригинальных текстах слово "математика" даже близко нигде не упоминается. Это зовется "формальная верификация".
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	67. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Fyjy (?), 20-Апр-25, 10:17
	А что по вашему такое "формальная верификация"? Чистое математическое моделирование. Первое попавшееся определение: "Формальная верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ."
	Ответить \| Правка \| Наверх \| Cообщить модератору


	68. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Fyjy (?), 20-Апр-25, 10:31
	Из википедии https://ru.wikipedia.org/wiki/%D0%A4%D0%... формальными методами называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем. Ну и первоисточники: https://shemesh.larc.nasa.gov/fm/fm-what.html "Formal Methods" refers to mathematically rigorous techniques... The phrase "mathematically rigorous" means that the specifications used in formal methods are well-formed statements in a mathematical logic.
	Ответить \| Правка \| К родителю #26 \| Наверх \| Cообщить модератору


	69. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Fyjy (?), 20-Апр-25, 10:37
	И, кстати, в описании самого 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"
	Ответить \| Правка \| К родителю #26 \| Наверх \| Cообщить модератору


	27. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (-), 19-Апр-25, 16:50
	Они доказали следующее: The Low* source code for each primitive is verified for memory safety, functional correctness, and secret independence. Я не совсем уверен, но всё же думаю, что functional correctness гарантирует, что код считает именно то, что у математиков в статьях написано формулами. А secret independence для меня выглядит чем-то охрененно важным, я правда не могу объяснить почему, потому что не криптограф и очень смутно понимаю о чём речь. Как секрет может быть независим, если он зависит как минимум от того, кто его генерирует? > чтобы доказать их надёжность надо доказать, что P != NP _В общем случае_. Чтобы доказать отсутствие data race в общем случае придётся доказывать P != NP, или даже хуже (мне кажется, проблема останова хуже, чем любая NP проблема). Но rust ведь как-то доказывает, так? Как он это делает? Видимо сейчас я раскрою тебе грязный секрет раста, но фишка в том, что когда rust загнал программиста в клетку shared^mutable, то после этого отсутствие датарейсов легко доказывается. Программисты на C могут загнать себя в эту клетку усилием воли, не дожидаясь когда раст придёт и их туда пинками загонит, и если сишники так сделают, то они тоже про свой код смогут доказывать, что у них нет датарейсов. И про отсутствие use-after-free и double-free они тоже смогут доказывать. Правда им эти доказательства придётся писать руками, но я думаю, что хотя бы отчасти их можно будет автоматизировать. С выходом за границы буфера сложнее, но там и раст читерит, он не доказывает ничего, в рантайм выносит проверки.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	47. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (47), 19-Апр-25, 18:40
	> (мне кажется, проблема останова хуже, чем любая NP проблема). ну вот это что такое? как можно понятие неразрешимости мешать с понятием сложности? Ну вот на днях была статья под заголовком "The Halting Problem is a terrible example of NP-Harder", что простите? пример нп-сложной? это что за ересь? //buttondown.com/hillelwayne/archive/the-halting-problem-is-a-terrible-example-of-np/
	Ответить \| Правка \| Наверх \| Cообщить модератору


	49. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (49), 19-Апр-25, 18:55
	> фишка в том, что когда rust загнал программиста в клетку shared^mutable, то после этого отсутствие датарейсов легко доказывается Этот kremlin (переименнованный согласно повестке в karamel) загоняет более жесткие ограничения чем раст.
	Ответить \| Правка \| К родителю #27 \| Наверх \| Cообщить модератору


	57. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (-), 20-Апр-25, 01:42
	Да, именно благодаря этому они могут доказывать больше.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	32. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (32), 19-Апр-25, 17:11
	А где там сишники? Онм вам уже по ночам снятся? В новости сказано, что библиотека написана на F*.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору


	45. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (45), 19-Апр-25, 18:09
	Пока этот Ф не лезет в проекты на сишке с нетерпимой необходимостью засунуть этот Ф прямо в проект мотивируя это тем что он там какой-то супер какой а сишка эта ващще (нахрен тогда припёрлись) - всем сишникам включая меня на этот Ф пофик, пусть компилит там себе в питоне что ему надо
	Ответить \| Правка \| Наверх \| Cообщить модератору


	78. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Vkni (ok), 20-Апр-25, 19:35
	+1 Вообще бесит это вечное «математически доказано» без подробностей. Как будто мы не знаем, что доказывать можно что угодно. Например, что количество символов не превышает полтора миллиарда. > что реализация соответствует спецификации, которую именно под неё написали ресёрчеры. Которая просто написана на другом языке программирования, и в которой тоже можно понаделать ошибок.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору

4. "В Python задействованы криптоалгоритмы с математическим дока..."	+2 +/–
Сообщение от YetAnotherOnanym (ok), 19-Апр-25, 11:42
Стальная дверь в картонной хижине.
Ответить \| Правка \| Наверх \| Cообщить модератору


	9. "В Python задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Омнонном (?), 19-Апр-25, 12:02
	с тремя стенами
	Ответить \| Правка \| Наверх \| Cообщить модератору


	22. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (-), 19-Апр-25, 16:02
	> Стальная дверь в картонной хижине. Не понимаю за что ему минус. Этому брейнфаку-2.0 с его pypy и чем там еще и характерными программерами - мало что поможет. Там код обычно пишут - толи скопировав из AI, толи программер сам такое спагетти нагенерил, обработка ошибок и всяких странных действий пользователя? Что вы! Поэтому большей части этих картонных макетов можно CVE навесить одной левой. Но большая их часть даже этого просто не стоит. Много чести для одноразовых картонных шляп с периодом жизни в год.
	Ответить \| Правка \| К родителю #4 \| Наверх \| Cообщить модератору


	33. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (32), 19-Апр-25, 17:17
	Не нервничайте так. Реальные программы на ugly Rust, тем более, все будут писаться с помощью этого самого AI.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	64. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (-), 20-Апр-25, 09:13
	Сейчас курсы безопасности есть вроде, можно и понять о чем он. Я кстати согласен.
	Ответить \| Правка \| К родителю #22 \| Наверх \| Cообщить модератору

5. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
Сообщение от Аноним (5), 19-Апр-25, 11:42
Математическая верификация реализации крипто функций в библиотеке HACL* - это очень круто. Осталось только верифицировать саму среду исполнения - Python и все будет совсем замечательно.
Ответить \| Правка \| Наверх \| Cообщить модератору


	6. "В Python задействованы криптоалгоритмы с математическим дока..."	–1 +/–
	Сообщение от Аноним (6), 19-Апр-25, 11:49
	Зачем? Вон в pyca/cryptography ржавчину запихнули, и вот это уж действительно сбоку припёка. А тут всё в порядке, надёжные алгоритмы должны быть в стандартной библиотеке.
	Ответить \| Правка \| Наверх \| Cообщить модератору

14. "В Python задействованы криптофункции с математическим доказа..."	–4 +/–
Сообщение от Ivan_83 (ok), 19-Апр-25, 12:56
Фигнёй какой то страдают. Для начала не понятно как вообще можно было так реализовать (скопипастить референсную реализацию на С) чтобы там накосячить. Потом вместо использования SIMD SHA они опять что то не то сделали. В общем питон стремительно копит техдолг и пилит важные либы на фриковских языках, видимо очень хочется работать только в убунте на амд64, примерно как опенврт собирается на полутора линуксах.
Ответить \| Правка \| Наверх \| Cообщить модератору


	28. "В Python задействованы криптофункции с математическим доказа..."	+/–
	Сообщение от Аноним (26), 19-Апр-25, 16:57
	> Фигнёй какой то страдают. Опять Ivan_83 не понимает, что происходит 😭 > как вообще можно было так реализовать (скопипастить референсную реализацию на С) чтобы там накосячить. Очень просто: написать на дырявом недоязыке из семидесятых годов. Да, да, я уже от тебя слышал "у меня такого никогда не происходило". Но, к сожалению, CPython и весь остальной серьезный софт пишут не такие крутые спецы, как Ivan_83. > В общем питон стремительно копит техдолг Ты хоть понимаешь, что значит понятие "техдолг"? В новости черным по белому написано, что они от него избавились, ибо в верифицированном коде нет и не никогда будет сишочных сюрпризов. > пилит важные либы на фриковских языках Это ты о Сишочке их 70-х с ее выходами за пределы буфера и переполнениями интов? Да, это идеальный, блждад, язык для важных либ.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	36. "В Python задействованы криптофункции с математическим доказа..."	+/–
	Сообщение от Аноним (32), 19-Апр-25, 17:23
	OpenWRT, как бы сама по себе, ОС. Или вы имеете ввиду, полностью кросс-собрать его из исходников под обычным GNU/Linux на компе? Так, вдоде, на любом дистре это возможно сделать.
	Ответить \| Правка \| К родителю #14 \| Наверх \| Cообщить модератору


	82. "В Python задействованы криптофункции с математическим доказа..."	+/–
	Сообщение от Ivan_83 (ok), 20-Апр-25, 23:18
	Да, ага. Если получится. У меня ощущение что пилят под убунту или ещё что то попсовое. На фре/маке собрать можно только помучавшись, как итог мне надоело и я завёл виртуалку с убунтой.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	59. "В Python задействованы криптофункции с математическим доказа..."	–2 +/–
	Сообщение от Фрол (?), 20-Апр-25, 04:44
	> Опять Ivan_83 не понимает, что происходит да ваще! что может хорошего сказать существо с ником иван?! сиди ваня и не высовуйся птушо ты ваня > Но, к сожалению, CPython и весь остальной серьезный софт пишут не такие крутые спецы, как Ivan_83. я тебе больше скажу - люди вообще делятся на инженеров и на всех остальных. так вот инженер - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало и с минимальным ущербом для окружающих. а неинженер вздохнет печально, достанет пилочку для ногтей, и полезет под стол пилить этой пилочкой компуктер. спонсор комментария - воспоминание о пыхтящей опе из под стола. да, она реально ковыряла там пилочкой для ногтей дыру для кнопки питания. которая кнопка от ласковой женской руки улетела внутрь корпуса и там повисла. при чем здесь раст, спросите вы? а да ни при чом, так просто, музыкой навеяло.
	Ответить \| Правка \| К родителю #14 \| Наверх \| Cообщить модератору


	70. "В Python задействованы криптофункции с математическим доказа..."	+/–
	Сообщение от Аноним (-), 20-Апр-25, 11:51
	алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало и с минимальным ущербом для окружающих. >воспоминание о пыхтящей опе из под стола. да, она реально ковыряла там пилочкой для ногтей дыру для кнопки питания. которая кнопка от ласковой женской руки улетела внутрь корпуса и там повисла. Сравнил себя с женщиной - офисным работником. Ну ты и херой! >люди вообще делятся на инженеров и на всех остальных Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины. Жалкое и убогое зрелище представляют из себя инженеры.
	Ответить \| Правка \| Наверх \| Cообщить модератору