可证明的安全性

有数学验证支持的安全保障

AWS 致力于帮助您实现最高的云安全性。借助自动推理技术,亦即运用数学逻辑来帮助回答有关基础设施的关键问题,AWS 能够检测可能潜在暴露脆弱数据的各类配置错误。我们将此称之为可证明的安全性,它为云本身和云中的安全性都提供了更高的保障。

下面介绍了有关当今和未来的关键云安全性挑战的最新研究和见解。

什么是自动推理?

研究与见解

对来自 AWS 数据中心的启动代码进行模型检查
数据中心安全是云中安全性的根本组成部分一。此洞察报告描述了我们为了提供可证明的启动代码安全性而采取的步骤,这是确保任何数据中心的安全的一个关键环节。

证明加密系统的时间平衡
AWS 高度重视您的数据安全性和完整性,因此我们开发了 SideTrail,这是一种程序分析工具,它可以运用数学方法来验证密码中的防伪措施的正确性。阅读此洞察报告以了解更多。

可证明的大规模资源策略安全性
正确配置的策略是组织安全状况的关键组成部分之一。策略配置不当也是云客户最为关心的安全问题之一。此洞察报告深入分析了 Zelkova 策略分析引擎,它可以自动检测各种类别的资源配置错误。

AMAZON S2N 的持续形式化验证
我们介绍了 s2n 的形式化验证,这是许多 Amazon 服务中使用的开源 TLS 实现。这种验证基础设施的一个关键要素是通过持续检查来确保相关属性在整个软件生命周期保持有效。每次更改代码时都将自动重新建立验证程序,极少甚至不需要开发人员作出任何干预。我们将介绍此验证本身以及促使在开发过程中集成此验证的技术决策。

对基于 AWS 的网络的可访问性分析
在此工业级的案例研究中,我们介绍了一种新的网络可访问性推理工具 Tiros,它使用现成的自动化定理证明工具来识别网络配置错误或安全漏洞。Tiros 是 Amazon Inspector 服务中最近推出的一项网络安全分析功能的基础,现已向数百万在云中构建应用程序的客户开放。在 AWS 中,Tiros 还用于为利用现有 AWS 联网功能构建的许多 AWS 服务自动化执行合规验证并遵守安全常量。

关于 AWS 的形式化推理
了解 Amazon Web Services 中的自动推理工具和方法如何为云提供最高级别的安全保障。此外,我们还谈论了潜在的未来研究和应用领域。

对象导向的安全验证
此洞察报告简要介绍了 AWS 安全专家用于证明系统正确性的方法。

用于生成测试输入的求解器辅助语言
开发小巧但有用的测试输入集绝非易事。我们的案例证明,一种以常量求解器支持的域特定语言可以帮助编程人员完成此工作。这种求解器可以生成测试输入集并保证每个输入都不同于其他输入,这种方法对于测试十分有用。

有关 JAVA 8 函数式编程功能的实用推理方法
我们介绍了 Java 建模语言和 OpenJML 推理程序验证工具的新增功能,这些新增功能用于支持 Java 8 中推出的函数式编程功能。我们还报告了 Amazon Web Services 开发的安全流协议库的扩展应用,这种流协议库是我们所提供服务的基础。

视频

AWS re:Invent 2019:可证明的访问控制 – 了解谁可以访问您的 AWS 资源

了解 AWS 自动推理技术的演变以及它在其嵌入的服务中的运作方式。

AWS re:Invent 2019:深入探究 IAM 访问分析器

深入探究这项面向安全团队和管理员的新功能,以验证资源策略仅提供预期的公共访问和跨账户访问。

AWS re:Invent 2019:领导力研讨会 – AWS 安全性

Stephen Schmidt 和 Neha Rungta 讨论了云安全性、身份和合规性的当前状态,并分享了 AWS 安全性最新资讯。 

AWS re:Inforce 2019 大会:AWS 自动推理技术的演变

Eric Brandwine 和 Neha Rungta 介绍了 AWS 的自动推理技术的演变历程,以及它嵌入 Amazon S3、AWS Config 和 Amazon Macie 等服务后的工作原理。

AWS re:Inforce 2019 大会:采用可证明的安全性的 AWS 方法实现更高标准的保障

Byron Cook 介绍了 AWS 的可证明的安全性计划,这是一组自动推理技术的总称,可帮助证明云中和云本身的关键安全性组件的正确性。 

AWS re:Inforce 2019:使用可证明的安全性在 AWS 上自动进行合规性验证

了解 AWS 可证明的安全性计划如何运用自动推理技术来自动证明客户的云环境符合特定的监管标准。

桥水基金在纽约的 AWS 技术峰会上介绍了 ARG 工具的使用

了解全世界最大的对冲基金桥水基金如何开发一种自动推理流程,用于分析安全策略并在自动化的控制验证和响应系统中运用。

AWS re:Invent 2018 大会:借助 AWS 大规模进行策略验证和执行

与负责管理基础设施即代码 (IaC) 的开发人员一起,了解高盛如何使用分布式的无服务器日志记录管道并利用 AWS 自动推理工具来帮助在流程中强制执行访问策略。 

AWS re:Invent 2018 大会:数据隐私和安全性背后的理论与数学

数据隐私和安全性是云客户最为关心的领域之一。在此会议中,AWS 自动推理小组分享了根源于数学验证的先进技术,这种技术可在当今数据驱动的世界里帮助提供最高的安全性。

LogMeIn 如何实现大规模的监管自动化并支持开发人员

了解 LogMeIn 如何快速迁移到 AWS 并借助 AWS 上的自动化优势保持安全性。我们介绍了 IAM、AWS CloudTrail、AWS Config 和 Amazon CloudWatch 等核心的 AWS 安全产品。 

什么是 AWS Zelkova?

了解有关 AWS Zelkova 的更多信息,此工具是 AWS 可证明的安全性计划的组成部分。Zelkova 是一种 IAM 数据监管工具,它嵌入在多种 AWS 服务中,可帮助评估 IAM 策略及其行为。

AWS 服务团队如何使用自动推理功能实现安全性

AWS 安全性自动推理小组的 Neha 介绍了她的团队如何为 AWS Config 和 Amazon Macie 构建新的自动推理规则。 

有关 Amazon Web Services 安全性的形式化推理

2018 年 7 月 16 日联合逻辑大会 (Federated Logic Conference) 上的全会讲座

AWS re:Invent 2017 大会:AWS CISO Steve Schmidt 介绍 Zelkova

AWS CISO 兼安全副总裁 Steve Schmidt 介绍了形式化/基于约束的工具的开发以及在 AWS 中的使用。

希望到 AWS 自动推理小组实习?

希望解决最具挑战性的一些云安全问题?

联系 AWS 业务代表
有问题? 联系 AWS 业务代表
探讨安全角色?
立即申请 »
想了解 AWS 安全性动态?
在 Twitter 上关注我们 »