The OpenNET Project / Index page

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



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

"Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от opennews (??), 06-Апр-19, 12:22 
Исследователи из государственного института исследований в информатике и автоматике (INRIA), подразделения Microsoft Research и университета Карнеги — Меллона представили (https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.html) первый тестовый выпуск (https://github.com/project-everest/hacl-star/releases) криптографической библиотеки EverCrypt (https://github.com/project-everest/hacl-star/blob/fstar-mast...), развиваемой в рамках проекта Everest (https://project-everest.github.io/) и применяющей математические методы формальной верификации надёжности. По своим возможностям и производительности EverCrypt очень близка к существующим криптографическим библиотекам (OpenSSL), но в отличие от них предоставляет дополнительные гарантии надёжности и безопасности.

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

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

Код проекта написан на функциональном языке F* (https://www.fstar-lang.org/), предоставляющем (https://arxiv.org/abs/1703.00053) систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) для программ и гарантировать корректность и отсутствие ошибок в реализации при помощи SMT-формул (https://ru.wikipedia.org/wiki/%D0%97%D0%...) и вспомогательных инструментов (https://en.wikipedia.org/wiki/Proof_assistant) доказательства. На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly.
Код на языке F* распространяется (https://github.com/project-everest/hacl-star/) под лицензией Apache 2.0, а итоговые модули на Си  и ассемблере под лицензией MIT. Некоторые части подготовленного проектом кода уже используются в Firefox (https://bugzilla.mozilla.org/show_bug.cgi?id=1387183), ядре Windows (https://www.microsoft.com/en-us/research/blog/evercrypt-cryp.../), блокчейне Tezos (https://www.reddit.com/r/tezos/comments/8hrsz2/tezos_switche.../) и VPN Wireguard (https://lwn.net/Articles/770750/).


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


-  Используемый при разработке инструментарий остаётся не верифицированным, в том числе возможно существование ошибок в F*, KreMLin (https://github.com/FStarLang/kremlin) (верифицирующий транслятор из языка F* в Си) и в компиляторах для сборки кода на Си (если не использовать верифицированный CompCert (http://compcert.inria.fr/compcert-C.html)).
-  Очень трудно правильно и точно воспроизвести спецификации. Например, где-то можно допустить опечатку, а где-то упустить вопрос преобразование порядка следования байтов. Поэтому до того как приступать к созданию оптимизированных версий реализации проводится доскональный аудит и тестирование спецификаций;

-  Применяемые модели верификации не учитывают такие угрозы, как атаки
Spectre и Meltdown, а также не защищают от новых классов ещё не известных атак, которые могут появиться в будущем;

По сути EverCrypt объединяет два ранее разрозненных проекта HACL* (https://github.com/mitls/hacl-star) и Vale (https://github.com/project-everest/vale), предоставляя на их основе унифицированный API и делая их пригодными для применения в реальных проектах.  HACL* написан на языке Low* и нацелен на предоставление криптопримитивов для использования в программах на языке Си с использованием API в стиле libsodium и NaCL. Проект Vale развивал предметно-ориентированный язык для создания верифицированных криптографических примитивов на ассемблере. Около 110 тысяч кода проекта HACL* на языке Low* и  25 тысяч строк кода на Vale объединены и переписаны в примерно 70 тысяч строк кода на универсальном языке F*, который также развивается в рамках проекта Everest. На базе созданных верифицированных примитивов проектом Everest дополнительно развивается стек miTLS (https://mitls.org/) с верифицированной реализацией TLSv1.3.

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

-  Алгоритмы хэшировния: все вариаенты SHA2, SHA3, SHA1 и MD5;
-  Коды проверки подлинности: HMAC поверх SHA1, SHA2-256, SHA2-384 и SHA2-512 для аутентификации источника данных;
-  Алгоритм формирования ключей HKDF (https://en.wikipedia.org/wiki/HKDF) (HMAC-based Extract-and-Expand Key Derivation Function);
-  Потоковый шифр ChaCha20 (http://cr.yp.to/chacha.html) (доступна не оптимизированная версия на Си)
-  Алгоритм аутентификации сообщений (MAC) Poly1305 (http://cr.yp.to/mac.html) (версии на Си и ассемблере),
-  Протокол Диффи-Хеллмана на эллиптических кривых 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 (на первом этапе главной целью является надёжность, а оптимизации и платформы будут реализованы во вторую очередь).


URL: https://news.ycombinator.com/item?id=19563073
Новость: https://www.opennet.ru/opennews/art.shtml?num=50470

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

Оглавление

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


1. "Новая криптографическая библиотека EverCrypt с математически..."  –4 +/
Сообщение от Аноним (1), 06-Апр-19, 12:22 
Интересно, как математически доказать потокобезопасность.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

2. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от адмирал третьего флота очевидно (?), 06-Апр-19, 12:42 
пока никак. увы.
Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

23. "Новая криптографическая библиотека EverCrypt с математически..."  +8 +/
Сообщение от Sw00p aka Jerom (?), 06-Апр-19, 17:27 
Дайте сначала определение "потокобезопасность"-и
Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

47. "Новая криптографическая библиотека EverCrypt с математически..."  +6 +/
Сообщение от Аноним (47), 06-Апр-19, 21:55 
Многопоточные алгоритмы невозможно описать математически?
Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

3. "Новая криптографическая библиотека EverCrypt с математически..."  +8 +/
Сообщение от nc (ok), 06-Апр-19, 12:48 
Какой еще Kremlin?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

5. "Новая криптографическая библиотека EverCrypt с математически..."  +5 +/
Сообщение от Анонимный селебрити (?), 06-Апр-19, 12:54 
Там только его рука :)
Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

27. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от Аноним (27), 06-Апр-19, 18:34 
Т. майор приложил свою лапу к созданию транслятора.
Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

4. "Новая криптографическая библиотека EverCrypt с математически..."  +7 +/
Сообщение от Анонимный селебрити (?), 06-Апр-19, 12:53 
Дейкстра одобряет
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

6. "Новая криптографическая библиотека EverCrypt с математически..."  +2 +/
Сообщение от АНБ (?), 06-Апр-19, 13:10 
> В первом альфа-выпуске уже в основной массе завершена верификация кода, но ещё
> остаются некоторые не охваченные области. Пока не верифицированы и не включены
> в поставку оптимизированные при помощи инструкций SHA-EXT  и AVX варианты
> SHA2-256 и Poly130.   Обещанный уровень производительности в текущий момент
> обеспечен только для алгоритма Curve25519. Также ещё не стабилизирован API, который
> будет расширяться в следующих альфа-версиях (планируется унифицировать структуры для
> всех API по примеру наиболее зрелого EverCrypt_Hash.h и унифицировать коды ошибок
> в EverCrypt.Error). Из недоработок также отмечается поддержка только архитектуры x86_64
> (на первом этапе главной целью является надёжность, а оптимизации и платформы
> будут реализованы во вторую очередь).

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

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

7. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (7), 06-Апр-19, 13:26 
> чисто академическая поделка

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

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

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

9. "Новая криптографическая библиотека EverCrypt с математически..."  +9 +/
Сообщение от пох (?), 06-Апр-19, 13:37 
> На фоне быстрого и проверенного годами OpenSSL

лол.

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

34. "Новая криптографическая библиотека EverCrypt с математически..."  +2 +/
Сообщение от myhand (ok), 06-Апр-19, 19:12 
АНБ проверило.  А ты хто такой?
Ответить | Правка | ^ к родителю #9 | Наверх | Cообщить модератору

41. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от пох (?), 06-Апр-19, 20:52 
у ентого вашего "АНБ" чекистский значок, кажись, на лацкане...

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

48. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от myhand (ok), 06-Апр-19, 22:21 
А вы каких фашистов выбираете?
Ответить | Правка | ^ к родителю #41 | Наверх | Cообщить модератору

18. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (18), 06-Апр-19, 15:13 
Libressl лучше
Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

73. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от dabdabya (?), 07-Апр-19, 15:27 
Кто-то минус влепил,но он действительно лучше. Libressl не требует perl для сборки и при сборке с -O3 быстрее того же openssl,который тоже собран с -O3
Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

123. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (123), 12-Апр-19, 12:39 
Только BoringSSL, только хардкор!
Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

35. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от ФАПСИ (?), 06-Апр-19, 19:16 
Абсолютно с вами согласен, коллега!
Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

11. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от X4asd (ok), 06-Апр-19, 14:06 
> Код на языке F* распространяется под лицензией Apache 2.0, а итоговые модули на Си и ассемблере под лицензией MIT

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

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

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

14. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от пох (?), 06-Апр-19, 14:25 
> как это понять?

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

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

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

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

21. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (21), 06-Апр-19, 15:42 
> за скомпилированный они меньше переживают

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

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

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

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

26. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 06-Апр-19, 17:52 
> О скопмилированном коде тут речь не идет.

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

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

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

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

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

30. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (27), 06-Апр-19, 18:53 
>С кодом, который ты накомпилируешь сам из 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*.

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

51. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 06-Апр-19, 23:17 
> Так что можешь хоть под GPL прелицензировать, то, что сам странслировал с
> F*.

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

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

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

31. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от Sw00p aka Jerom (?), 06-Апр-19, 18:58 
речь идет именно о сгенерированном Си коде, никакой компиляции

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

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

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"

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

40. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (40), 06-Апр-19, 20:33 
> речь идет именно о сгенерированном Си коде, никакой компиляции

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

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

45. "Новая криптографическая библиотека EverCrypt с математически..."  –3 +/
Сообщение от Sw00p aka Jerom (?), 06-Апр-19, 21:12 
>с потерей человекочитаемости называется компиляцией

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

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

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

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

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

49. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 06-Апр-19, 22:50 
> пс: цитата из вики, для особо одаренных

вашу викивракию пишут такие же "эксперты" как и вы - не посещавшие даже лекции для первокурсников про теорию компиляторов. Так, что-то слышавшие краем уха.

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

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

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

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

57. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 00:35 
>не посещавшие даже лекции для первокурсников про теорию компиляторов.

ок, понятно, а теперь ответьте на один вопрос - кто автор "теории компиляторов"? ответите и дальше продолжим дискуссию.

>не вдаваясь в подробности в каком году и какими специалистами она написана.

ну вот отлично, жду ответа на свой вопрос.

пс: как называется процесс "текст на русском" -> "текст на английском" ?
вот коту моему все равно с какого на какой язык транслировали, ему нужно в итоге транслировать в "кыскыскыс", "мяумяу", "ахтыскотина", "брысьотсюда". Моему желудку все равно каков рецепт и какую душу вложил кулинар, ему важней объем белков, жиров и углеводов.

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

58. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 00:37 
про первокурсников, а вы собственно из серии программистов которым "не нужна математика"?
Ответить | Правка | ^ к родителю #49 | Наверх | Cообщить модератору

68. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от t_ (?), 07-Апр-19, 12:53 
Самое забавное, что он прав и в вики это тоже верно написано.

Перечитайте что ли вводную главу книги драконов.

Кричать про экспертов и, при этом, не отличать компилятор от транслятора - гиблое дело.

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

75. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от Аноним84701 (ok), 07-Апр-19, 16:46 
Девочки, не ссорьтесь!

Cуществует "и то и это".
Остроконечники^W различающие "перевод" (трансляцию) и тупоконечники^W считающие компиляцию частным случаем трансляции. Тоже  "0 ∈ ℕ vs 0  ∉ ℕ", только в профиль.
Классический пример: "переводчик формул" (FORmula TRANslation, FORTRAN)

> Перечитайте что ли вводную главу книги драконов.

Цитирую, с картинками:

> 1.1. Language Processors
> Simply stated, a compiler is a program that can read a program in one language -- the source language -- and translate it into an equivalent program in another language -- the target language; see Fig.1.1
> An important role of the compiler is to report any errors in the source program that it detects during the translation process.
>Figure 1.1: A compiler


source program
        |
        v
+-------------+
|   Compiler  |
+-------------+
       |
       v
target program

В той же англоязычной википедии стоит:
> A compiler is a computer program that translates computer code written in one programming language (the source language) into another programming language (the target language).

Более того, с этим же "согласны"  берклеевцы:
http://inst.eecs.berkeley.edu/~cs164/sp19/lectures/lecture1.pdf
> Implementing Programming Languages
> • Strategy 2: Compiler: program that translates program into machine

[...]
> – Variant of 2: Compiler that translates program into another programming language (such as C), or into an intermediate language (such as Java class format) for which there is a translator or compiler.

Т.е. компилятор тут - частный случай/разновидность транслятора.

> Кричать про экспертов и, при этом, не отличать компилятор от транслятора - гиблое дело.

Судить по этому критерию о качестве знаний - не менее гиблое.

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

81. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 18:58 
>Т.е. компилятор тут - частный случай/разновидность транслятора.

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

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

83. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним84701 (ok), 07-Апр-19, 19:41 
>>Т.е. компилятор тут - частный случай/разновидность транслятора.
> Да, но именно результат "компиляции" (это типа последняя фаза трансляций) может спокойно
> исполняться на конечной машине,

Может, а может и нет. Я просто подсказываю, что зависит от используемой (вполне общепринятой) терминологии с использованием более общего понятие "compiler" (т.е. включая переводчик).
Я вообще не собираюсь спорить о том, чья классификация (не)правильная. Просто (по факту) есть и та и другая, используется специалистами и по моему глупо игнорировать или делать вид, что  "правильно только наше понимание и наша терминология!".

> даже "Ассемблер" транслируя ассемблерный код в "нули  и единицы", которые могут спокойно исполниться машиной, совершает процесс "компиляции"

Э-э-э не-не, ассемблер как раз обычно вне таких классификаций и стоит особняком.

Если брать ту же Книгу Драконов, то assembly там одна из возможных конечных целей компилятора.
Хотя сам процесс превращения современного assembly-кода c его тучей макросов, структур и довольно сложными вычислениями "времени ассемблеризации"  и прочим, вполне тянет на "полноценную" компиляцию.
В общем, "все сложно".

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

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

86. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 20:25 
>Э-э-э не-не, ассемблер как раз обычно вне таких классификаций и стоит особняком.

нет не стоит, и он от ЯП других ничем не отличается, ибо он из мнемонического кода транслирует в коды операций процессора. И я именно эту стадию считаю как понятие "компиляции", в других случаях это все трансляция (перевод).

тип такого:

англ ->(тут перевод в) рус ->(тут перевод в) нем ->(тут компиляция) кошачий. :)

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

что есть конечная цель? представить код "понятный" процессору (машине).

>Хотя сам процесс превращения современного assembly-кода c его тучей макросов, структур и довольно сложными вычислениями "времени ассемблеризации"  и прочим, вполне тянет на "полноценную" компиляцию.

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

>Правда, я не припоминаю ни одной "накладки" или путанницы из-за этого на практике

так проблема в строгом определении любого понятия, ибо если его нет, то все ведет к таким дискуссиям (холиварам). Можем еще и похоливарить на тему JIT компиляции.

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

87. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним84701 (ok), 07-Апр-19, 20:51 
> нет не стоит, и он от ЯП других ничем не отличается,

То что не отличается, я даже не спорил, а вот то что все же стоИт, пусть в основном и по историческим причинам "так принято" - с этим как раз сталкиваешься достаточно часто (см. man gcc опция -S или -c)
>  И я  именно эту стадию считаю как понятие "компиляции", в других случаях это  все трансляция (перевод).

*пожимая плечами* а авторы библиотеки похоже придерживаются другой классификации и наверное стоит принимать во внимание в первую очередь ее.

>>Если брать ту же Книгу Драконов, то assembly там одна из возможных конечных целей компилятора.
> что есть конечная цель? представить код "понятный" процессору (машине).

Это очередная неточность перевода:
Конечная цель - в смысле результата работы самого компилятора: в оригинале "compiler target".

Ну и не припоминается ни одного современного компилятора, генерирующего сразу машинный код.
В качестве еще одного примера приходит на ум тот же (g)as, как "классический" бэкэнд для gcc.
Кстати, там (как и в clang, других компиляторов чтобы проверить, у меня сейчас нет), как раз различают этот нюанс:


man gcc
-c  Compile or assemble the source files, but do not link.  The linking
           stage simply is not done.  The ultimate output is in the form of an
           object file for each source file.
[...]
           Unrecognized input files, not requiring compilation or assembly,
           are ignored.

       -S  Stop after the stage of compilation proper; do not assemble.

man clang
-c     Run all of the above, plus the assembler, generating a target
              ".o" object file.


> так проблема в строгом определении любого понятия, ибо если его нет, то
> все ведет к таким дискуссиям (холиварам). Можем еще и похоливарить на  тему JIT компиляции.

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

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

88. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 21:28 
>Конечная цель - в смысле результата работы самого компилятора: в оригинале "compiler target".

Так результат работы того же gcc с опцией -c (Compile or assemble) на выходе даёт "The ultimate output is in the form of an object file for each source file.", обратим внимание на "object file", что это? это разве промежуточный код?

открываем википедию и читаем

"Объектные файлы представляют собой блоки машинного кода и данных с неопределенными адресами ссылок на данные и процедуры в других объектных модулях, а также список своих процедур и данных."

А компоновщик уже тупо свяжет их, и создаст полноценный исполняемый файл.

Так, что же в итоге такое процесс компиляции, как не трансляция в машинные коды операций.


>Ну и не припоминается ни одного современного компилятора, генерирующего сразу машинный код.

Go-lang - не? "сразу машинный код" может сгенерить только очень близкий к машинному ЯП, то есть "Ассемблер как ЯП"

>как и в clang, других компиляторов чтобы проверить, у меня сейчас нет

если брать llvm, то clang транслирует в биткод llvm (промежуточный), и собственно ассемблер llvm готовит машинный.

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

94. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (94), 08-Апр-19, 11:57 
>>Т.е. компилятор тут - частный случай/разновидность транслятора.
> Да, но именно результат "компиляции" (это типа последняя фаза трансляций) может спокойно
> исполняться на конечной машине, даже "Ассемблер" транслируя ассемблерный код в "нули
> и единицы", которые могут спокойно исполниться машиной, совершает процесс "компиляции"
> (то есть привести к виду "исполняемого" на конкретной машине).

"Ассемблер" совершает процесс "ассемблирования". Это когда каждая мнемоника транслируется в машинную команду 1 в 1. Есть ещё макроассемблеры, позволяющие генерировать группы команд по шаблону (макросу). А есть т.н. "assembly compiler". Например, https://en.wikipedia.org/wiki/High_Level_Assembly -- первые версии компилировали исходный код в исходники для других ассемблеров. Однако, ключевым отличием "компилятора ассемблера" является способность производить не всеми очевидные преобразования (в частности, оптимизации), когда один и тот же фрагмент исходного текста порождает различный машинный код.

И, кстати, выхлоп после мало какого ассемблера может исполняться без линковки непосредственно.


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

105. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от Sw00p aka Jerom (?), 08-Апр-19, 16:52 
>первые версии компилировали исходный код в исходники для других ассемблеров.

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

компайлед или там ассемблед это уже готовый машинный код, который исполняется. Исходный код на питоне странсилованный в исходный код на Си - исполнится?

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

116. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (94), 09-Апр-19, 07:59 
>>первые версии компилировали исходный код в исходники для других ассемблеров.
> это не компиляция!!! - а перевод (трансляция, кодогенерация в другой язык, называйте
> как хотите)

"Это" была цитата (в переводе) René Tournois (Betov), автора SpAsm и RosAsm (см. https://web.archive.org/web/20040602212238/http://betov.free...)

Возможно, его мнение несколько предвзято, поскольку заявлено в священной войне с Randall Hyde (автором HLA), но это мнение -- практика.

> компайлед или там ассемблед это уже готовый машинный код, который исполняется. Исходный
> код на питоне странсилованный в исходный код на Си - исполнится?

Не вижу связи с классификацией ассемблеров.

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

99. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от t_ (?), 08-Апр-19, 13:59 
Ты молодец. Открыл нужную книгу, выделил слово translate, но вывод сделал неверный.

Компилятор не является частным случаем или разновидностью транслятора.
Компиляция вообще с трансляцией не связана, это разные процессы.

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

Не надо путать компилятор-программу и компиляцию-процесс.

Трансляция занимается переводом.
Компиляция занимается сборкой.

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

>> Кричать про экспертов и, при этом, не отличать компилятор от транслятора - гиблое дело.
> Судить по этому критерию о качестве знаний - не менее гиблое.

Согласен.
Но у человека много гонора, и прежде чем посылать других на курсы, неплохо было бы ему самому на них сходить.
Почитай его комменты, у него есть опыт и из-за этого сильно развито ЧСВ, а база-то непрочная для дискуссий.

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

109. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним84701 (ok), 08-Апр-19, 21:56 
> Ты молодец. Открыл нужную книгу, выделил слово translate, но вывод сделал неверный.
> Компилятор не является частным случаем или разновидностью транслятора.
> Компиляция вообще с трансляцией не связана, это разные процессы.
> Транслятор является подпрограммой компилятора.
> Если выкинуть транслятор из компилятора,

Еще раз - "translator" в _этом_ варианте англоязычной терминологии  вообще как-то специально не выделяется (кроме процесса "translation").
А еще есть такое понимание:
https://www.microcontrollertips.com/compilers-translators-in.../
> Translators
> The most general term for a software code converting tool is “translator.”
>  A translator, in software programming terms, is a generic term that could refer to a compiler, assembler, or interpreter;

Короче, мне далее срат^W обсуждать тонкости различия терминологии в  переводе не интересно -- изначально речь шла о формулировках в #14-#21
>> На основании эталонного кода на языке F* затем генерируется код на ассемблере, Си, OCaml, JavaScript и Web Assembly.
> О скопмилированном коде тут речь не идет. Поэтому не путайте. Скомпилированный исходный код под той же лицензией, что и сам исходный код.

Т.е. именно в этом контексте различать "translator" и утверждать "translation != compilation" (точнее, заявлять что генерация кода != компиляция поэтому не считается) … не, конечно можно, но смысл, если из контекста документации и описания понятно, что авторы придерживаются другой терминологии и вряд ли комментарии на опеннете ее изменят?

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

114. "Новая криптографическая библиотека EverCrypt с математически..."  +2 +/
Сообщение от t_ (?), 09-Апр-19, 01:21 
> A translator, in software programming terms, is a generic term that could refer to a compiler, assembler, or interpreter;

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

Здесь нет никакого противоречия.


Этот термин пришёл из обработки документов. К ней он и относится, и означает упорядочение информации собранной из разных источников.

Представь, что у тебя есть набор лабораторных работ. Из которых тебе надо сделать курсовую. Наверное слышал словосочетание "скомпилированная работа"?

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

2) Ты берёшь эти лабораторки, копируешь их в большой текст, потом берёшь и редактируешь текст, добавляешь новый, переставляешь абзацы местами, задействуешь синонимайзеры. Компиляция была? Разумеется была. Она всегда есть! В данном случае с оптимизацией.

3) Ты берёшь эти лабораторки, но тебе надо написать работу на английском. Ты их переводишь и сохраняешь в один текст.
Аналог: компиляция выполнена с трансляцией (переводом). На выходе результат на другом языке. И только в случае трансляции получается ДРУГОЙ язык, например Vala => C.

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

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

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

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

Вот на это отличие обратил внимание Sw00p aka Jerom.
У него пока тоже нет полного понимания, но можно было бы объяснить ему это по-человечески, не самоутверждаясь.

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

117. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 09-Апр-19, 18:41 
>трансляция отвечает за перевод данных из исходной формы в результирующую.

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

Хочу отметить, что я делаю именно акцент на "конечный этап трансляции" - это и есть компиляция. Вот такое строгое мое мнение понятия компиляции.

>Представь, что у тебя есть набор лабораторных работ. Из которых тебе надо сделать курсовую. Наверное слышал словосочетание "скомпилированная работа"?

###
Сырбор всей дисскуссии начался с того, что "трансляция" (перевод) с одного исходного текста ЯП на другой исходный текст был назван как процесс компиляции. (Что по моему мнению - ложно. И попытаюсь это доказать в итоге.)
###

>Ты берёшь эти лабораторки и копируешь в один большой текст. Компиляция была? Была.

Нет, не была. Была "сборка" в выше указанном моем определении процесса компиляции.

>Компиляция была? Разумеется была. Она всегда есть! В данном случае с оптимизацией.

Нет, не была, таже самая "сборка". Оптимизацию объясню ниже.

>Аналог: компиляция выполнена с трансляцией (переводом).

Из моего определения процесса компиляции - "итоговая трансляция" (конечный этап).


>На выходе результат на другом языке. И только в случае трансляции получается ДРУГОЙ язык, например Vala => C.

И как я понял, в итоге по вашему мнению "процесс компиляции" есть процесс трансляции из языка A в язык B.

Отсюда, по вашему мнению, процесс трансляции (перевода) из Python в C - есть процесс компиляции, так ли это ? Если да, то приведу такой пример.

Допустим, есть множество языков вида L1, L2, L3 ... LN, где LN есть "результирующий язык" (машинные коды операций), а пронумерованные это прочие высокоуровневые ЯП. Введем оператор трансляции "->" (стрелочка).

Из вашего мнения следует L1 -> L2 - есть процесс компиляции, тогда L1 -> L1` (штрих) также есть процесс компиляции. L1` (штрих) - тут в роли процесса "обфускации" или же "рефакторинга", та же "оптимизация". И получается, что это так же трансляция если строго трансляцию не принимать как только L1 -> L2.


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

"для получения готового результата" - то есть исполняемого? Если да, то Python -> C, где тут "готовый результат"? Вы противоречите своему определению процесса компиляции.


>Но так как в кодогенерации компиляция и интерпретация не имеют смысла без трансляции, то компиляторы и интерпретаторы общепринято называются трансляторами.

Тут как-то сумбурно, кодогенерации это фактическая трансляция.


>Вот на это отличие обратил внимание Sw00p aka Jerom.
>У него пока тоже нет полного понимания, но можно было бы объяснить ему это по-человечески, не самоутверждаясь.

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

Если бы каждый шаг L1 -> L2 -> L3 ... -> LN и весь процесс трансляций в целом называть компиляцией, то зачем мы еще порождаем всякие понятия L1 -> L1` (штрих) как "обфускация", "рефакторинг", "оптимизация"?

Почему мы принимаем Java как "компилируемый язык"?

Пример:

Python -> Java -> Java-bytecode (конечный этап трансляции для JVM)

Этот пример имеет место быть, так как Java-bytecode тут конечный этап трансляции для JVM, и по моему мнению (когда конечный этап - это машинные коды операций), компиляция тут заключается только лишь в процессе трансляции Java -> Java-bytecode, но не Python -> Java. И эту компиляцию, для строгого отличия от "нативной" (Asm -> CPU Opcodes), я называю - "виртуальной компиляцией".

Тоже самое: C -> Asm -> CPU Opcodes, Asm -> CPU Opcodes - последняя стадия трансляции - компиляция, C -> Asm - просто трансляция (обычно говорят кодогенерация)

пс: всем спасибо за участие в дискуссии.

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

118. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от t_ (?), 10-Апр-19, 02:38 
Изначально верный ответ дал Аноним84701 :D
> Девочки, не ссорьтесь!
> Cуществует "и то и это".

===============================

> если "результирующую" понимать как конечный этап (машинные коды операций), то да это и есть по моему мнению процесс компиляции

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

> Хочу отметить, что я делаю именно акцент на "конечный этап трансляции" - это и есть компиляция.

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

> Сырбор всей дисскуссии начался с того, что "трансляция" (перевод) с одного исходного текста ЯП на другой исходный текст был назван как процесс компиляции. (Что по моему мнению - ложно. И попытаюсь это доказать в итоге.)

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

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

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

> Если бы каждый шаг L1 -> L2 -> L3 ... -> LN и весь процесс трансляций в целом называть компиляцией, то зачем мы еще порождаем всякие понятия L1 -> L1` (штрих) как "обфускация", "рефакторинг", "оптимизация"?

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

> Почему мы принимаем Java как "компилируемый язык"?

Потому что он компилируется в байт-код для виртуальной машины.

Но понятие "компилируемый язык" лично я не люблю. Потому что это зависит от реализации.
Например, для бейсика выпускались как компиляторы, так и интерпретаторы.

Или вот строчка из вики про Python: "В отличие от компилируемых языков программирования, в Python...".
То есть Python, фактически, объявляется некомпилируемым языком. И при этом "Файлы .pyc содержат скомпилированный байт-код исходных файлов Python". Но как же так? Ведь Python объявили интерпретируемым языком, а оказывается это не мешает его скомпилировать. Причём делает это лично интерпретатор Python, потому что в нём есть модуль компиляции.

Мне больше нравится такое утверждение:
"a language is not "interpreted" or "compiled" as such. A specific implementation can be an interpreter or a compiler (or a hybrid or a JIT compiler or a vm etc)".

Написать интерпретатор java помешает лицензия и огромный объём работы, но возможность этого никто не отменял. :)
Будет своя тормозная реализация интерпретатора джавы без виртуальной машины.
Можешь даже сам попробовать реализовать интерпретатор хотя бы для небольшого подмножества джавы (хотя бы операторы c++) и всё будет работать. Компилируемый, интерпретируемый - это просто ярлыки, применимые для конкретных реализаций.

> компиляция тут заключается только лишь в процессе трансляции Java -> Java-bytecode, но не Python -> Java

Именно тут ошибка.

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

К dragonbook, и раз тебе нравится вики, можно добавить ссылку:
https://en.wikipedia.org/wiki/Source-to-source_compiler

> пс: всем спасибо за участие в дискуссии

Взаимно! :)

-------------------------------------------------------

Резюме:
1) компиляция != трансляция - процессы разные, трансляция выполняется внутри компиляции
2) компилятор == транслятор - компилятор выполняет трансляцию в процессе компиляции
3) "конечный этап" не обязательно равен "машинные коды операций". это частный случай. можно скомпилировать исходный код одного языка в исходный код другого

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

