The OpenNET Project / Index page

[ новости /+++ | форум | wiki | теги | ]

Новая криптографическая библиотека EverCrypt с математическим доказательством надёжности

06.04.2019 12:18

Исследователи из французского государственного института исследований в информатике и автоматике (INRIA), подразделения Microsoft Research и университета Карнеги — Меллона представили первый тестовый выпуск криптографической библиотеки EverCrypt, развиваемой в рамках проекта Everest и применяющей математические методы формальной верификации надёжности. По своим возможностям и производительности EverCrypt очень близка к существующим криптографическим библиотекам (OpenSSL), но в отличие от них предоставляет дополнительные гарантии надёжности и безопасности.

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

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

Код проекта написан на функциональном языке F*, предоставляющем систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) для программ и гарантировать корректность и отсутствие ошибок в реализации при помощи SMT-формул и вспомогательных инструментов доказательства. На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly. Код на языке F* распространяется под лицензией Apache 2.0, а итоговые модули на Си и ассемблере под лицензией MIT. Некоторые части подготовленного проектом кода уже используются в Firefox, ядре Windows, блокчейне Tezos и VPN Wireguard.

Отмечается, что верификация позволяет избавиться от многих ошибок, но не исключает всех проблем:

  • Используемый при разработке инструментарий остаётся неверифицированным, в том числе возможно существование ошибок в F*, KreMLin (верифицирующий транслятор из языка F* в Си) и в компиляторах для сборки кода на Си (если не использовать верифицированный CompCert).
  • Очень трудно правильно и точно воспроизвести спецификации. Например, где-то можно допустить опечатку, а где-то упустить вопрос преобразования порядка следования байтов. Поэтому до того как приступать к созданию оптимизированных версий реализации, проводится доскональный аудит и тестирование спецификаций;
  • Применяемые модели верификации не учитывают такие угрозы, как атаки Spectre и Meltdown, а также не защищают от новых классов ещё не известных атак, которые могут появиться в будущем;

По сути EverCrypt объединяет два ранее разрозненных проекта HACL* и Vale, предоставляя на их основе унифицированный API и делая их пригодными для применения в реальных проектах. HACL* написан на языке Low* и нацелен на предоставление криптопримитивов для использования в программах на языке Си с использованием API в стиле libsodium и NaCL. Проект Vale развивал предметно-ориентированный язык для создания верифицированных криптографических примитивов на ассемблере. Около 110 тысяч строк кода проекта HACL* на языке Low* и 25 тысяч строк кода на Vale объединены и переписаны в примерно 70 тысяч строк кода на универсальном языке F*, который также развивается в рамках проекта Everest. На базе созданных верифицированных примитивов проектом Everest дополнительно развивается стек miTLS с верифицированной реализацией TLSv1.3.

В первом выпуске библиотеки EverCrypt представлены верифицированные реализации следующих криптографических алгоритмов, которые предложены в вариантах на Си или ассемблере (при использовании библиотеки автоматически выбирается оптимальная для текущей платформы реализация):

  • Алгоритмы хэшировния: все варианты SHA2, SHA3, SHA1 и MD5;
  • Коды проверки подлинности: HMAC поверх SHA1, SHA2-256, SHA2-384 и SHA2-512 для аутентификации источника данных;
  • Алгоритм формирования ключей HKDF (HMAC-based Extract-and-Expand Key Derivation Function);
  • Потоковый шифр ChaCha20 (доступна неоптимизированная версия на Си)
  • Алгоритм аутентификации сообщений (MAC) Poly1305 (версии на Си и ассемблере),
  • Протокол Диффи-Хеллмана на эллиптических кривых Curve25519 (версии на Си и ассемблере с оптимизациями на базе инструкций BMI2 и ADX);
  • AEAD режим блочного шифрования (аутентифицированное шифрование) ChachaPoly (неоптимизированная версия на Си);
  • AEAD режим блочного шифрования AES-GCM (версия на ассемблере с оптимизациями AES-NI).

