Система «Fiat Cryptography» MIT автоматизирует процесс обеспечения безопасности почти всего

  • HLCS 

Источник · Перевод автора

Лаборатория компьютерных наук и искусственного интеллекта (Computer Science and Artificial Intelligence Laboratory, CSAIL) в MIT разработала систему для запуска сложных математических алгоритмов для обеспечения безопасности онлайн-коммуникации. «Fiat Cryptography», как называется код, в настоящее время обеспечивает около 90 процентов коммуникаций Google Chrome.

Исследователи представили свой доклад (http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf) на симпозиуме EEE по безопасности и конфиденциальности в мае, хотя эта технология была первоначально теоретизирована и развернута в лабораториях MIT в 2018 году.

«Fiat Cryptography» предназначена для автоматической генерации и одновременной проверки оптимизированных криптографических алгоритмов для всех аппаратных платформ, процесс, который раньше выполнялся вручную.

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

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

Исследователи сначала искали решение на языках программирования C и ассемблера и перенесли эти методы в свою библиотеку кода — список самых эффективных алгоритмов для каждой архитектуры.

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

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

«По сути, это все равно, что взять процесс, который работает в человеческом мозге, и понять его достаточно хорошо, чтобы написать код, имитирующий этот процесс», — сказал Адам Чипала (Adam Chlipala), исследователь CSAIL, работавший над проектом, в интервью MIT News.

С тех пор «Fiat Cryptography» была развернута Google BoringSSL, криптографической библиотекой с открытым исходным кодом, используемой Google Chrome, приложениями Android и другими программами.

К Чипале присоединились аспиранты CSAIL Андрес Эрбсен (Andres Erbsen) в качестве первого автора, Джейд Филипум (Jade Philipoom) и Джейсон Гросс (Jason Gross) в качестве соавторов, а также Роберт Слоан (Robert Sloan), аспирант инженерного факультета.

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