На этом я завершаю свой флуд.

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

119. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 10-Апр-19, 15:03 
Если приводить цитаты из вики, то повторюсь:

https://en.wikipedia.org/wiki/Source-to-source_compiler

Читаем раздел history:

"""
One of the earliest programs of this kind was Digital Research's XLT86 in 1981, a program written by Gary Kildall, which translated .ASM source code for the Intel 8080 processor into .A86 source code for the Intel 8086.
"""

Суть такого компилятора ограничивалась уже самым "конечным яп".

Но читаем дальше раздел Programming language implementations:

И видим, что скрестили ежа с ужем.

Но давайте остоновимся на определении:

"""
A source-to-source compiler is a type of compiler that takes the source code of a program written in a programming language as its input and produces the equivalent source code in the same or a different programming language.
"""

То есть "Транспайлер — тип компилятора", а что такое компилятор из той же вики?

https://ru.wikipedia.org/wiki/%D0%9A%D0%...

"""
Компиля́ция — сборка программы, включающая трансляцию всех модулей программы, написанных на одном или нескольких исходных языках программирования высокого уровня и/или языке ассемблера, в эквивалентные программные модули на низкоуровневом языке, близком машинному коду (абсолютный код, объектный модуль, иногда на язык ассемблера)[2][3][4] или непосредственно на машинном языке или ином двоичнокодовом низкоуровневом командном языке и последующую сборку исполняемой машинной программы.
"""

А сам процесс описан строго:

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

А теперь повторно задам вопрос: Трансляция из Python -> C, C - является "машинно-ориентированным языком"? Если нет, то как можно этот процесс трансляции называть компиляцией?

пс: Из вашего мнения следует, помимо "обфускации", "рефакторинга", "оптимизации", что и обычное "редактирование" исходного кода есть процесс компиляции. Так ли это?


пс2: Выше Пох подставил под сомнение статью в википедии об компиляторе, но в тоже самое время приводит из неё же статью про транспайлер, в которой ссылка на понятие компилятора. И вы собственно так же поступаете, не противоречивы ли ваши действия?

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

120. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от t_ (?), 10-Апр-19, 23:40 
> А теперь повторно задам вопрос: Трансляция из Python -> C, C - является "машинно-ориентированным языком"? Если нет, то как можно этот процесс трансляции называть компиляцией?

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

"A source-to-source COMPILER is a type of COMPILER that takes the source code of a program written in a programming language as its input and PRODUCES the EQUIVALENT SOURCE CODE in the same or a different programming language."

Что в слове compiler непонятно? При такой компиляции, без трансляции в машинно-ориентированный язык, никакого машинно-ориентированного языка на выходе нет.

> пс: Из вашего мнения следует, помимо "обфускации", "рефакторинга", "оптимизации", что и обычное "редактирование" исходного кода есть процесс компиляции. Так ли это?

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

