可證明的安全性

經過數學論證的安全保證

AWS 致力於協助您實現雲端中最高級別的安全性。透過使用自動推理技術,以及運用數學邏輯來協助解答有關基礎架構的關鍵問題,AWS 能夠偵測可能會暴露易受攻擊資料的所有錯誤設定類別。我們將這稱為可證明的安全性,這為雲端安全性以及在雲端提供了更高級別的保證。

下面提供了有關當今及未來關鍵雲端安全挑戰的最新研究和洞見。

什麼是自動推理?

研究與洞見

AWS 資料中心的模型檢查啟動程式碼
資料中心安全性是雲端中安全性的基本組成部份。這份洞見白皮書說明了我們為提供可證明的啟動程式碼安全性而採取的步驟,這是建立任何資料中心安全性的關鍵步驟。

提供密碼系統的時間平衡
在 AWS,資料的安全性和完整性是我們的首要任務,因此我們開發了 SideTrail,這是一種程式分析工具,可透過數學方式驗證密碼中對策的正確性。在此洞見白皮書中了解詳細資訊。

大規模資源政策可證明的安全性
正確設定的政策是組織安全狀況的重要組成部份。政策設定錯誤是雲端客戶主要的安全問題之一。此洞見白皮書將深入探討 Zelkova,這是一個政策分析引擎,可以自動偵測整個資源設定錯誤類別。

AMAZON S2N 的連續形式驗證
我們說明了 s2n 的形式驗證,s2n 是眾多 Amazon 服務中使用的開放原始碼 TLS 實作。驗證基礎架構的一個關鍵方面是連續檢查,可確保在軟體的生命週期內其效能仍能得到驗證。每次變更程式碼時,都會自動重建驗證,而開發人員幾乎不需要互動。我們說明了驗證本身以及能夠整合至開發中的技術決策。

AWS 型網絡連線性分析
在此工業案例研究中,我們說明了一種稱為 Tiros 的新網路連線性推理工具,該工具使用現成的自動定理驗證工具,來識別安全漏洞的網路錯誤設定。Tiros 是 Amazon Inspector 服務中最近引入的網路安全分析功能的基礎,現已可供數百萬在雲端建置應用程式的客戶使用。Tiros 也可以在 AWS 中使用,以便針對基於現有 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 Access Analyzer

針對安全團隊和管理員深入研究此新功能,驗證資源政策僅提供預期的公用和跨帳戶存取。

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 Provable Security 計劃如何運用自動推理技術,來自動驗證客戶的雲端環境符合特定法規標準。

AWS 自動推理小組的工作原理

我們與 AWS 自動推理小組的工程師和研究人員進行了交談,並了解到他們有關團隊合作的喜好。看看這個團隊正在進行的相關專案,以協助客戶實現可證明的雲端安全性!

Bridgewater Associates 在紐約 AWS 峰會上討論了 ARG 工具的使用

了解全球最大的對沖基金 Bridgewater Associates 如何開發自動推理程序,以分析安全性政策,並在自動化控制驗證和回應系統中實作這些政策。

AWS re:Invent 2018︰使用 AWS 進行大規模政策驗證和執行

與管理基礎架構即程式碼 (IaC) 的開發人員一起,了解 Goldman Sachs 如何使用分散式無伺服器日誌記錄管道,以及利用 AWS 自動推理工具來協助在程序中執行存取政策。 

AWS re:Invent 2018︰資料隱私權和安全背後的理論和數學

資料隱私權和安全性是雲端客戶的首要考量。在此專題講座中,AWS 自動推理小組分享了源於數學論證的進階技術,可在當今資料驅動的世界中提供最高層級的安全保證。

LogMeIn 如何大規模自動執行管控並為開發人員提供支援

了解 LogMeIn 如何透過 AWS 上的自動化功能快速移動並保持安全。我們逐步介紹了 AWS 的核心安全建置區塊,例如 IAM、AWS CloudTrail、AWS Config 和 Amazon CloudWatch。 

什麼是 AWS Zelkova?

進一步了解有關 AWS Zelkova 的資訊,該工具是 AWS 可證明的安全性計劃的一部份。Zelkova 是一種 IAM 資料管控工具,嵌入在各種 AWS 服務中,可協助評估 IAM 政策及其行為。

AWS 服務團隊如何使用自動推理來實現安全性

AWS 安全自動推理小組的 Neha 闡述了她的團隊如何為 AWS Config 和 Amazon Macie 建立新的自動推理規則。 

關於 Amazon Web Services 安全性的形式推理

2018 年 7 月 16 日聯邦邏輯會議上的大會演講

AWS re:Invent 2017︰AWS CISO Steve Schmidt 談論 Zelkova

AWS CISO 和安全副總裁 Steve Schmidt 討論 AWS 中形式/約束型工具的開發和使用。

有興趣在 AWS 自動推理小組實習?

想要解決某些最具挑戰性的雲端安全性問題?

聯絡 AWS 業務代表
有問題? 聯絡 AWS 業務代表
探索安全職缺?
立即申請 »
需要 AWS 安全更新?
在 Twitter 上關注我們 »