В первом альфа-выпуске уже в основной массе завершена верификация кода, но ещё остаются некоторые неохваченные области. Пока не верифицированы и не включены в поставку оптимизированные при помощи инструкций SHA-EXT и AVX варианты SHA2-256 и Poly130. Обещанный уровень производительности в текущий момент обеспечен только для алгоритма Curve25519.

Также ещё не стабилизирован API, который будет расширяться в следующих альфа-версиях (планируется унифицировать структуры для всех API по примеру наиболее зрелого EverCrypt_Hash.h и унифицировать коды ошибок в EverCrypt.Error). Из недоработок также отмечается поддержка только архитектуры x86_64 (на первом этапе главной целью является надёжность, а оптимизации и платформы будут реализованы во вторую очередь).

  1. Главная ссылка к новости (https://news.ycombinator.com/i...)
  2. OpenNews: Открыт код сверхнадёжного микроядра seL4
  3. OpenNews: Агентство DARPA экспериментирует с созданием игр для верификации надёжности открытого ПО
  4. OpenNews: Fabric - новый язык программирования для безопасных распределенных вычислений
  5. OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
  6. OpenNews: Google представил криптографическую библиотеку Tink
Лицензия: CC-BY
Наводку на новость прислал Artem S. Tashkinov
Тип: Интересно / Программы
Ключевые слова: evercrypt, crypt, verify
При перепечатке указание ссылки на opennet.ru обязательно
Обсуждение (105) Ajax | 1 уровень | Линейный | Раскрыть всё | RSS
  • 1.1, Аноним (1), 12:22, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    Интересно, как математически доказать потокобезопасность.
     
     
  • 2.2, адмирал третьего флота очевидно (?), 12:42, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    пока никак. увы.
     
  • 2.23, Sw00p aka Jerom (?), 17:27, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +8 +/
    Дайте сначала определение "потокобезопасность"-и
     
  • 2.47, Аноним (47), 21:55, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +6 +/
    Многопоточные алгоритмы невозможно описать математически?
     

  • 1.3, nc (ok), 12:48, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    Какой еще Kremlin?
     
     
  • 2.5, Анонимный селебрити (?), 12:54, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +5 +/
    Там только его рука :)
     
     
  • 3.27, Аноним (27), 18:34, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Т. майор приложил свою лапу к созданию транслятора.
     

  • 1.4, Анонимный селебрити (?), 12:53, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +7 +/
    Дейкстра одобряет
     
  • 1.6, АНБ (?), 13:10, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    > В первом альфа-выпуске уже в основной массе завершена верификация кода, но ещё
    > остаются некоторые не охваченные области. Пока не верифицированы и не включены
    > в поставку оптимизированные при помощи инструкций SHA-EXT  и AVX варианты
    > SHA2-256 и Poly130.   Обещанный уровень производительности в текущий момент
    > обеспечен только для алгоритма Curve25519. Также ещё не стабилизирован API, который
    > будет расширяться в следующих альфа-версиях (планируется унифицировать структуры для
    > всех API по примеру наиболее зрелого EverCrypt_Hash.h и унифицировать коды ошибок
    > в EverCrypt.Error). Из недоработок также отмечается поддержка только архитектуры x86_64
    > (на первом этапе главной целью является надёжность, а оптимизации и платформы
    > будут реализованы во вторую очередь).

    На фоне быстрого и проверенного годами OpenSSL выглядит бледно.
    К тому же, яйцеголовые теоретики сами пишут, что верификация не защищает на самом деле ни от чего, просто делет код медленее, как и проверки времени выполнения.
    В общем, вердикт - чисто академическая поделка и не стоит внимания. Лучше оставаться на старом, добром и вполне надежном (если руки не из джопы) OpenSSL!

     
     
  • 2.7, Аноним (7), 13:26, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > чисто академическая поделка

    Да, во многом так. Не первая причем. Такое хорошо для верификации практически неизменных вещей, стандартов. Возможно криптобиблиотек.

    Но обычное ПО не особо подходит - долго, дорого, а за это время выходит новая версия.

     
  • 2.9, пох (?), 13:37, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +9 +/
    > На фоне быстрого и проверенного годами OpenSSL

    лол.

     
     
  • 3.34, myhand (ok), 19:12, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +2 +/
    АНБ проверило.  А ты хто такой?
     
     
  • 4.41, пох (?), 20:52, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    у ентого вашего "АНБ" чекистский значок, кажись, на лацкане...

     
     
  • 5.48, myhand (ok), 22:21, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    А вы каких фашистов выбираете?
     
  • 2.18, Аноним (18), 15:13, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Libressl лучше
     
     
  • 3.73, dabdabya (?), 15:27, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Кто-то минус влепил,но он действительно лучше. Libressl не требует perl для сборки и при сборке с -O3 быстрее того же openssl,который тоже собран с -O3
     
  • 3.123, Аноним (123), 12:39, 12/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Только BoringSSL, только хардкор!
     
  • 2.35, ФАПСИ (?), 19:16, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Абсолютно с вами согласен, коллега!
     

  • 1.11, X4asd (ok), 14:06, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > Код на языке F* распространяется под лицензией Apache 2.0, а итоговые модули на Си и ассемблере под лицензией MIT

    как это понять?

    исходный код на Apache2, но его скомпилированный вариант уже на MIT? а исходный код скомпилированного варианта тогда под какой лицензией -- MIT или Apache2?

     
     
  • 2.14, пох (?), 14:25, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > как это понять?

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

    > а исходный код скомпилированного варианта тогда под какой лицензией

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

     
     
  • 3.21, Аноним (21), 15:42, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > за скомпилированный они меньше переживают

    Читаем внимательно

    > На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly.

    О скопмилированном коде тут речь не идет. Поэтому не путайте. Скомпилированный исходный код под той же лицензией, что и сам исходный код.

     
     
  • 4.26, пох (?), 17:52, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > О скопмилированном коде тут речь не идет.

    о, очередной "программист" самоучка? Компилятор с F на C - вполне себе компилятор, и код этот - компилированный. Что тебе бы рассказали на первом курсе института, если бы ты его посещал.

    И именно о нем речь и идет.
    (Забавно, кстати, что разглядывавшие этот код люди нашли его более читаемым чем код аналогичного свойства, написанный человеками.)

    так вот с кодом, который скомпилировали разработчики - можешь делать что угодно. С кодом, который ты накомпилируешь сам из F* - только в рамках apache license.

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

     
     
  • 5.30, Аноним (27), 18:53, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >С кодом, который ты накомпилируешь сам из F* - только в рамках apache license.

    https://ru.wikipedia.org/wiki/Лицензия_Apache
    "Согласно Free Software Foundation, GPLv3 совместима с Apache License v2.0. Как следствие, разработчики всегда имеют возможность свои программы под Apache License v2.0 перевести под GPL v3.0, чтобы быть уверенными в том, что производные их разработок (форки) останутся свободными."
    Так что можешь хоть под GPL прелицензировать, то, что сам странслировал с F*.

     
     
  • 6.51, пох (?), 23:17, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Так что можешь хоть под GPL прелицензировать, то, что сам странслировал с
    > F*.

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

    А разработчики могут перевести хоть под коммерческую лицензию, как уже не раз случалось. Или, вот, вовсе под MIT. Поскольку, внезапно, их может совершенно не беспокоить "останутся ли свободными" форки их проекта.

     
  • 5.31, Sw00p aka Jerom (?), 18:58, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    речь идет именно о сгенерированном Си коде, никакой компиляции

    https://github.com/project-everest/hacl-star/tree/master/snapshots

    и собственно о лицензиях

    Licenses

    All F* source code is released under Apache 2.0.
    All generated C, OCaml, Javascript and Web Assembly code is released under MIT.


    внимание на "All generated"

     
     
  • 6.40, Аноним (40), 20:33, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > речь идет именно о сгенерированном Си коде, никакой компиляции

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

     
     
  • 7.45, Sw00p aka Jerom (?), 21:12, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –3 +/
    >с потерей человекочитаемости называется компиляцией

    )))) пройдите по ссылке указанной выше, и вовсе не компиляция, а трансляция (кодогенерация)

    пс: цитата из вики, для особо одаренных

    "Компили́ровать — проводить трансляцию машинной программы с предметно-ориентированного языка на машинно-ориентированный язык"

    и с коих пор Си - машинно-ориентированный?

     
     
  • 8.49, пох (?), 22:50, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    вашу викивракию пишут такие же эксперты как и вы - не посещавшие даже лекции д... текст свёрнут, показать
     
     
  • 9.57, Sw00p aka Jerom (?), 00:35, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    ок, понятно, а теперь ответьте на один вопрос - кто автор теории компиляторов ... текст свёрнут, показать
     
  • 9.58, Sw00p aka Jerom (?), 00:37, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    про первокурсников, а вы собственно из серии программистов которым не нужна мат... текст свёрнут, показать
     
  • 9.68, t_ (?), 12:53, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Самое забавное, что он прав и в вики это тоже верно написано Перечитайте что ли... текст свёрнут, показать
     
     
  • 10.75, Аноним84701 (ok), 16:46, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Девочки, не ссорьтесь Cуществует и то и это Остроконечники W различающие п... текст свёрнут, показать
     
     
  • 11.81, Sw00p aka Jerom (?), 18:58, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Да, но именно результат компиляции это типа последняя фаза трансляций может ... текст свёрнут, показать
     
     
  • 12.83, Аноним84701 (ok), 19:41, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Может, а может и нет Я просто подсказываю, что зависит от используемой вполне ... текст свёрнут, показать
     
     
  • 13.86, Sw00p aka Jerom (?), 20:25, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    нет не стоит, и он от ЯП других ничем не отличается, ибо он из мнемонического ко... текст свёрнут, показать
     
     
  • 14.87, Аноним84701 (ok), 20:51, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    То что не отличается, я даже не спорил, а вот то что все же стоИт, пусть в основ... текст свёрнут, показать
     
     
  • 15.88, Sw00p aka Jerom (?), 21:28, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Так результат работы того же gcc с опцией -c Compile or assemble на выходе даё... текст свёрнут, показать
     
  • 12.94, Аноним (94), 11:57, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Ассемблер совершает процесс ассемблирования Это когда каждая мнемоника тран... текст свёрнут, показать
     
     
  • 13.105, Sw00p aka Jerom (?), 16:52, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    это не компиляция - а перевод трансляция, кодогенерация в другой язык, назыв... текст свёрнут, показать
     
     
  • 14.116, Аноним (94), 07:59, 09/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Это была цитата в переводе Ren 233 Tournois Betov , автора SpAsm и RosAsm... текст свёрнут, показать
     
  • 11.99, t_ (?), 13:59, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Ты молодец Открыл нужную книгу, выделил слово translate, но вывод сделал неверн... текст свёрнут, показать
     
     
  • 12.109, Аноним84701 (ok), 21:56, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Еще раз - translator в _этом_ варианте англоязычной терминологии вообще как-т... текст свёрнут, показать
     
     
  • 13.114, t_ (?), 01:21, 09/04/2019 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Всё правильно написано, поскольку ни компилятор, ни интерпретатор, ни сборщик не... текст свёрнут, показать
     
     
  • 14.117, Sw00p aka Jerom (?), 18:41, 09/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    если результирующую понимать как конечный этап машинные коды операций , то да... текст свёрнут, показать
     
     
  • 15.118, t_ (?), 02:38, 10/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Изначально верный ответ дал Аноним84701 D В про... текст свёрнут, показать
     
     
  • 16.119, Sw00p aka Jerom (?), 15:03, 10/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Если приводить цитаты из вики, то повторюсь https en wikipedia org wiki Sourc... текст свёрнут, показать
     
     
  • 17.120, t_ (?), 23:40, 10/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Я тоже повторно объясню компиляция не требует обязательного результата в виде м... текст свёрнут, показать
     
     
  • 18.121, Sw00p aka Jerom (?), 01:17, 11/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    где на странице в вике о компиляторе это написано там строго утверждено - резул... текст свёрнут, показать
     
  • 8.60, Аноним (60), 07:06, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Вообще-то Вики сама суть результат компиляции com-pile дословно в одну кучу ... текст свёрнут, показать
     
  • 8.79, Аноним84701 (ok), 17:35, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Выше по ссылке https github com project-everest hacl-star Еще используется ex... текст свёрнут, показать
     
  • 7.50, пох (?), 23:07, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    вы только в википедию этот бред теперь не пишите вместо того, который там уже, п... текст свёрнут, показать
     
     
  • 8.66, myhand (ok), 11:11, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Почему-ж В помойку надо складать мусор, она для того и предназначена ... текст свёрнут, показать
     
  • 8.101, meantraitor (?), 15:59, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Вы сравниваете ежа с ужом По ссылке, которую вы привели, описана текстовая сери... текст свёрнут, показать
     
     
  • 9.111, пох (?), 23:10, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    вы, похоже, не владеете темой Вся суть проекта llvm - что вот это вот внутренн... текст свёрнут, показать
     
     
  • 10.124, meantraitor (?), 13:00, 12/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Да-да, уже 15 лет не владею Все современные компиляторы так устроены уже давн... текст свёрнут, показать
     
  • 6.42, пох (?), 20:54, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    перепись безграмотных "программистов" на опеннете...
     
     
  • 7.46, Sw00p aka Jerom (?), 21:13, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –2 +/
    отмазки одни, давай по делу
     
     
  • 8.102, meantraitor (?), 16:03, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Тут он все правильно сказал Я сначала смеялся, потом плакал, под конец уже кров... текст свёрнут, показать
     
     
  • 9.107, Sw00p aka Jerom (?), 20:16, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    чаво он там правильного сказал У него трансляция с одного исходного языка на др... текст свёрнут, показать
     
  • 5.100, meantraitor (?), 15:42, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > о, очередной "программист" самоучка? Компилятор с F на C - вполне себе компилятор, и код этот -
    > компилированный. Что тебе бы рассказали на первом курсе института, если бы ты его посещал.

    Вы бы, это, поаккуратнее с подобными безаппеляционными высказаваниями.
    Ни разу это не компилятор, а (source-to-source) транслятор

     
     
  • 6.115, t_ (?), 01:42, 09/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Он тоже прав. :)
    Просто он имеет в виду компилятор, внутри которого работает source-to-source транслятор.
    Например, так:

    pkg search vala
    vala-0.40.11,1                 Programming language and compiler that converts Vala code into C code

    Иными словами, процессы компиляции и трансляции различаются. Но все они работают внутри компилятора (интерпретатора).

     
  • 2.19, KonstantinB (ok), 15:22, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Полагаю, так сделано потому, что Apache 2.0 требует явного указания на то, какие файлы модифицированы - чтобы понимать, были ли внесены изменены в формальные спецификации доказательства.

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

     
     
  • 3.37, X4asd (ok), 19:38, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Полагаю, так сделано потому, что Apache 2.0 требует явного указания на то, какие файлы модифицированы - чтобы понимать, были ли внесены изменены в формальные спецификации доказательства.

    а кому пришло бы в глову модифицировать НЕ исходный код а получившийся скомпилированный вариант?

    я думал такое желание было только у васянов которые делали ZverDVD

     
     
  • 4.43, пох (?), 20:58, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > а кому пришло бы в глову модифицировать НЕ исходный код

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

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

     
     
  • 5.55, KonstantinB (ok), 00:18, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Что там у wireguard не смотрел, в виду его феерической ненужности

    Как говорили в одной древней любительской сети, "отучаемся говорить за всех".

    > наверняка меняли

    Менял сам автор так, как его попросили.

    > до верифицированной целиком замены openssl) - покамест как до китая раком

    Ясен пень. Openssl пишется уже 20 с гаком лет. Но инициативу поддерживаю.

     
  • 5.93, X4asd (ok), 11:33, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >> а кому пришло бы в глову модифицировать НЕ исходный код
    > Не всегда получается чужой исходник вот так, не модифицируя, встроить в свою сложную (и мутную) библиотеку.

    зачем ты мне привёл пример про изменение ИСХОДНОГО кода?

    я же говорил про изменение НЕисходного кода

     
     
  • 6.110, пох (?), 22:42, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > я же говорил про изменение НЕисходного кода

    код, который меняет мазила - сгенерен из кода на F* (который сам по себе мало кому вообще зачем-то сдался), вероятно, это то что ты называешь "неисходным".

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

     
  • 4.56, KonstantinB (ok), 00:20, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > а кому пришло бы в глову модифицировать НЕ исходный код а получившийся скомпилированный вариант?

    В общем-то по MIT это делать как раз можно (беря их скомпилированные варианты).
    Суть такого лицензирования в том, чтобы заявить:
    1) берите скомпиенное у нас, у нас все формально верифицировано, а у Васяна там хрен знает что,
    2) если уж беретесь править доказательства, то четко указывайте, где что поменяли, чтобы мы могли проверить корректность.

     
     
  • 5.92, X4asd (ok), 11:30, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >> а кому пришло бы в глову модифицировать НЕ исходный код а получившийся скомпилированный вариант?
    > В общем-то по MIT это делать как раз можно (беря их скомпилированные
    > варианты).
    > Суть такого лицензирования в том, чтобы заявить:
    > 1) берите скомпиенное у нас, у нас все формально верифицировано, а у
    > Васяна там хрен знает что,
    > 2) если уж беретесь править доказательства, то четко указывайте, где что поменяли,
    > чтобы мы могли проверить корректность.

    речь не о "можно ли?" а о "зачем такое делать?".

     

  • 1.15, кругомвраги (?), 14:46, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • –3 +/
    >Процесс верификации сводится к определению подробных спецификаций...

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

     
     
  • 2.32, Sw00p aka Jerom (?), 19:03, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    в смысле неразглашаемая?
     
     
  • 3.61, Аноним (60), 07:21, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > в смысле неразглашаемая?

    У "Кругомвраги" известный из истории смысл

    Einkreisung - Идеология, овладевшая умами немцев в самом конце XIX века - после формирования блока Антанты. В более сильном варианте стала проповедоваться после окончания ПМВ в стиле мы самые сильные и лучшие, и поэтому весь мир только и думает, как бы нам нагадить.

    https://de.wikipedia.org/wiki/Einkreisung

     
  • 3.125, кругомвраги (?), 21:04, 12/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    библиотека это по сути чёрный ящик причем для всех и даже авторов т к для знани... текст свёрнут, показать
     
     
  • 4.126, Sw00p aka Jerom (?), 01:33, 13/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > нам предлагается набор спецификаций которым должен соответствовать ящик

    доверяй, но проверяй

    Если, нам предлагают, это не значить, что нас защищают

    пс: вы в курсе, что есть такое К который меньше Д в степени Е по модулю Н есть текст, который зашифрован в стемени Е по модулю Н?

     

  • 1.16, . (?), 15:05, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти

    Все эти ошибки возникают при динамической работе с памятью или при зависимости логики от внешних данных. Крипту ничто не мешает писать на массивах, выходы за границы которых отлавливаются статическим анализатором. Тогда, если тесты успешны программа иначе себя вести не может.
    Пример:
    void encrypt(uint64_t block[4], uint64_t rk[120]);

    С другой стороны в библиотеках обычно дают на выбор несколько алгоритмов, каждый из который имеет варианты реализации в зависимости платформы (endianness, разрядность, аппаратное ускорение, особенности ОС). Поэтому подход с формальной верификацией имеет смысл, но это компромисс который обычного пользователя в общем-то не касается.

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

     
     
  • 2.17, Аноним (17), 15:11, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Напишите на массивах хотя бы парсер сертификатов X.509, а мы посмотрим.
     
     
  • 3.20, . (?), 15:36, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    В сабжевой библиотеке этого тоже нет. Сам я со структурой сертификатов не разбирался, но ясно, что парсинг нужен только если она не статическая. В таких случаях используют дерево и следовательно работу с памятью, а парсить на массивах извращение.
     
  • 2.38, Ivan_83 (ok), 19:42, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    1. При такой передаче много лишнего копирования памяти.

    2. Тут не предусмотрен возврат данных.

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

     
     
  • 3.53, . (?), 23:46, 06/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Поскольку другой поточный шифр RC4, которые уже везде обьявили дырявым, то кроме чачи/сальсы ничего и нет.

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

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

    Одномерный массив в си всегда передается как указатель:
    void encrypt(uint64_t block[4], const uint64_t rk[120]);
    void encrypt(uint64_t *block, const uint64_t *rk);
    Для компилятора нет разницы. Поэтому, чтобы гарантированно не облажаться с выходом за границы понадобится еще статический анализатор.

    Нужна ли формальная верификация библиотекам для массового использования? Да.
    Нужна ли она в принципе для написания крипты? Нет, так как криптография в софте легко разбивается на функции, изменяющие массив (или структуру) фиксированного размера.
    Вот что я пытался сформулировать.

     
     
  • 4.59, Sw00p aka Jerom (?), 02:32, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >Нет, так как криптография в софте легко разбивается на функции, изменяющие массив (или структуру) фиксированного размера.

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


     
  • 4.72, Sw00p aka Jerom (?), 14:57, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >Операция сложения используется, как единственный источник нелинейности.

    нет, нелинейность в шифрах задают так называемые "бент-функции", в том же aes это его S-Box

     
     
  • 5.74, . (?), 16:18, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Chacha и подобные шифры используют три операции: сложение, xor и побитовый сдвиг. Сложение здесь единственная нелинейная операция. В целом это все дает хорошую защиту от классических методов криптоанализа, основанных на статистике. Но у сложения есть ряд интересных свойств, которые как мне кажется позволяют полностью вскрыть шифры данной конструкции. Естественно, эти свойства сейчас исследуются профессиональными криптографами и в случае обнаружения способа его скорее всего опубликуют.
    Aes кстати тоже содержит не самый лучший s-box из всех возможных. Алгебраический иммунитет 2, хотя можно почти при той же нелинейности 3. Здесь подробнее:
    https://mailarchive.ietf.org/arch/msg/cfrg/iGeC0IO9K0AGS_AvUHcOLMfd8Dk

    Bent-функции (максимально нелинейные) это математическая модель, в чистом виде редко применяются.

     
     
  • 6.80, Sw00p aka Jerom (?), 18:18, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >Но у сложения есть ряд интересных свойств, которые как мне кажется позволяют полностью вскрыть шифры данной конструкции.

    не у сложения (по модулю), а от выбора S-Box

     
     
  • 7.82, . (?), 19:03, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Оригинальная чача, s-box'ов там нет.
    https://github.com/odzhan/tinycrypt/blob/master/stream/chacha/ref/chacha.c
     
     
  • 8.84, Sw00p aka Jerom (?), 20:00, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    ChaCha State это и есть фактический S-box... текст свёрнут, показать
     
  • 8.85, Sw00p aka Jerom (?), 20:07, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    добавлю, почему тогда эти начальные стейты в сальсе были одни, а в чачача ДЖБ их... текст свёрнут, показать
     
     
  • 9.91, Ivan_83 (ok), 00:21, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Напиши ему и спроси ... текст свёрнут, показать
     
  • 9.97, товарищ майор (?), 12:18, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    наши коллеги из NSA очень попросили ... текст свёрнут, показать
     
     
  • 10.108, Sw00p aka Jerom (?), 20:18, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Так это как в случае со слабым S-box Цитата из вики В 2008 году Daniel Bernste... текст свёрнут, показать
     
     
  • 11.112, . (?), 23:14, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    S-box определяет вид нелинейного преобразования У сальсы и чачи нелинейное прео... текст свёрнут, показать
     
     
  • 12.113, Sw00p aka Jerom (?), 00:48, 09/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    рассеивание и запутывание - какие-то упрощенные определения, S-box - блок по... текст свёрнут, показать
     
  • 4.90, Ivan_83 (ok), 00:20, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Согласен. Но все же создалось некоторое впечатление, что сместить пытаются не rc4,
    > а именно aes.

    Чача вроде как быстрее AES если не использовать aes-ni.

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

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

     
  • 4.104, meantraitor (?), 16:21, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > Одномерный массив в си всегда передается как указатель

    А двумерный? А десятимерный?

    > Поэтому, чтобы гарантированно не облажаться с выходом за границы понадобится еще статический
    > анализатор.

    extern int N;
    void foo(int bar[120], int xyz[120]) {
       for (int i = 0; i < N; ++i)
          bar[i] = xyz[i];
    }

    В лучшем случае, статический анализатор предупреждение выдаст.

     
     
  • 5.106, . (?), 17:31, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А двумерный? А десятимерный?

    Вы правы, любой массив это указатель.

    > extern int N;

    Похоже на выстрел в ногу, как и например передача в функцию &(bar[N]). Получается много условностей, но все же гарантировано безопасный кодинг на си мне представляется возможным в некоторых случаях. А именно, когда код может быть полностью проверен статическим анализатором.

     
  • 3.62, Аноним (60), 07:24, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > 1. При такой передаче много лишнего копирования памяти.

    Справедливо для C, но не для C++.

     
     
  • 4.63, Аноним (60), 07:50, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    >> 1. При такой передаче много лишнего копирования памяти.
    > Справедливо для C

    Тут я ошибся.

     
  • 3.103, meantraitor (?), 16:16, 08/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    > 1. При такой передаче много лишнего копирования памяти.

    Ха-ха, а сколько памяти сожрет

    void foo(int64_t array[1024*1024*1024]);

    даже страшно себе представить! ;-P

    > 2. Тут не предусмотрен возврат данных.

    Э?

    void bar(int baz[4], int xyw[4]) {
       for (int i = 0; i < 4; ++i)
          baz[i] = xyw[i];
    }

     

  • 1.22, Аноним (22), 16:25, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    >доказательства надежности
    >KreMLin

    Так толсто, что аж тонко.

     
  • 1.25, Аноним (25), 17:32, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    >KreMLin

    Так вот случаем защита машин подсчёта голосов в США была реализована не на этой библиотеке?

     
     
  • 2.69, Анонимс (?), 14:38, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    На этой, на этой. А так, как она в открытых исходниках, значит, скоро её соберут мантейнеры и включат во все дистрибутивы мира. Ну, вы теперь понимаете, кто самый могущественный в мире и кто может свергать и назначать президентов в любой стране.
     

  • 1.44, Аноним (-), 21:06, 06/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > Например, соответствие спецификации гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти.

    А как же Rust, как же без него?! 😢

     
  • 1.54, анонас (?), 00:01, 07/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Так я не понял, а Rust где?
     
     
  • 2.70, Анонимс (?), 14:41, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    Так, как rust ещё молодой язык, то ещсложно
     
     
  • 3.71, Анонимс (?), 14:46, 07/04/2019 [^] [^^] [^^^] [ответить]  
  • +/
    сложно найти высококвалифицированных специалистов, особенно по криптографии.
     

  • 1.122, getfr (?), 00:59, 12/04/2019 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Математически доказать надежность этой программы, как подавляющего количества других невозможно. Даже если использовать теорию правильности программ
     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Спонсоры:
    Слёрм
    Inferno Solutions
    Hosting by Ihor
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2019 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру