Max Home IndustryВыпущена версия Cryptol с открытым исходным кодом. Язык разработан специально для криптографии, и хотя это первая общедоступная версия, язык находится в стадии разработки и используется уже почти 15 лет.
Cryptol был первоначально разработан Галуа для Агентства национальной безопасности США, но он также используется частными компаниями.
Написав о новом выпуске в блоге компании, команда отмечает, что Cryptol помогает разработчикам обнаруживать (или избегать) ошибок корректности в криптографическом коде. Они говорят, что Cryptol сокращает разрыв между эталонной спецификацией криптографического алгоритма и исполняемой версией, которую можно использовать для тестирования и проверки.
Проблема со многими криптографическими алгоритмами заключается в том, что они написаны в научных статьях в математической нотации, которая не является исполняемой. Затем она преобразуется в «эталонную реализацию», которая отличается от математической, и эта эталонная реализация затем используется в приложениях, но не было простого способа проверить точность эталонной реализации по математической спецификации.
Cryptol — это предметно-ориентированный язык для определения криптографических алгоритмов. По словам создателей, реализация алгоритма Cryptol больше похожа на свою математическую спецификацию, чем реализация на языке общего назначения.
Используя спецификацию в Cryptol, программисты могут генерировать свои собственные тестовые векторы, доказывать теоремы и (используя другие инструменты) проверять эквивалентность своим собственным программам или генерировать код или оборудование из спецификации.
Разработчики говорят, что Cryptol — это мощный инструмент для использования возможностей решателей SMT, таких как Yices, Z3 и CVC4. Версия с открытым исходным кодом размещена на GitHub. Если вы хотите увидеть диапазон возможных применений, загрузка включает в себя папку funstuff с решениями головоломок, таких как судоку, закодированными в Cryptol, которые затем можно решить с помощью команды: sat.