Amazon Web Services ブログ

Category: Compute

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

AUMOVIO が Amazon Bedrock 搭載のエージェント型コーディングアシスタントでソフトウェア開発を強化

本ブログ記事では、AUMOVIO が Amazon Web Services (AWS) のサービスと知見を活用して、Software-Defined Vehicle (SDV) 領域における革新的な自動車向けコーディングアシスタントを開発した事例をご紹介します。AUMOVIO のソリューションは、複数の AI モデルを活用して開発ライフサイクルの各工程を加速させながら、自動車業界の標準と AUMOVIO 独自のコーディングベストプラクティスに準拠しています。可能な限りコードを再利用し、変更を最小限に抑えることで、このアシスタントは V 字モデルの他の工程に必要な作業を大幅に削減します。

← Older posts
Newer posts →