EasyCrypt -- теорем-прувер, фактически небольшой интерактивный фреймворк со своим языком, для формальной верификации криптографических протоколов, которые представляются в виде императивных программ. Большой плюс, что интегрируется с Coq.
It has four built-in logics:
- a probabilistic, relational Hoare logic (pRHL);
- a probabilistic Hoare logic (pHL);
- an ordinary (possibilistic) Hoare logic (HL);
- an ambient higher-order logic for proving general mathematical facts and connecting judgments in the other logics.
Какие минусы в сравнении с моим подходом:
-- В HoTT равенство -- это гомотопия (путь между типами), что позволяет легко и просто формализовать инвариантность и эквивалентность структур (хотим доказать, что два протокола (реализации) "эквивалентны" в смысле безопасности).
Например, в EasyCrypt доказательство того, что
a+b=b+a для целых чисел, требует явного аксиоматического подхода. А в HoTT это следует из свойств абелевых групп (коммутативность встроена в структуру).-- EasyCrypt требует явного моделирования условий безопасности (например, случайных оракулов или свойств конфиденциальности).
HoTT позволяет инкапсулировать эти условия в зависимые типы: можно определить тип SecureProtocol, который автоматически требует доказательства свойств безопасности.
Например,
HomotopyGroup(Protocol, 1) ≡ 0 для первой гомотопической группы.-- EasyCrypt работает с конкретными алгоритмами и их реализациями.
HoTT позволяет моделировать абстрактные математические структуры (группы, кольца, категории...), которые есть самая база криптографии, что упрощает доказательства теорем о безопасности, основанных на алгебраических свойствах.
Например, классы LoopSpace и HomotopyGroup могут быть использованы для анализа топологических свойств криптографических протоколов (устойчивость к циклическим атакам, ...).
-- EasyCrypt требует раздельного доказательства логических и математических утверждений. HoTT объединяет это всё в единую систему, где математические доказательства (например, теоремы из теории чисел) и логические рассуждения о программах происходят в одном и том же формальном фреймворке, что стирает сложности перехода между уровнями абстракции.
=
Конечно, в прикладном смысле сравниваться смысла нету, потому что, в частности, необходимы прежде всего криптографические примитивы (например, хэш-функциии, случайные оракулы, DLP...). Но я могу их формально описать буквально за неделю, и никакой специальной интеграции не требуется, потому что у меня по сути просто чистый питонячий код и одна библиотечка.
И тут кстати большой вопрос, а насколько эти сервисы сами верифицированы в плане своей реализации? :) А если там программный баг, или ошибка в логике?
У меня по крайней мере логическая реализация HoTT проверяется тестами и стандартным чек-листом просто по "Homotopy Type Theory: Univalent Foundations of Mathematics". А возможно кстати, сделаю формальную верификацию и моей реализации, в качестве хорошего примера.
(Размышления письмом завтра продолжу, ещё парочку фреймворков разберу, чтобы как следует эту темку продумать)