Category: Thought Leadership

COBOL のモダナイゼーションを成功させるには、決定論的にリバースエンジニアリングを行い、検証済みで追跡可能な仕様を生成し、それらの仕様をフォワードエンジニアリング用の AI 搭載コーディングアシスタントに流し込むことができるソリューションが必要です。モダナイゼーションを成功させるには、リバースエンジニアリングとフォワードエンジニアリングの両方が必要です。詳しくは、本ブログで知ることができます。

このブログ記事では、移行途中の過渡期に於けるハイブリッドアーキテクチャの連携パターンと連携ソリューションを設計 […]

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

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

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

Amazon Threat Intelligence が観測した、AI で強化された脅威アクターによる FortiGate デバイスへの大規模な不正アクセスキャンペーンについて解説します。ロシア語話者の脅威アクターが複数の商用生成 AI サービスを活用し、55 か国以上、600 台超の FortiGate デバイスの認証情報を悪用して内部ネットワークに侵入し、AI が生成した攻撃計画やツールを駆使して Active Directory の侵害やバックアップインフラストラクチャの標的化を行いました。攻撃手法の詳細と、組織が講じるべき防御策および AWS 固有の推奨事項を紹介します。

ウェブサイトのパフォーマンス問題はよくあることですが、根本原因の特定は困難な作業となります。この投稿では、 S […]

本記事は 2025/11/24 に公開された “Running NVIDIA Cosmos wor […]

本記事は 2025/11/25 に公開された “Physical AI in practice: […]

Amazon Connect はネイティブのテストとシミュレーション機能を発表しました。外部ツールや手動での電話テストなしでコンタクトフローを自動的にテストでき、検証時間を削減します。直感的なビジュアルデザイナーでテストケースを作成し、イベント駆動型モデルで自然な顧客インタラクションをシミュレートできます。このブログ記事ではテストの概要、実践例とベストプラクティスを紹介します。