Но компиляция не об этом, она об организации данных из разных источников. Что подразумевается под разными источниками? Это, во-первых, источники данных на входе процесса компиляции (например, файлы в дереве кода и за его пределами), а во-вторых - обработанные данные на выходах промежуточных процессов, которые занимаются преобразованием данных внутри процесса компиляции (Здесь и выше я специально выделяю процесс компиляции, потому что ещё есть промежуточные процессы внутри трансляции и прочих процессов. Они отношения к компиляции не имеют, как и их результативные данные.)

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


> пс2: Выше Пох подставил под сомнение статью в википедии об компиляторе, но в тоже самое время приводит из неё же статью про транспайлер, в которой ссылка на понятие компилятора. И вы собственно так же поступаете, не противоречивы ли ваши действия?

Это не противоречие, а дополнение.
Включи логику уже. :)

Истинно ли высказывание в вики, или ложно?

1) Из определения уже явно видно, что оно состоит из двух утверждающих частей, и что преобразование в язык, близкий к машинному коду тоже выполняется трансляцией: "(включающая ТРАНСЛЯЦИЮ всех модулей программы, написанных на одном или нескольких исходных языках программирования высокого уровня и/или языке ассемблера, В эквивалентные программные МОДУЛИ НА низкоуровневом ЯЗЫКЕ, БЛИЗКОМ МАШИННОМУ КОДУ)" - это одна часть. Никакой речи о компиляции, которая что-то переводит в другое представление (машинно-зависимый язык и пр.), не идёт. И правильно, компиляция не занимается переводом в машинно-зависимый код, что ты утверждаешь, ссылаясь на это определение. А где же речь о компиляции? А она в оставшейся части:

