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

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

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

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

Что такое автоматизация логических рассуждений?

Последние статьи и публикации в блогах

НОВОЕ IAM ACCESS ANALYZER

IAM Access Analyzer анализирует с математической точки зрения политики контроля доступа, назначенные для ресурсов, и определяет, какие ресурсы находятся в открытом доступе или доступны из других аккаунтов. С помощью IAM Access Analyzer вы можете наглядно представить совокупное влияние элементов управления доступом, чтобы убедиться, что ваши ресурсы защищены от несанкционированного доступа за пределами вашего аккаунта. Эта первая в своем роде возможность доступна бесплатно. Перейдите на страницу сервиса AWS IAM и включите IAM Access Analyzer уже сегодня.

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

MODEL CHECKING BOOT CODE FROM AWS DATA CENTERS
Безопасность центра обработки данных – основной компонент безопасности в облаке. В этом аналитическом документе описаны наши действия по обеспечению доказуемой безопасности загрузочного кода, который имеет важное значение при установлении безопасности любого центра обработки данных.

PROVING TIME-BALANCING OF CRYPTO SYSTEMS
Безопасность и целостность ваших данных в AWS – наш главный приоритет, поэтому мы разработали SideTrail, программный аналитический инструмент, который с математической точки зрения проверяет правильность мер защиты в криптографическом коде. Дополнительные сведения см. в этом аналитическом документе.

PROVABLE SECURITY OF RESOURCE POLICIES, AT SCALE
Правильно настроенная политика играет важную роль в безопасности организации. Неправильная конфигурация политики – одна из основных проблем безопасности пользователей облака. В этом аналитическом документе подробно изложены принципы работы Zelkova, механизма анализа политик, который может автоматически определить целые классы ошибок в конфигурации ресурсов.

CONTINUOUS FORMAL VERIFICATION OF AMAZON S2N
Мы описываем формальную проверку s2n, версии TLS с открытым исходным кодом, которая используется во многих сервисах Amazon. Ключевой аспект такой безопасной инфраструктуры – непрерывные проверки для подтверждения свойств на протяжении всего жизненного цикла программного обеспечения. При каждом изменении кода подтверждение происходит автоматически при минимальном взаимодействии с разработчиком или вовсе без него. Мы описываем само подтверждение и технические решения, позволившие интегрировать его в разработку.

REACHABILITY ANALYSIS FOR AWS-BASED NETWORKS
В этом промышленном примере использования мы описываем новый инструмент логических рассуждений о сетевой доступности под названием Tiros, который использует готовые автоматизированные средства доказательства теорем для определения ошибок в конфигурации сети, способствующих возникновению уязвимостей безопасности. Tiros лежит в основе недавно представленного компонента анализа сетевой безопасности в сервисе Amazon Inspector, который теперь доступен для миллионов пользователей, создающих приложения в облаке. Кроме того, Tiros используется в AWS для автоматизации соответствия требованиям и соблюдения постоянной безопасности во многих сервисах AWS, разработанных на основе существующих сетевых возможностей AWS.

FORMAL REASONING ABOUT AWS
Узнайте, как инструменты и методы автоматизации логических рассуждений в Amazon Web Services обеспечивают самый высокий уровень безопасности в облаке. Кроме того, мы обсуждаем потенциальные перспективы исследований и разработки приложений в будущем.

OBJECT-ORIENTED SECURITY PROOFS
В этом аналитическом документе описана история появления методики, которую специалисты AWS по безопасности использовали, чтобы доказать правильность систем.

A SOLVER-AIDED LANGUAGE FOR TEST INPUT GENERATION
Разработать небольшой, но полезный набор входящих данных для тестирования непросто. Мы покажем, как специализированный язык при поддержке решателя задач удовлетворения ограничений помогают программистам в этом процессе. Решатель может сгенерировать набор тестовых входящих данных и гарантировать их полезное для тестирования отличие между собой.

