Исходное сообщение
"Новая криптографическая библиотека EverCrypt с математически..." Отправлено ., 06-Апр-19 15:05
> гарантирует безопасную работу с памятью и отсутствие ошибок, приводящих к переполнению буфера, разыменованию указателей, обращению к уже освобождённым областям памяти или двойному освобождению блоков памяти Все эти ошибки возникают при динамической работе с памятью или при зависимости логики от внешних данных. Крипту ничто не мешает писать на массивах, выходы за границы которых отлавливаются статическим анализатором. Тогда, если тесты успешны программа иначе себя вести не может. Пример: void encrypt(uint64_t block[4], uint64_t rk[120]); С другой стороны в библиотеках обычно дают на выбор несколько алгоритмов, каждый из который имеет варианты реализации в зависимости платформы (endianness, разрядность, аппаратное ускорение, особенности ОС). Поэтому подход с формальной верификацией имеет смысл, но это компромисс который обычного пользователя в общем-то не касается. Вот шифр чача на мой взгляд слишком активно сейчас проталкивают. Он конечно быстрее и в чем-то лучше аес, но сдается, что его уже могут скажем так анализировать.