2) (Компиляция - СБОРКА программы), (тут первая часть про трансляцию). Вот же компиляция, она просто передаёт исходные данные транслятору и СОБИРАЕТ результаты трансляции в конкретную форму, необходимую для дальнейшей обработки и передачи другим процессам.

Что и следует из толкований глаголов: compile и translate. Как ни странно - слова на английском языке тоже берутся не от балды.

Чтобы доказать истинность или ложность вики перефразируем определение в вопросительной форме:
является ли "сборка программы, включающая трансляцию всех модулей программы, написанных на одном или нескольких исходных языках программирования высокого уровня и/или языке ассемблера, в эквивалентные программные модули на низкоуровневом языке, близком машинному коду" компиляцией?

То есть, можно ли назвать это действие/процесс (а на самом деле - совокупность процессов) компиляцией?
Конечно можно, такой вариант существует. Значит вики не врёт.

Далее рассуждаем.
Раз существуют компиляторы не в низкоуровневые языки, что противоречит вики, и, при этом, вики не врёт, значит вики содержит неполную информацию. Причём неполную информацию содержит только русская вики, потому что в английской всё в порядке:
1) "The name compiler is PRIMARILY used..." (primarily фактически означает "данное определение не является строгим")
2) "A program that translates between high-level languages is usually called a source-to-source compiler or transpiler". (Тут видим упоминание о компиляторах-транспиляторах.)

