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

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

Сообщения

[Сортировка по ответам | RSS]

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

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

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

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

9. Сообщение от Омнонном (?), 19-Апр-25, 12:02	+/–
с тремя стенами
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #4

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

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

16. Сообщение от Аноним (16), 19-Апр-25, 15:09	–1 +/–
https://opennet.ru/61700-nist
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #11 Ответы: #40

17. Сообщение от Аноним (47), 19-Апр-25, 15:09	+1 +/–
Project Everest - название говорит само за себя, все чем занимаются майки - булшит псевдонаучный, чем им TLA+ не понравился, AWS уже свалил с него как только Лемпорта на пенсию отправили?
Ответить | Правка | Наверх | Cообщить модератору

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

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

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

25. Сообщение от zionist (ok), 19-Апр-25, 16:39	+/–
> По производительности библиотека HACL* близка к OpenSSL, но в отличие от последней предоставляет дополнительные гарантии надёжности и безопасности. Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами? Подозрительно!
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #29, #31, #37

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

27. Сообщение от Аноним (-), 19-Апр-25, 16:50	–1 +/–
Они доказали следующее: 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 они тоже смогут доказывать. Правда им эти доказательства придётся писать руками, но я думаю, что хотя бы отчасти их можно будет автоматизировать. С выходом за границы буфера сложнее, но там и раст читерит, он не доказывает ничего, в рантайм выносит проверки.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #3 Ответы: #47, #49

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

29. Сообщение от Аноним (26), 19-Апр-25, 16:59	+1 +/–
> Интересно, почему Тео, до сих пор, не озаботился математическими доказательствами? Потому что дядя-работодатель на заплатил за это Тео.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25

30. Сообщение от Аноним (30), 19-Апр-25, 17:03	+1 +/–
Направление неплохое, не какое-то раст безобразие. Но мелкософт и инструментарий напрягают.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #41

31. Сообщение от Аноним (-), 19-Апр-25, 17:04	+1 +/–
Ничего подозрительного. Математические доказательства кода только сейчас становятся плюс-минус практичными, но всё ещё они большинству недоступны. Лет через дцать, когда будут готовые инструменты, и туториалы на каждом программерском сайте, у Тео не останется выбора. Либо его код будет выглядеть копролитом и никто не будет им пользоваться, либо он будет срочно читать туториалы, и следуя им доказывать свой код. Хотя с другой стороны, к тому моменту чатботы научатся. Туториалы будут не нужны. Я сейчас-то уже практически их не читаю -- куча воды в каком-то странном авторском порядке... если же начать прессовать чатбота вопросами, и читать про новые для себя слова и понятия умныя статьи, чтобы потом доказывать чатботу что тот несёт бред, это гораздо забавнее, интерактивнее, и главное ты концентрируешься на том, что тебе непонятно, а не на том, что непонятно было автору туториала, когда тот изучал предмет.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25

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

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

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

37. Сообщение от Аноним (32), 19-Апр-25, 17:28	+1 +/–
Потому, что INRIA не интересен Тео с его 0.01%-ной ОС? Только его OpenSSL был бы интересен, но, наверное, написанное именно на Сишке математически не верифицировать.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25 Ответы: #92

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

41. Сообщение от Нуину (?), 19-Апр-25, 18:01	+1 +/–
> Но мелкософт и инструментарий напрягают А то, что Гвидо работает в мс и команда ускорения питона (да, такая есть) из мс тебя не напрягает?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #30

42. Сообщение от yurikoles (ok), 19-Апр-25, 18:03	+2 +/–
>Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами. Мне кажется это слабое звено. Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C, производный от него.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #48, #50, #53, #56, #90

43. Сообщение от Нуину (?), 19-Апр-25, 18:03	–1 +/–
Штош... будет крайне забавно, когда в реализации найдут уязвимость) зы что-то скорости? Медленнее небось?
Ответить | Правка | Наверх | Cообщить модератору

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