PRACTICAL METHODS FOR REASONING ABOUT JAVA 8’s FUNCTIONAL PROGRAMMING FEATURES
Мы описываем новые возможности, добавленные в язык моделирования Java и дедуктивный инструмент проверки программ OpenJML для поддержки функциональных возможностей программирования, представленных в Java 8. Кроме того, мы рассказываем о применении расширений к библиотеке протоколов безопасной потоковой передачи данных, разработанной Amazon Web Services и используемой в качестве основы для предоставляемых сервисов.

Видео

AWS re:Invent 2019. Provable access control – Know who can access your AWS resources

Узнайте о развитии технологий автоматического обоснования в AWS и о том, как это работает в сервисах, где такие технологии являются встроенными.

AWS re:Invent 2019. Deep Dive into IAM Access Analyzer

Узнайте подробнее о новой возможности для специалистов по безопасности и администраторов: она позволяет проверять политики ресурсов на предмет предоставления только намеренного публичного доступа или доступа для других аккаунтов.

AWS re:Invent 2019. Leadership Session – AWS Security

Стивен Шмидт и Неха Рунгта рассказывают о текущей ситуации в сфере обеспечения безопасности, идентификации и соответствия требованиям в облаке, а также о новостях AWS Security. 

AWS re:Inforce 2019: The Evolution of Automated Reasoning Technology at AWS

Эрик Брандвайн и Неха Рунгта обсуждают эволюцию технологии автоматизации логических рассуждений в AWS и принцип ее работы в сервисах, в которые она встроена, в том числе Amazon S3, AWS Config и Amazon Macie.

AWS re:Inforce 2019: An AWS Approach to Higher Standards of Assurance w/ Provable Security

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

AWS re:Inforce 2019: Automate Compliance Verification on AWS Using Provable Security

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

Представитель компании Bridgewater Associates рассказывает об использовании инструментов ARG на встрече AWS Summit в Нью-Йорке

Узнайте, как специалисты компании Bridgewater Associates, крупнейшего в мире хедж-фонда, разработали процесс автоматизации логических рассуждений, который анализирует политики безопасности и внедряет их в автоматизированные системы проверки средств контроля и необходимого реагирования.

AWS re:Invent 2018: Policy Verification and Enforcement at Scale with AWS

Узнайте, как компания Goldman Sachs использует распределенные бессерверные конвейеры ведения журналов и инструменты автоматизации логических рассуждений AWS для применения политики доступа, а разработчики управляют инфраструктурой как кодом (Infrastructure as Code, IaC). 

AWS re:Invent 2018: The Theory and Math Behind Data Privacy and Security

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

How LogMeIn Automates Governance and Empowers Developers at Scale

Узнайте, как компании LogMeIn удается быстро развиваться и обеспечивать безопасность, используя средства автоматизации в AWS. Мы рассмотрим все основные компоненты безопасности AWS, такие как IAM, AWS CloudTrail, AWS Config и Amazon CloudWatch. 

Что такое AWS Zelkova?

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

How AWS service teams use Automated Reasoning for security

Неха из группы по автоматизации логических рассуждений для обеспечения безопасности AWS рассказывает о том, как ее команда создала новые правила автоматизации логических рассуждений для AWS Config и Amazon Macie. 

Formal reasoning about the security of Amazon Web Services

Пленарная лекция во время конференции Federated Logic Conference, 16 июля 2018 г.

AWS re:Invent 2017: директор AWS по информационной безопасности Стив Шмидт рассказывает о Zelkova

Директор AWS по информационной безопасности и вице-президент по безопасности Стив Шмидт рассказывает о разработке и использовании формальных и основанных на ограничениях инструментах в AWS.

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

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

Связаться с представителем AWS
Есть вопросы? Связаться с представителем AWS
Ищете работу в сфере обеспечения безопасности?
Предложите свою кандидатуру прямо сегодня »
Хотите получать новости по безопасности AWS?
Следите за новостями в Twitter »