Tag: Security Blog

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 などの応用事例を紹介します。

Amazon GuardDuty 調査エージェントのパブリックプレビューを発表しました。AI を活用してセキュリティ検出結果の調査を自動化し、調査時間を数時間から数分に短縮します。リスクレベル、信頼度スコア、MITRE ATT&CK 手法マッピング、推奨アクションを含む構造化された評価を提供します。本記事では、コンソールと AWS CLI による有効化と調査の実行手順、AWS MCP サーバーとの統合、AWS Security Incident Response との使い分けを解説します。

AWS Security Hub の 2 つの大きな拡張を発表します。マルチクラウドセキュリティ管理の対象を Microsoft Azure に拡大し、Azure の検出結果を AWS と統合して優先順位付けできるようになりました。さらに GuardDuty AI Protection による Amazon Bedrock や SageMaker の脅威検出、GuardDuty AI-powered investigations による調査の自動化、Security Hub AI inventory による AI 資産の可視化など、AI ワークロード保護の新機能も紹介します。

本記事では、Amazon Bedrock のデータ保持モード (none、default、inherit、provider_data_share) の仕組みと、設定したモードが保持の上限として機能する動作を解説します。Amazon Bedrock Projects による保持要件が異なるワークロードの分離、サービスコントロールポリシー (SCP) を使用して組織全体でモデルプロバイダーとのデータ共有を防止しゼロデータ保持を強制する方法、クロスリージョン推論プロファイルとの相互作用、AWS CLI や API による設定の検証手順を紹介します。

Amazon Bedrock で Anthropic の Claude Fable 5 モデルが、悪用防止のためのさらに強力なガードレールを備えて再びご利用いただけるようになりました。本記事では、サイバー能力を持つフロンティアモデルを防御側に届けながら攻撃者による悪用を防ぐバランスの取り方、Project Glasswing を通じた Anthropic との連携、問題の重大度と対応の SLA など、フロンティアモデルを安全にお客様へ提供するための AWS の取り組みを紹介します。

本ブログでは、企業が規制コンプライアンスのためにコンソールアクセスを企業ネットワークに制限するユースケースを取り上げ、AWS Sign-In のリソースベースポリシーと RCP を使った実装方法を紹介します。リソース許可ステートメントの作成、コンソール認可の有効化、CloudTrail による検証、Console Private Access やデータ境界フレームワークとの統合まで詳しく説明します。

TLS エンドポイントをポスト量子暗号 (PQC) に移行する第一歩は、現状のインベントリと状態把握です。本記事では、ALB、NLB、Amazon API Gateway のエンドポイントを継続的に監視する PQC Readiness Scanner を紹介します。AWS Config コンフォーマンスパックを活用し、各エンドポイントを 3 階層フレームワークに分類して移行の優先順位付けを自動化する方法を、シングルアカウントおよび Organizations でのデプロイ手順とあわせて解説します。

コードの脆弱性に対応する AWS Continuum を発表します。テレメトリ収集とダッシュボード監視に頼る従来の運用モデルから、テレメトリ、コンテキスト、推論、アクションへと至る新しいアプローチへ移行します。フロンティアモデルを活用し、発見、優先順位付け、検証、緩和と修復という 4 つの継続的フェーズで、コードの脆弱性のライフサイクル全体にマシンスピードで対応する仕組みを紹介します。