47. Сообщение от Аноним (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ообщить модератору
Родитель: #27

48. Сообщение от Аноним (47), 19-Апр-25, 18:49	+/–
> если реально всё равно используется выхлоп на C тут по идеи выхлоп то примитивный, с минимальными конструкциями языка которые не гарантируют корректность, то есть всякого рода жонглирование указателями не используется и т.д. как по мне, все это ересь, на основе спецификации должен генерироваться прямой конкретный машинный код, а не программы на других формальных языках.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #42

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

50. Сообщение от Аноним (26), 19-Апр-25, 19:01	+/–
> Непонятно какая разница на сколько надёжен оригинальный код, если реально всё равно используется выхлоп на C, Разница в том, что С код в этом случае сгенерирован автоматически, а не написан ручками.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #42

53. Сообщение от Аноним (32), 19-Апр-25, 19:17	+3 +/–
Удивлю вас, но в конечном итоге, выхлоп в машинных кодах. А там нет никаких чекеров боровов.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #42

54. Сообщение от нокия (?), 19-Апр-25, 23:23	+/–
Это может быть полезно не только в пайтон, конечно: Low Subset* Compiles to C/Wasm via KaRaMeL, enabling verified systems code (e.g., HACL*’s cryptographic primitives) Очень круто!
Ответить | Правка | Наверх | Cообщить модератору

56. Сообщение от Аноним (56), 20-Апр-25, 01:05	+/–
В карамел доказывается экивалентность семантики кода на F и С
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #42 Ответы: #58

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

58. Сообщение от Аноним (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ообщить модератору
Родитель: #56 Ответы: #80

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

62. Сообщение от freehck (ok), 20-Апр-25, 08:44	+/–
> питон <...> пилит важные либы на фриковских языках Не-не-не, они не пилят. Эти либы написаны другими людьми, куда более профессиональными. ) > питон стремительно копит техдолг Ну, если подходить формально, то это -- часть их техдолга. Но питон пилится прикладниками, и следовательно алгоритм приоритезации разработки простой: нашёлся кто-то, кому именно это было нужно, он оплатил и пропихнул задачу вперёд. И только. А фигня она в глобальном плане или не фигня -- вопрос десятый.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #14 Ответы: #83

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

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

68. Сообщение от 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.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #26

69. Сообщение от 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"
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #26

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

72. Сообщение от Аноним (72), 20-Апр-25, 11:54	+1 +/–
Что такое эти математически доказанные функции? Я пытался разобраться, искал, нашел в итоге видео где человек прочитал математическое заклинание похожее на доказательство из геометрии, и всё, код доказан. Это так работает?
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #74, #76

74. Сообщение от Аноним (-), 20-Апр-25, 12:48	+1 +/–
Тут одна тонкость. Математическое заклинание должно 100% подходить к задаче. Иначе  волшебство не сработает.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #72

75. Сообщение от Фрол (?), 20-Апр-25, 12:57	+/–
> алкаш слесарь из ЖЭКа - в любом случае гвоздь забьет, а шуруп вкрутит. используя что угодно, что под руку попало ...и не туда, куда надо. > Сравнил себя с женщиной - офисным работником. ты откуда такой местечковый мачо вылез? у этой дамы походу диплом с примата был. офисный работник, мой асс. > Инженер не может сочинять музыку, не способен писать книги и пьесы, не может писать картины. Кнут с Раскиным передают привет и спрашивают, а они тогда - кто?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #70 Ответы: #77

76. Сообщение от Аноним (47), 20-Апр-25, 14:16	+/–
а где ссылка на видео, чтобы хоть как-то это прокомментировать?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #72

77. Сообщение от Аноним (47), 20-Апр-25, 14:23	+/–
> Кнут с Раскиным передают привет и спрашивают, а они тогда - кто? кек, с коих пор они инженера?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #75

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

79. Сообщение от Аноним (79), 20-Апр-25, 21:36	+/–
Между строк читается, что весь накопленный за десятки лет багаж открытого кода будет на перспективе ближайших лет полностью выброшен на помойку из-за того, что нет возможности надежно оценить его безопасность. OpenSSL ни разу не жалко, но эта же логика будет в конце концов применяться к любому коду. Новый NIH синдром.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #84, #88, #89

80. Сообщение от Аноним (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ообщить модератору
Родитель: #58 Ответы: #81

81. Сообщение от Аноним (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ообщить модератору
Родитель: #80 Ответы: #85

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

83. Сообщение от Ivan_83 (ok), 20-Апр-25, 23:21	+/–
Да это всё понятно и питон весь такой в белом пальте. А виноваты какие то фрики которые py-cryptography пилят. Только по итогу эта либа глубого и много где в завимостях и без неё питон почти бесполезен, как ОС без программ.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #62

84. Сообщение от Аноним (84), 20-Апр-25, 23:33	+/–
Не будет. Попытки создать язык с формально доказуемым выводом создавались давно. Coq как средство доказательства теорем, Haskell,... Но так на них и не перешли. Зато развилось нечто под названием Python....
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #79

85. Сообщение от Аноним (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ообщить модератору
Родитель: #81 Ответы: #86, #87

86. Сообщение от Аноним (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ообщить модератору
Родитель: #85

87. Сообщение от Аноним (47), 21-Апр-25, 04:23	+/–
//github.com/FStarLang/karamel/blob/master/DESIGN.md Тут вот по шагам все расписано, что делает конкретно карамель, и я не вижу ни одного "доказывающего" шага.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #85

88. Сообщение от Ivan_83 (ok), 21-Апр-25, 05:19	+/–
Ничего не будет. Даже банальное переписывание требует много времени. Безопасность - ну такое себе, в текущем виде всё более чем годно и проблемы скорее с потерей контроля над зависимостями, притом у новых языков это прям со старта, а у старых по историческим причинам зависисмости в основном руками поштучно и такой проблемы нет. Переполнения, выходы за границы и прочее - проще починить чем переделывать. Но есть конечно некоторые проекты где всё совсем плохо в коде, архитектуре и тп, но это обычно нишевые штуки. Вот такое реально лучше переписать с нуля, но желающих особо нет - оно не попсовое. А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #79 Ответы: #94

89. Сообщение от Ivan_83 (ok), 21-Апр-25, 05:22	+/–
Даже больше скажу, вот прям за деньги: процесс длительный, тяжёлый и сплошные затраты без профита. Всех желающих просто пошлют в лес, если опять не удастся напилить грантов за счёт каких нибудь налогоплательщиков. И даже когда начнут и может даже что то перепишут - старй код никуда не денется, всякие девайсы с ним будут ещё десятки лет жить. И отдельные старые системы тоже десятилетия будут использоватся, как кобол вон до сих пор в проде.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #79

90. Сообщение от Ivan_83 (ok), 21-Апр-25, 05:26	+/–
Ты смешной. Тебе не нравится язык который ты не не понимаешь и ты думаешь что какой то магический язык решит все проблемы. С может транслироватся почти 1в1 к машинному, старые компеляторы в оптимизации не умели и С код легко угадывался по асмовым листингам. Только вот бывают проблемы и с логикой в коде и с железом, так что если ты решил достичь совершенства (зачем то), то тебе и железо надо особенное какое то, явно не то что у тебя щас, и какие то особенные пейсатели кода, тоже не те что сейчас. Удачи.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #42

92. Сообщение от Ivan_83 (ok), 21-Апр-25, 05:32	+/–
Забавно слышать. Чтоб вы понимали это именно OpenBSD является апстримом в мире защитных механизмов. Из него тащат вся и в венду и в линкус и во фрю и хз куда ещё. К сожалению libressl умирает - его забросили поддерживать меинтейнеры попсовых дистров. И я забросил - мне надоело постоянно тратить на это время.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #37

94. Сообщение от Аноним (94), 21-Апр-25, 14:17	+/–
>А тот же опенссл уже и так переписали раза 3: либрессл, борингссл и ещё чего то там, на любой вкус. Это просто форки, ничего там почти не переписывали
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #88 Ответы: #95

95. Сообщение от Ivan_83 (ok), 21-Апр-25, 15:36	+/–
Да как же! libressl Тео сильно переписал. Боринг я не смотрел, вроде его на кресты перевели, да и оно за пределами хрома особо не юзается, кажется это сделали чтобы ГОСТ и прочие стандарты надёжно огородить от браузера.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #94

96. Сообщение от Аноним (96), 21-Апр-25, 21:21	+/–
Там в новом пистоне еще t-strings будут: шаблонные строки, также известные как t-strings, были официально приняты в качестве функции в Python 3.14, который выйдет в конце этого года. Более безопасная и гибкая обработка строк и т.д. https://davepeck.org/2025/04/11/pythons-new-t-strings/
Ответить | Правка | Наверх | Cообщить модератору

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

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