Amazon Web Services ブログ

Category: Amazon EC2

Kubernetes と Agones から Amazon GameLift Servers への移行

Kubernetes 上で動作する Agones は専用ゲームサーバーのホスティングによく使われますが、グローバル規模になると運用が複雑になります。本記事では、運用面とコスト面から Agones ベースのソリューションと Amazon GameLift Servers の違いを比較し、Agones から Amazon GameLift Servers へ移行する手順を解説します。

KNFSD ファイルキャッシュのご紹介: NFS ストレージをクラウドに拡張

本記事では、KNFSD File Cache (KNFSD) の仕組みと、オンプレミスのファイラー、サードパーティ、Amazon FSx などの AWS サービスを問わず、NFS 準拠のストレージとどのように連携するかを説明します。また、単一の Terraform モジュールを使って本番環境向けのオートスケーリングクラスターをデプロイする方法も紹介します。このクラスターは、100 Gb 毎秒あたり時間 6 ドル未満で集約スループットを実現します。

AWS Nitro Isolation Engine: AWS Nitro System におけるハイパーバイザーの形式的検証

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

形式的検証済みの Nitro Isolation Engine が Amazon EC2 の仮想マシン分離を数学的に保証

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