Пох подставил под сомнение статью, потому что она не описывает различные варианты, про которые он знает, потому что у него есть опыт. Зато статья про транспилятор дополняет статью про компилятор.

Что тут добавить. Не стоит основываться на одном источнике информации. Или даже массе источников, если они повторяют одно и то же.

---------------

Насчёт противоречий. Подумал, и решил сделать ещё пару противоречий к резюме предыдущего сообщения (чтобы жизнь мёдом не казалась) :)

1) компиляция != трансляция - процессы разные, трансляция выполняется внутри компиляции
2) компиляция == трансляция - на выходе компиляции - оттранслированный код. Поскольку трансляция выполнилась внутри компиляции, то можно считать трансляцию подпроцессом и синонимом компиляции

3) компилятор == транслятор - компилятор выполняет трансляцию в процессе компиляции
4) компилятор != транслятор - целое не является частью самого себя (высказывание работает не всегда!).

Поразмышляй над ними. Как поймёшь разницу, тогда выйдешь на другой уровень понимания. А лучше сам напиши какой-нибудь компилятор-транслятор.
Это как смотреть на картинку, где нарисована одновременно старуха и молодая девушка. А некоторые люди могут видеть что-то одно, пока не попробуют смотреть по-другому. И трудно объяснить, как надо смотреть.

P.S. Сайт уже скукожился. Давай закругляться :) А то уже надоело заниматься т(а)(у)фтологией (выбрать подходящее)
Всё равно дальше я могу лишь предыдущие сообщения цитировать.

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

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

121. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 11-Апр-19, 01:17 
>компиляция не требует обязательного результата в виде машинно-ориентированного языка

где на странице в вике о компиляторе это написано? там строго утверждено - результат в виде машинно-ориентированного языка.

>A source-to-source COMPILER

Это уже противоречие, потому-что COMPILER это source-to-opcodes по определению в самой же вики на странице компилятора.

>Но обычным редактированием это не назовёшь.

Из вашего же определения выходит, что "редактирование" как следствие компиляции. У вас все есть компиляция.

>Это не противоречие, а дополнение.
>Включи логику уже. :)

Дополнение к чему? когда под гребенку компиляции можно и редактирование кода пихнуть?

>И правильно, компиляция не занимается переводом в машинно-зависимый код, что ты утверждаешь, ссылаясь на это определение. А где же речь о компиляции? А она в оставшейся части:

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

>Раз существуют компиляторы не в низкоуровневые языки, что противоречит вики, и, при этом, вики не врёт, значит вики содержит неполную информацию.

Отличная логика, раз существует то, что противоречит определению, значить это должно считаться дополнением к определению? Вот я вам и привел в пример, что по вашей логике и редактирование кода есть компиляция. И весь прикол в том, что если не принимать строгого определения понятия компиляции, то под гребенку компиляции можно дополнить всё что угодно.

Про  "раз существует" замечу, коментом выше указал, вы читали раздел History по ссылке source-to-source COMPILER? Извратить (дополнить) можно всё, а смысл тогда в строгих определениях?

>"The name compiler is PRIMARILY used..." (primarily фактически означает "данное определение не является строгим")

PRIMARILY - в основном, и это утвердительно, строгое определение.

>"A program that translates between high-level languages is usually called a source-to-source compiler or transpiler". (Тут видим упоминание о компиляторах-транспиляторах.)

вот оно что, так речь пошла уже о совсем другом процессе? поэтому придумали новый термин транспайлер, ибо термин компайлер в связке с source-to-source противоречит определению понятия компайлер?


>Пох подставил под сомнение статью, потому что она не описывает различные варианты, про которые он знает, потому что у него есть опыт.

Я что-то от него не услышал про те самые варианты про которые он знает (у него есть опыт? пусть поделится, буду только благодарен).

>Зато статья про транспилятор дополняет статью про компилятор.

Когда я говорил, что source-to-source это банальная трансляция, Пох говорил что компиляция, а выяснилось в итоге, что это транспиляция какая-то.

>1) компиляция != трансляция - процессы разные, трансляция выполняется внутри компиляции

Если разные процессы, то и сравнивать их незачем. Но в моем мнении именно последний этап трансляции включается в процесс компиляции. Все предыдущие - нет.


>4) компилятор != транслятор - целое не является частью самого себя (высказывание работает не всегда!).

https://ru.wikipedia.org/wiki/%D0%9F%D0%...

>Поразмышляй над ними. Как поймёшь разницу, тогда выйдешь на другой уровень понимания. А лучше сам напиши какой-нибудь компилятор-транслятор.

На пенсии займусь как раз этим, ща по времени никак.

>Это как смотреть на картинку, где нарисована одновременно старуха и молодая девушка.

здравомыслие должно иметь место всегда.

>Удачи в осознании разницы!

Лучше уж истины, и вам того же.


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

60. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (60), 07-Апр-19, 07:06 
> пс: цитата из вики, для особо одаренных

Вообще-то "Вики" сама суть результат компиляции (com-pile дословно "в одну кучу").

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

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

79. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним84701 (ok), 07-Апр-19, 17:35 
> )))) пройдите по ссылке указанной выше, и вовсе не компиляция, а трансляция (кодогенерация)

Выше по ссылке
https://github.com/project-everest/hacl-star
> All our code is written and verified in F* and then compiled to C via the KreMLin tool.

Еще используется "extraction"
> HACL* relies on F* (stable branch) and KreMLin (stable branch) for verification, extraction to OCaml (specs/) and extraction to C (code/).

https://github.com/FStarLang/kremlin/
> KreMLin is a tool that extracts an F* program to readable C code.
> This work has been formalized on paper. 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.

Очевидно, что авторы не пользуются терминологией с явно выраженным различием между "translation" и "compilation", поэтому прискипывание к конечной формулировке (тем более, после перевода) вряд ли что-то даст в конечном результате (т.е. вне опеннета).

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

50. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 06-Апр-19, 23:07 
> Автоматическая генерация кода на одном языке из исходников на другом с потерей
> человекочитаемости

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

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

В общем-то, и выхлоп gcc -S тоже вполне человекочитаем, а что там нечеловеческая фигня написана - так она в общем-то и в исполняемом коде такая же и остается ;-)
Видимо, gcc по мнению адептов викивракии тоже "не компилятор".

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

а последняя фраза верная. Собственно, вон есть такой прекрасный llvm - производит он нечто примерно такое: http://llvm.org/docs/LangRef.html#module-structure - никакая "машина" (в том смысле, в котором поняли бы современники термина "машинный код") ЭТО не исполняет, ни в текстовой форме, ни в какой либо другой. (человекочитаемым, на мой взгляд, это тоже не является, но это кому как. Лично я уж лучше выхлоп gcc -S читать буду)

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

