Amazon Web Services ブログ

Category: Graviton

自動推論で実現する Amazon のポスト量子暗号の検証と最適化

AWS は、Amazon Automated Reasoning Group、AWS Cryptography、オープンソースコミュニティと協力し、ポスト量子暗号 (PQC) ML-KEM の形式的に検証された最適化実装 mlkem-native を開発しました。本記事では、CBMC によるメモリ安全性・型安全性の検証、HOL Light と s2n-bignum によるアセンブリ実装の正当性証明、SLOTHY によるマイクロアーキテクチャ最適化を組み合わせ、セキュリティ・性能・保守性を同時に実現した取り組みをご紹介します。AWS-LC への統合により、c7i や c7g で約 2 倍の性能向上を達成しました。

形式的検証済み AES-XTS: s2n-bignum に加わった初の AES アルゴリズム

AWS は AES-XTS 復号の最適化された Arm64 アセンブリ実装の形式的検証に成功し、s2n-bignum ライブラリに初の AES アルゴリズムとして追加しました。本記事では、コア演算のアセンブリコードを単純化することで SLOTHY による自動最適化を可能にし、HOL Light 対話型定理証明器を用いて IEEE 1619 仕様への適合を数学的に証明したプロセスを紹介します。暗号文スティーリングや定数時間設計、メモリ安全性の検証についても解説します。

自動推論で「25519」楕円曲線暗号の高速化と正当性保証を実現

自動推論と CPU マイクロアーキテクチャ固有の最適化を組み合わせ、AWS-LC における x25519/Ed25519 楕円曲線暗号の高速化と正当性保証を実現しました。HOL Light 定理証明器による形式的証明で実装の正しさを検証し、AWS Graviton 2、AWS Graviton 3、Intel Ice Lake の 3 つのマイクロアーキテクチャ全体で平均 86% のパフォーマンス向上を達成しています。定数時間実装によるサイドチャネル攻撃対策や、アプリケーションでの活用方法についても紹介します。

Graviton での RSA の高速化: 形式的検証で正当性を証明し開発も加速

Amazon の Automated Reasoning グループが、Graviton チップにおける RSA 署名のスループットを、モンゴメリ乗算やカラツバアルゴリズム、SIMD 命令の活用により鍵サイズに応じて 33～94% 向上させました。さらに、HOL Light 対話型定理証明器と形式的検証済み多倍長整数演算ライブラリ s2n-bignum を用いて最適化コードの機能的正当性を証明し、開発時間の短縮も実現した取り組みを紹介します。

Integral Ad Science における Amazon OpenSearch Service を使った日次 1 億件超のドキュメント処理の紹介

Integral Ad Science (IAS) が Amazon OpenSearch Service を活用し、日次 1 億件以上のドキュメントを処理するスケーラブルな SaaS 型 ML プラットフォームを構築した事例を紹介します。ベクトル検索の最適化により、複雑な検索オペレーションで 40〜55% のパフォーマンス向上を達成しました。

Amazon GameLift Servers でローンチを成功させるためのステップ：開発フェーズ

私たちはグローバルなゲームサーバーホスティングのためのフルマネージド型サービスである Amazon GameLift Servers をお勧めしています。このサービスは、オーケストレーション、グローバルなセッション配置、ゲームセッションライフサイクル管理を担うため、マルチプレイヤーゲームのローンチにおける運用作業とストレスを軽減するのに役立ちます。

このブログシリーズでは、ゲームローンチを成功させるための準備の重要な考慮事項について説明します。この最初のブログはプリプロダクションで実行すべきアクションに焦点を当て、第 2 部はプリローンチ準備 ( ローンチの 2〜3 ヶ月前 ) に焦点を当てます。これらの推奨事項は、開発初期のインテグレーションからゲームローンチまで数百のゲームスタジオをサポートした経験に基づいています。

← Older posts