Доказуемая безопасность

Обеспечение безопасности с математическим подтверждением

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

Возможности доказуемой безопасности
Ресурсы доказуемой безопасности
Что такое автоматизированное построение логических рассуждений? (2:56)

Как это работает

Мы применяем автоматизированное построение логических рассуждений в ключевых областях обслуживания, таких как хранение данных, сетевые технологии, виртуализация, идентификация и криптография. Вы можете увидеть автоматизированное построение логических рассуждений в работе в Amazon CodeGuru, Простом сервисе хранения данных Amazon (Amazon S3), Управлении идентификацией и доступом AWS (IAM), Анализаторе доступа к сети Amazon VPC, Анализаторе достижимости Amazon VPC и Проверенных разрешениях Amazon.
  • Amazon CodeGuru

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

  • Блокирование публичного доступа к Amazon S3

  • Блокирование публичного доступа к S3 использует автоматизированное построение логических рассуждений для обеспечения контроля на уровне всего аккаунта AWS или на уровне отдельных корзин S3, чтобы гарантировать, что объекты никогда не будут иметь публичного доступа, ни сейчас, ни в будущем.

  • IAM Access Analyzer

  • Средство анализа доступа AWS Identity and Access Management (IAM) использует автоматизированное построение логических рассуждений для анализа всех путей доступа к вашим ресурсам, как публичных, так и доступа между несколькими аккаунтами, и предоставляет всесторонний анализ этих путей.

  • Amazon VPC Network Access Analyzer

  • Network Access Analyzer использует автоматизированное построение логических рассуждений для определения достижимых путей и проверки инвариантов безопасности в вашей сети AWS.

  • Анализатор достижимости Amazon VPC

  • Анализатор достижимости использует автоматизированное построение логических рассуждений для определения допустимых путей и объяснения недостижимых путей в вашей сети AWS.

  • Проверенные разрешения Amazon

  • Сервис «Проверенные разрешения Amazon» использует автоматическое обоснование, чтобы определять высокоточные разрешения для пользователей приложений.

Исследования и аналитические данные

Миллиард SMT-запросов в день

В этом ключевом докладе конференции Computer-Aided Verification (CAV) Неха Рунгта, директор по прикладным наукам AWS Identity, рассказывает о том, как AWS делает возможности автоматизированного построения логических рассуждений доступными для всех своих клиентов.

Вас интересует возможность стажировки в группе AWS по автоматизации логических рассуждений?

Хотите найти решение для самых сложных проблем безопасности в облаке?

Сообщите нам!

Подробнее об AWS