За 10 лет существования группы Automated Reasoning (ARG) Amazon довела формальную верификацию до рабочих AWS-сервисов. Один из самых заметных результатов — доказанная корректность нового движка авторизации, который обрабатывает 1 миллиард API-вызовов в секунду.
История группы и её влияние
В 2016 году на базе Amazon была основана группа ARG, целью которой стало использование математической логики для проверки корректности систем. На протяжении десятилетия исследователи работали над тем, чтобы не просто тестировать, а и формально доказывать работу AWS-систем, обеспечив их безопасность на уровне критически важных услуг.
С момента своего создания ARG разработала несколько инструментов, таких как Tiros и Zelkova, которые стали основой для различных сервисов, включая Amazon Inspector и IAM Access Analyzer. Эти инструменты обеспечивают анализ безопасности и соответствие требованиям для множества приложений в экосистеме AWS.
Технологические достижения
С помощью Tiros, инструмента для анализа сетевой безопасности, стало возможным выявление ошибочных конфигураций и уязвимостей в виртуальных частных облаках. В 2022 году его функциональность была интегрирована в Amazon Inspector, что позволило миллионам пользователей повысить уровень защиты своих облачных приложений.
Zelkova, в свою очередь, позволяет проверять политики AWS на соответствие требованиям безопасности, что укрепляет доверие пользователей к платформе. Оба инструмента доказали свою эффективность и стали образцами для подражания в индустрии.
Что все это значит для разработчиков и компаний
Для разработчиков и бизнеса это критически важный шаг. Математические гарантии безопасности служат обоснованием для более широкого применения AWS среди крупных клиентов и стартапов, стремящихся к надежности и соответствию стандартам. Теперь компании могут уверенно разрабатывать решения с минимальным риском ошибок и уязвимостей.
Следующим шагом для Amazon станет расширение применения формальной верификации в ИИ-инструментах: компания уже использует эти подходы в Bedrock Guardrails, AgentCore и Kiro. Это означает, что в будущем мы можем ожидать появления еще более надежных решений в экосистеме AWS.