66. "Новая криптографическая библиотека EverCrypt с математически..."  +2 +/
Сообщение от myhand (ok), 07-Апр-19, 11:11 
> вы только в википедию этот бред теперь не пишите вместо того

Почему-ж?  В помойку надо складать мусор, она для того и предназначена.

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

101. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от meantraitor (?), 08-Апр-19, 15:59 
> Собственно, вон есть такой прекрасный llvm - производит он нечто примерно такое:
> http://llvm.org/docs/LangRef.html#module-structure - никакая "машина" (в том смысле, в котором
> поняли бы современники термина "машинный код") ЭТО не исполняет, ни в текстовой форме, ни в
> какой либо другой. (человекочитаемым, на мой взгляд, это тоже не является, но это кому как.
> Лично я уж лучше выхлоп gcc -S читать буду)

Вы сравниваете ежа с ужом. По ссылке, которую вы привели, описана текстовая сериализация
внутреннего представления (IR) компилятора. Из gcc что-то подобное тоже можно выковырять
и вряд ли оно вам больше понравится.
Хотите сравнивать - сравнивайте clang -S vs. gcc -S.
Чтоб вы знали - эта фича (сериализация/десериализация IR в/из текста) - одна и немногих
реально крутых и полезных фич. Если это вам кажется нечеловекочитаемым - не читайте, оно не
для вас предназначено.

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

111. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 08-Апр-19, 23:10 
> Вы сравниваете ежа с ужом.

вы, похоже, не владеете темой.

Вся суть проекта llvm - что вот это вот "внутреннее представление" и есть результат работы его компиляторов. Фронтэнды именно llvm и производят, из любого языка.
А binary targets обеспечиваются на следующем этапе, backend'ом. Причем наличие у бэкэнда asm printer'а - желательная, но совершенно необязательная фича, и совершенно параллельная binary emitter (так что еще и не факт, что на любой платформе -S вообще работоспособен)

> Из gcc что-то подобное тоже можно выковырять

у gcc, afaik, это именно сугубо внутреннее даже не "представление", а состояние компилятора, причем каждого отдельное - выковырять может и можно, но обратно запихать невозможно, и уж тем более у них нет никакого формального "language reference" для этого представления, оно языком вообще не является.

А здесь это именно язык llvm. Но совершенно нечеловекочитаемый, даром что похож.

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

124. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от meantraitor (?), 12-Апр-19, 13:00 
> вы, похоже, не владеете темой.

Да-да, уже 15 лет не владею ;)

Все современные компиляторы так устроены уже давно - фронтенды производят IR (intermediate
representation), который уже далее обрабатывается middleend'ом и/или backend'ом.
И, кстати, этих IR'ов может быть несколько в одном и том же компиляторе

И gcc и llvm именно так и устроены.
Как я вам уже сказал, отличие llvm в том, что этот IR из него можно вытащить, а можно и запихать
обратно в текстовом виде. Заодно llvm включает в себя байткод-интерпретатор, который умеет этот IR (двоичный, не тесктовый!) исполнять и JIT.

Что касается asm printer и binary emitter, то чаще все-таки бывает, что target умеет -S, но не умеет сразу .o, чем наоборот.

То, что вы называете "состоянием" gcc - это тоже IR, и не важно, что его нельзя вытянуть из компилятора. Точнее, обычно IR таки можно достать из всех компиляторов - в двоичном виде.
(Все эти временные файлы, которые компиляторы могут производить - это он)
И обратно его потом можно засунуть. Но только в llvm к нему приделали текстовое представление.
Сравните clang -emit-llvm -S vs. clang -emit-llvm -c

> А здесь это именно язык llvm. Но совершенно нечеловекочитаемый, даром что похож.

Еще раз - этот "язык", а на самом деле сериализованный IR, не предназначен для чтения
людьми, а исключительно для писателей компиляторов. А для этих "нелюдей" исключительно удобно
- иметь возможность достать IR, покрутить его и запихнуть обратно. Или, например, regression
tests на нем писать.
Не знаю, что там такого ужасно нечитаемого в самом представлении как таковом.
Большая часть нечитаемости происходит из-за того как они variable renaming делают для SSA

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

42. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 06-Апр-19, 20:54 
перепись безграмотных "программистов" на опеннете...
Ответить | Правка | ^ к родителю #31 | Наверх | Cообщить модератору

46. "Новая криптографическая библиотека EverCrypt с математически..."  –2 +/
Сообщение от Sw00p aka Jerom (?), 06-Апр-19, 21:13 
отмазки одни, давай по делу
Ответить | Правка | ^ к родителю #42 | Наверх | Cообщить модератору

102. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от meantraitor (?), 08-Апр-19, 16:03 
Тут он все правильно сказал.
Я сначала смеялся, потом плакал, под конец уже кровавыми слезами.
Никто не в теме, а устроили срач с видом специалистов.
Ответить | Правка | ^ к родителю #46 | Наверх | Cообщить модератору

107. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 08-Апр-19, 20:16 
чаво он там правильного сказал? У него трансляция с одного исходного языка на другой исходный язык - называется компиляцией.
Ответить | Правка | ^ к родителю #102 | Наверх | Cообщить модератору

100. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от meantraitor (?), 08-Апр-19, 15:42 
> о, очередной "программист" самоучка? Компилятор с F на C - вполне себе компилятор, и код этот -
> компилированный. Что тебе бы рассказали на первом курсе института, если бы ты его посещал.

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

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

115. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от t_ (?), 09-Апр-19, 01:42 
Он тоже прав. :)
Просто он имеет в виду компилятор, внутри которого работает source-to-source транслятор.
Например, так:

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

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

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

19. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от KonstantinB (ok), 06-Апр-19, 15:22 
Полагаю, так сделано потому, что Apache 2.0 требует явного указания на то, какие файлы модифицированы - чтобы понимать, были ли внесены изменены в формальные спецификации доказательства.

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

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

37. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от X4asd (ok), 06-Апр-19, 19:38 
> Полагаю, так сделано потому, что Apache 2.0 требует явного указания на то, какие файлы модифицированы - чтобы понимать, были ли внесены изменены в формальные спецификации доказательства.

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

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

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

43. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от пох (?), 06-Апр-19, 20:58 
> а кому пришло бы в глову модифицировать НЕ исходный код

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

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

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

55. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от KonstantinB (ok), 07-Апр-19, 00:18 
> Что там у wireguard не смотрел, в виду его феерической ненужности

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

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

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

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

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

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

93. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от X4asd (ok), 08-Апр-19, 11:33 
>> а кому пришло бы в глову модифицировать НЕ исходный код
> Не всегда получается чужой исходник вот так, не модифицируя, встроить в свою сложную (и мутную) библиотеку.

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

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

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

110. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от пох (?), 08-Апр-19, 22:42 
> я же говорил про изменение НЕисходного кода

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

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

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

56. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от KonstantinB (ok), 07-Апр-19, 00:20 
> а кому пришло бы в глову модифицировать НЕ исходный код а получившийся скомпилированный вариант?

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

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

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

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

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

15. "Новая криптографическая библиотека EverCrypt с математически..."  –3 +/
Сообщение от кругомвраги (?), 06-Апр-19, 14:46 
>Процесс верификации сводится к определению подробных спецификаций...

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

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

32. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 06-Апр-19, 19:03 
в смысле неразглашаемая?
Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

61. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (60), 07-Апр-19, 07:21 
> в смысле неразглашаемая?

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

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

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

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

125. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от кругомвраги (?), 12-Апр-19, 21:04 
библиотека это по сути чёрный ящик причем для всех и даже авторов т.к. для знания и понимания работы нужно знать и программирование со всеми фишками и особенностями и криптографию чтоб врубаться и реализовывать её правильно.
нам предлагается набор спецификаций которым должен соответствовать ящик т.е. соответствие входа и выхода при определённых данных и действиях
но кто мешает добавить туда дополнительные спецификации? миллионыглаз бдящие код? не смешите.
к примеру вот ящик для секурного хранения записочек соответствует спецификации
положить записочку набрать код нажать принять, и набрать код нажать отдать и записочка вывалится.
но кто мешает разрабу добавить третью для майора - пнуть ногой ящик нажав обе кнопки - откроется ящик со всеми записочками.
вот про это я и говорю - вся криптография стоит на вере в честность разрабов.
Ответить | Правка | ^ к родителю #32 | Наверх | Cообщить модератору

126. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 13-Апр-19, 01:33 
> нам предлагается набор спецификаций которым должен соответствовать ящик

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

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

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

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

16. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от . (?), 06-Апр-19, 15:05 
> гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти

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

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

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

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

17. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от Аноним (17), 06-Апр-19, 15:11 
Напишите на массивах хотя бы парсер сертификатов X.509, а мы посмотрим.
Ответить | Правка | ^ к родителю #16 | Наверх | Cообщить модератору

20. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от . (?), 06-Апр-19, 15:36 
В сабжевой библиотеке этого тоже нет. Сам я со структурой сертификатов не разбирался, но ясно, что парсинг нужен только если она не статическая. В таких случаях используют дерево и следовательно работу с памятью, а парсить на массивах извращение.
Ответить | Правка | ^ к родителю #17 | Наверх | Cообщить модератору

38. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Ivan_83 (ok), 06-Апр-19, 19:42 
1. При такой передаче много лишнего копирования памяти.

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

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

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

53. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от . (?), 06-Апр-19, 23:46 
> Поскольку другой поточный шифр RC4, которые уже везде обьявили дырявым, то кроме чачи/сальсы ничего и нет.

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

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

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

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

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

59. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 02:32 
>Нет, так как криптография в софте легко разбивается на функции, изменяющие массив (или структуру) фиксированного размера.

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


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

72. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 14:57 
>Операция сложения используется, как единственный источник нелинейности.

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

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

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

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

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

80. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 18:18 
>Но у сложения есть ряд интересных свойств, которые как мне кажется позволяют полностью вскрыть шифры данной конструкции.

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

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

82. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от . (?), 07-Апр-19, 19:03 
Оригинальная чача, s-box'ов там нет.
https://github.com/odzhan/tinycrypt/blob/master/stream/chach...
Ответить | Правка | ^ к родителю #80 | Наверх | Cообщить модератору

84. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 20:00 
ChaCha State это и есть фактический S-box
Ответить | Правка | ^ к родителю #82 | Наверх | Cообщить модератору

85. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 07-Апр-19, 20:07 
добавлю, почему тогда эти начальные стейты в сальсе были одни, а в чачача ДЖБ их изменил?
Ответить | Правка | ^ к родителю #82 | Наверх | Cообщить модератору

91. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Ivan_83 (ok), 08-Апр-19, 00:21 
> добавлю, почему тогда эти начальные стейты в сальсе были одни, а в
> чачача ДЖБ их изменил?

Напиши ему и спроси.

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

97. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от товарищ майор (?), 08-Апр-19, 12:18 
наши коллеги из NSA очень попросили.

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

108. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 08-Апр-19, 20:18 
Так это как в случае со слабым S-box

Цитата из вики:

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

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

112. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от . (?), 08-Апр-19, 23:14 
S-box определяет вид нелинейного преобразования. У сальсы и чачи нелинейное преобразование одно и то же - сложение. Меняются константы, линейные преобразования (битовые сдвиги), а так же порядок применения сложения. То есть это разные шифры, но суть у них одна.

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

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

113. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Sw00p aka Jerom (?), 09-Апр-19, 00:48 
> По Шеннону для шифрования комбинируют рассеивание и запутывание.

"рассеивание и запутывание" - какие-то "упрощенные" определения, S-box - блок подстановок (замен) (нелинейные), P-box - блок перестановок (линейные). (SP-сеть, Сеть Фейстеля)

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

90. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Ivan_83 (ok), 08-Апр-19, 00:20 
> Согласен. Но все же создалось некоторое впечатление, что сместить пытаются не rc4,
> а именно aes.

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

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

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

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

104. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от meantraitor (?), 08-Апр-19, 16:21 
> Одномерный массив в си всегда передается как указатель

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

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

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

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

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

106. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от . (?), 08-Апр-19, 17:31 
> А двумерный? А десятимерный?

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

> extern int N;

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

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

62. "Новая криптографическая библиотека EverCrypt с математически..."  –1 +/
Сообщение от Аноним (60), 07-Апр-19, 07:24 
> 1. При такой передаче много лишнего копирования памяти.

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

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

63. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (60), 07-Апр-19, 07:50 
>> 1. При такой передаче много лишнего копирования памяти.
> Справедливо для C

Тут я ошибся.

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

103. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от meantraitor (?), 08-Апр-19, 16:16 
> 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];
}

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

22. "Новая криптографическая библиотека EverCrypt с математически..."  +1 +/
Сообщение от Аноним (22), 06-Апр-19, 16:25 
>доказательства надежности
>KreMLin

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

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

25. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (25), 06-Апр-19, 17:32 
>KreMLin

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

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

69. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Анонимс (?), 07-Апр-19, 14:38 
На этой, на этой. А так, как она в открытых исходниках, значит, скоро её соберут мантейнеры и включат во все дистрибутивы мира. Ну, вы теперь понимаете, кто самый могущественный в мире и кто может свергать и назначать президентов в любой стране.
Ответить | Правка | ^ к родителю #25 | Наверх | Cообщить модератору

44. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Аноним (-), 06-Апр-19, 21:06 
> Например, соответствие спецификации гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти.

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

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

54. "Новая криптографическая библиотека EverCrypt с математически..."  –2 +/
Сообщение от анонас (?), 07-Апр-19, 00:01 
Так я не понял, а Rust где?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

70. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Анонимс (?), 07-Апр-19, 14:41 
Так, как rust ещё молодой язык, то ещсложно
Ответить | Правка | ^ к родителю #54 | Наверх | Cообщить модератору

71. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от Анонимс (?), 07-Апр-19, 14:46 
сложно найти высококвалифицированных специалистов, особенно по криптографии.
Ответить | Правка | ^ к родителю #70 | Наверх | Cообщить модератору

122. "Новая криптографическая библиотека EverCrypt с математически..."  +/
Сообщение от getfr (?), 12-Апр-19, 00:59 
Математически доказать надежность этой программы, как подавляющего количества других невозможно. Даже если использовать теорию правильности программ
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

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

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




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

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