http://www.xakep.ru/post/62429/

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

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

Раньше Cryptol выпускалась с закрытыми исходниками, но сейчас вышла вторая версия программы с открытым кодом под 3-пунктовой лицензией BSD. Разработчики говорят, что написание этой программы заняло примерно 20 человеко-лет, так что публикация исходников — существенная жертва в пользу человечества.