Amazon Web Services ブログ

Category: Compute

AWS Weekly Roundup: BYOM for Amazon RDS for SQL Server、AWS IoT Device SDK for Swift など (2026 年 6 月 8 日)

2026 年 6 月 8 日週、AWS IoT Device SDK for Swift が一般公開されました […]

サーバーレス関連の見逃し情報 2025 年第 4 四半期

お知らせ 2026年7月からオンラインでサーバーレスに関するワークショップを4件開催します。ぜひ、ご参加くださ […]

AWS Weekly Roundup: イスタンブールの AWS ローカルゾーン、オープンソースの ExtendDB、Kiro Web など (2026 年 5 月 25 日)

スタートアップとの仕事には、本当に刺激的な何かがあります。私は 2 年以上にわたって、このような仕事に精力的に […]

自動推論で実現する 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 仕様への適合を数学的に証明したプロセスを紹介します。暗号文スティーリングや定数時間設計、メモリ安全性の検証についても解説します。

← Older posts