Amazon Web Services ブログ

Tag: automated reasoning

意外な発見: 自動推論がもたらすシステムの効率化と保守性向上

AWS では過去 10 年にわたり自動推論を適用する中で、形式的検証されたコードが未検証のコードよりもパフォーマンスに優れることが多いことを確認しています。S3 インデックスサブシステムの開発高速化、IAM 認可エンジンの 50% のパフォーマンス向上、暗号ライブラリのデプロイとコードの高速化という 3 つの事例を通じて、自動推論がシステムの正しさの保証にとどまらず、効率化と保守性の向上にもつながる好循環を紹介します。

自動推論で「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 を用いて最適化コードの機能的正当性を証明し、開発時間の短縮も実現した取り組みを紹介します。