Tag: AWS Nitro System

AWS Nitro System のハイパーバイザー内で分離を実施する専用コンポーネント「AWS Nitro Isolation Engine」の一般提供を Graviton5 ベースのインスタンスで開始しました。形式的検証により、機密性と完全性、機能的正確性、ランタイムエラーの不在、メモリ安全性という 4 つの特性を数学的に証明し、形式的に検証された初のクラウドハイパーバイザーを実現します。Rust による実装や今後の展望も紹介します。

Amazon EC2 の新しい M9g/M9gd インスタンスとともに一般提供が始まった Nitro Isolation Engine は、商用クラウド環境にデプロイされた初の形式的検証済みハイパーバイザーの重要なコンポーネントで、その唯一の役割は仮想マシン (VM) を相互に分離することです。本記事では、Isabelle/HOL 定理証明支援系を用い、機械的に検証された 330,000 行の数学的記述によって VM 間の分離を証明した手法を解説します。μRust と分離論理による機能検証、非干渉性に基づく機密性と完全性の証明を紹介します。

Amazon Web Services (AWS) は、定理証明支援系 Isabelle/HOL を用いて Nitro Isolation Engine (NIE) の正当性とセキュリティ保証を検証し、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。本記事では、ブール論理から一階述語論理、高階論理、依存型理論に至る数理論理の言語階層を解説し、Isabelle/HOL が備える数学的な記述の表現力、自動化、スケーラビリティのバランスや、sledgehammer やロケールなどの主要機能、seL4 や CRDT などの応用事例を紹介します。

AWSが「Digital Sovereignty Pledge」を公表した際、私たちはAWSのサービスがどのように設計・運用されているか、特に顧客データの取り扱いに関して、より高い透明性と確証を顧客に提供することを約束しました。その透明性向上の一環として、英国に拠点を置く大手サイバーセキュリティコンサルティング会社であるNCC Groupに、Nitro Systemと当社がお客様に提供するセキュリティ保証に関する独立したアーキテクチャレビューを実施するよう依頼しました。このたび、NCCから報告書が発行され、当社の主張を裏付ける評価が提示されました。

ソリューションアーキテクトの松尾です。2021年10月14日に「Amazon EC2 大活用 ~ 最新ラインナ […]

政府機関や規制の厳しい業界から、中小企業、ベンチャー企業まで、世界中のお客様が Amazon Web Serv […]