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

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

Сообщения

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

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

	11. "В Python задействованы криптоалгоритмы с математическим дока..."	–5 +/–
	Сообщение от Аноним (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 задействованы криптоалгоритмы с математическим дока..."	+1 +/–
	Сообщение от Аноним (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 задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (-), 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 задействованы криптоалгоритмы с математическим дока..."	+/–
	Сообщение от Аноним (-), 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. Скрыто модератором	+/–
	Сообщение от Аноним (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ообщить модератору

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

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

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

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