G-gen の杉村です。当記事では、Google Cloud Next Tokyo 26 の、1日目のキーノートに関する速報レポートをお届けします。 Google Cloud Next Tokyo 26 イベント概要 キーノートの概要 AI による産業の革新 NTTデータの事例 Google の AI エージェントエコシステム Gemini Enterprise のデモ 損害保険ジャパンの事例 Ｓｋｙの事例 スクウェア・エニックスの事例 Agentic Workplace の実現 AI 時代のサイバーセキュリティ Google Cloud Next Tokyo 26 イベント概要 Google Cloud の旗艦イベントである Google Cloud Next の東京版、Google Cloud Next Tokyo 26 は、2026年7月30日（木）と31日（金）の2日間で開催されます。本年は昨年と同様、東京ビッグサイトで開催されました。 東京ビッグサイト ビッグサイト入口 キーノートの概要 初日のキーノート（基調講演）では、AI の社会実装に向けた Google Cloud の AI エージェントエコシステムの紹介や、Google Workspace を活用した自律的なワークプレイスの実現、そして Gemini Enterprise app を中心としたエンタープライズ企業における導入事例が紹介されました。 今回の講演は、技術的なアップデートや新製品の新発表をするというよりも、過去の Google Cloud Next や Google の関連イベントの発表内容を踏襲し、Google の AI エコシステムの紹介や、エージェンティックな仕事改革といった概念の紹介、また日本国内の Google 製品事例にフォーカスしたものでした。 キーノート会場 AI による産業の革新 最初に登壇したのは、Google Cloud Japan 代表の三上智子氏です。 同氏は、産業革命において電気の発明から産業構造の変革まで30年を要したことと現代の AI ブームを比較します。産業革命では工場の各個別の機械にモーターを組み込んだことで革新が起きたことから、現代でも各個別の業務に AI を組み込んで再設計することでこそ、より速いスピードで革新が訪れるのである、という考えを示しました。 Google Cloud 三上智子氏 AI 利用者の約半数がシャドー AI を経験しているという調査結果について言及し、AI ガバナンスの重要性を強調しました。また2030年に向けて、AI を活用した労働力不足への対策や、個人の「暗黙知」「匠の技」を継承していくことが課題となっていくであろうという展望を示しました。 また従来から強調されているとおり、Google が Gemini モデルや AI アプリケーション、プラットフォームのみならず、TPU といった物理レイヤに至るまで、AI 関連技術をフルスタックで開発していることを強調しました。 Google は AI 関連技術をフルスタックで開発 NTTデータの事例 続いて、株式会社NTTデータの常務執行役員 テクノロジーセグメント長 Chief AI Officer、西村忠興氏が登壇しました。 同氏は、NTTデータが2026年6月に Google Cloud と包括契約を締結し、 Google Workspace と Gemini Enterprise を大規模に活用していくことを決定したと述べました。提供者自らが最初の顧客としてソリューションを大規模に導入・活用する「クライアントゼロ」の取り組みを通じてノウハウを蓄積し、顧客へ提供していくとしています。 NTTデータ 西村忠興氏 「クライアントゼロ」 Gemini Enterprise は、Google Cloud が提供する AI エージェント Web アプリケーションです。正式名称は Gemini Enterprise app ですが、多くの公式ドキュメントで単に Gemini Enterprise と言及されていることから、当記事でも Gemini Enterprise の呼称を使用します。 blog.g-gen.co.jp Gemini Enterprise の導入の理由として、 自律的 AI ワークプレイスの実現 というビジョンへの共感や、Google Workspace と Gemini Enterprise が厳格な検証をクリアし、高いセキュリティとガバナンスを備えていることを挙げました。同社は、「チャット型 AI」主体の AI 利用から「自律型 AI エージェント」の利用へと移行し、これを社会に実装することで価値を実現していく考えを示しました。 Google の AI エージェントエコシステム Google Cloud アウトバウンド プロダクト マネジメント ディレクター、リリー・マクニーラス氏が登壇し、Gemini Enterprise Agent Platform などの全体像を解説しました。同氏は、Gemini Enterprise Agent Platform がシンプルさ、安全性、費用対効果を備え、エンタープライズクラスの企業の課題に対処できることを強調しました。 Google Cloud リリー・マクニーラス氏 Gemini Enterprise Agent Platform は、Google Cloud が提供する AI エージェント開発・運用のための統合プラットフォームです。リモート AI エージェントをホストするフルマネージドサービスである Agent Runtime 、エージェントを登録するレジストリとなる Agent Registry 、エージェントの通信制御を担う Agent Gateway のほか、先述の Gemini Enterprise も、Gemini Enterprise Agent Platform のサービス群の1つです。 blog.g-gen.co.jp 同氏は、以下のような紹介を行いました。いずれも新発表ではなく、2026年4月に米国ラスベガスで行われた Google Cloud Next 等のイベントで発表済みのものを、再度強調するものでした。 最新の生成 AI モデル、Gemini 3.5 Flash、Gemini Flash-Lite、Gemini 3.6 Flash、Gemini 3.1 Pro Gemini 3.5 Pro は従来どおり「Coming Soon」 Gemini 3.5 Flash は日本リージョンに対応しており、データ所在の規制要件などに対応可能であること 動画の生成やインタラクティブな編集が可能な Gemini Omni Flash 高度なアルゴリズム開発や課題解決用のエージェントである AlphaEvolve（ロジスティクス、半導体、ゲノミクス向け） 顧客向け（B to C）の AI エージェントを提供する Gemini Enterprise for Customer Experience また、AI と統合されたアプリケーション開発環境である Google Antigravity の企業向けバージョンである Google Antigravity for Enterprise についても再度、紹介されました。Google Antigravity は Gemini Enterprise Agent Platform の API を通じて Gemini モデルなどを呼び出せるようになっており、今後、管理・統制関係の機能も強化されていくことが従来から発表されています。今回の講演では、統制機能に関する詳細やロードマップなどは発表されませんでした。 Gemini Enterprise のデモ Google Cloud のアプライド AI エンジニアである岡本充洋氏により、小売業における Gemini Enterprise のデモが行われました。 同氏は、スーパーバイザーが店舗に臨店し、店舗の状況を音声で記録して報告書を自動作成し、Teams で共有するまでの一連の業務を、Gemini Enterprise の画面から離れずに完了させる様子を実演しました。 また、Gemini Spark を使用し、前日に分析レポートの作成を指示しておき、翌朝に Inbox で結果のレポートを受け取り、PDF として OneDrive に保存するというデモも披露しました。 Gemini Spark は、ユーザーが指示を出すとバックグラウンドで非同期にタスクを処理し、後から結果を得ることができる AI エージェント機能です。2026年7月現在、日本では「数週間以内に個人向けの Google AI Pro プランで利用可能になる」ことが発表されています。 参考 : 「Gemini Spark」： 24 時間 365 日対応する自分だけの AI エージェントが日本の Pro ユーザーにも拡大 今回の講演では、Google Workspace や Gemini Enterprise で Gemini Spark が利用可能になるかどうかは、明言されませんでした。 Gemini Spark 損害保険ジャパンの事例 ＳＯＭＰＯホールディングス株式会社 デジタル・データ戦略部長 兼 損害保険ジャパン株式会社 執行役員 ＣＤＯ ＤＸ推進部長の中島正朝氏が登壇し、既存事業を横断的に DX する「ヨコのDX」における AI 活用事例を紹介しました。 ＳＯＭＰＯホールディングス株式会社 中島正朝氏 同社は、新規事業等における DX を「タテの DX」、既存事業等を横断するものを「ヨコの DX」と位置づけています。 同氏は、Gemini Enterprise 導入の決め手として Gemini Notebook（旧称 NotebookLM）を挙げました。社内の規定類をデータソースとして登録して利用しているほか、会議の録音を自動的に Gemini Notebook に追加することで議事録の作成を不要にした事例を紹介しました。本社公式のノートブックを作成しており、本社へ問い合わせる前にまず AI に確認する習慣が醸成されているとしました。 また、以下のような業務特化型エージェントの市民開発が進んでいることを紹介しました。 モクさぽ（目標設定のためのエージェント） モジおこ（会議の内容を文字起こし） レカみる（レッカー費用などの一次検証） トップダウンでの発信により、AI エージェントの WAU（Weekly Active Users）は80％に達し、AI によって浮いた時間は高付加価値業務に充てられていると述べました。 モクさぽ モジおこ レカみる Ｓｋｙの事例 Ｓｋｙ株式会社の執行役員 太田雅尚氏が登壇し、Gemini Enterprise の全社導入事例を紹介しました。 Ｓｋｙ株式会社 太田雅尚氏 同社では、「コーディング」「検索、質問」「文章作成」などが AI の用途の半分を占めていること、残りの半分が、それらの混合と思われ分類できない「その他」の用途であることを述べました。 AI の用途 同氏は、選定の理由として「処理精度」、「高度な検索」、そして「ガバナンス」を挙げました。導入から5か月間で20,000個のエージェントが作成され、個人の暗黙知やローカルデータの可視化に大きく貢献していると語りました。 スクウェア・エニックスの事例 株式会社スクウェア・エニックスの AI&エンジン開発ディビジョン ジェネラル・マネージャー、荒牧岳志氏が登壇しました。 スクウェア・エニックス 荒牧岳志氏 同氏は、同社における「新しいゲーム体験の創出」と「開発サポート」という2つの異なる場面における AI 活用を紹介し、AI がゲーム画面を見て、考えて、動くことができるマルチモーダル性の重要性を説きました。 Gemini Enterprise Agent Platform を採用し、「ドラゴンクエスト10オンライン」において、ゲーム画面を見て自ら話しかけてくる「おしゃべりスラミィ」を実装した事例を紹介しました。また、開発現場では QA の自動化にも活用されていると述べました。 Agentic Workplace の実現 Google Cloud の Google Workspace プロダクト担当 バイス プレジデント、ユリー クォン キム氏が登壇しました。 Google Cloud ユリー クォン キム氏 同氏は、企業におけるデータの断片化という課題を指摘し、Agentic Workplace の時代が到来したことを述べました。 Workspace Intelligence により分散したデータが統合され、AI に安心して業務を任せられる環境が構築されることを強調しました。 Workspace Intelligence は、2026年4月に発表された、Google Workspace の標準機能です。Gmail、Google ドライブ、Google カレンダー、Google チャットなどを横断して、AI が情報を収集し、コンテキストとして使用してユーザーのタスクを実行します。Gmail 等のサイドパネルで AI に指示をするだけで、これらのアプリを横断した情報収集とタスクの実行が可能です。 参考 : 生成 AI 機能の Workspace Intelligence を制御する 加えて、以下のような実例が紹介されました。 朝、Gmail から優先して読むべきメールをピックアップし、自然言語で質問するとファイルを検索してサマリを表示 Sheets Canvas を使用し、スプレッドシート上で AI がカンバンボードなどのミニアプリを自動作成 Google Meet で、複数言語で会話してもお互いの言語へリアルタイムに AI 同時翻訳を実行 Sheets Canvas で作成されたカンバンボード 続いて、カスタマー エンジニアである服部淳氏によるデモが行われました。Google Pics での画像編集や、Slides のサイドパネルから指示を出して Google チャット、Gmail、Google ドキュメントなどの情報を読み取り、Google スライドで資料を自動生成する様子が紹介されました。 AI を使ったスライドの作成と編集 なお Google Pics とは、AI を使った画像編集ツールです。近日中に Google Workspace で使用可能になることが発表されています。 参考 : Google Pics: AI 画像生成および編集ツール | Google Workspace AI 時代のサイバーセキュリティ 最後に、三上智子氏が再び登壇しました。 同氏は、AI 時代におけるサイバーセキュリティの重要性を強調し、 AI Threat Defense とその機能の一部である CodeMender を紹介してキーノートを締めくくりました。 CodeMender AI Threat Defense は、Google が提唱する AI エージェントを活用したセキュリティフレームワークです。AI モデルである Gemini、セキュリティ製品である Wiz、ソースコードの脆弱性修復エージェントである CodeMender、脅威インテリジェンスである Mandiant を組合わせて、セキュリティを向上させる考えです。 参考 : Google AI Threat Defense 発表：攻撃者の先を行くために 杉村 勇馬 (記事一覧) 執行役員 CTO 元警察官という経歴を持つ IT エンジニア。クラウド管理・運用やネットワークに知見。AWS 認定資格および Google Cloud 認定資格はすべて取得。X（旧 Twitter）では Google Cloud や Google Workspace のアップデート情報をつぶやいています。 Follow @y_sugi_it

みなさん、こんにちは。ソリューションアーキテクトの杉山です。今週も 週刊AWS をお届けします。 みなさんは AWS Builder Center を活用されていますか? AWS Builder Center は、世界中のビルダーが書いた記事や動画などのコンテンツ、コミュニティ、学習リソースがひとつに集まったプラットフォームです。トピックごとにコンテンツがまとまっているのが便利で、例えば agent-to-agent のトピックページ では、AI エージェント同士を連携させる A2A に関する記事を一覧で読むことができます。気になる技術分野のトピックをフォローしておくと、最新のノウハウを効率よくキャッチアップできるので、ぜひ覗いてみてください。 それでは、先週の主なアップデートについて振り返っていきましょう。 2026年7月20日週の主要なアップデート 7/20(月) KNFSD File Cache のプレビュー提供を開始 AWS は NFS キャッシュソリューション KNFSD File Cache のプレビュー提供を開始しました。Apache-2.0 ライセンスのオープンソースで、オンプレミスや別リージョン、他クラウドの NFS サーバーをマウントし、AWS 内の NFS クライアントに再エクスポートします。頻繁に読み取られるデータをメモリとローカル NVMe にキャッシュし、高レイテンシー回線を越えるアクセスを 1 回に抑えて VPC 内速度で配信します。Linux カーネル標準の nfs-kernel-server と FS-Cache を利用し、Packer で AMI を構築後 Terraform でクラスターをデプロイします。全 AWS リージョンで利用でき、ライセンス費用はかからず消費した AWS リソースにのみ課金されます。 Amazon CloudWatch が Coding Agent Insights を発表 Amazon CloudWatch は、AI コーディングエージェントの利用状況を可視化する Coding Agent Insights を発表しました。Claude Code、OpenAI Codex、GitHub Copilot の OpenTelemetry (OTel) メトリクスを CloudWatch に取り込み、組織/部門/チーム/ユーザー単位で利用状況やコストを確認できます。Claude apps gateway for AWS と連携すると、追加の計装なしで Claude Code のテレメトリを収集できます。ダッシュボードは CloudWatch コンソールの GenAI Observability 配下に自動で表示され、料金は標準の CloudWatch OTel メトリクス取り込み料金が適用されます。 Amazon WorkSpaces Applications がマルチセッションフリートで Microsoft OneDrive と Google Drive に対応 Amazon WorkSpaces Applications のマルチセッションフリートで、永続ストレージオプションとして Microsoft OneDrive for Business と Google Drive が利用できるようになりました。従来はマルチセッションフリートで Amazon S3 バックエンドの home folder のみが選択肢でしたが、今回のアップデートでユーザーは自身の OneDrive / Google Drive アカウントを接続し、ストリーミングセッション内でクラウドファイルを直接参照・保存・同期できます。マルチセッションフリートは 1 つのフリートインスタンスを複数ユーザーで共有してセッション密度を高める構成で、コストを抑えながらクラウドストレージ体験を提供できます。機能の追加料金はなく、標準の WorkSpaces Applications 利用料金のみが適用されます。有効化には 2026 年 6 月 29 日以降にリリースされたエージェントを含むイメージが必要です。 Amazon Connect のエージェント型音声機能を対応言語と発話制御の拡張により強化 Amazon Connect は、agentic voice (エージェント型音声) 機能で 50 以上のロケール (言語) と 100 を超える音声オプションに対応しました。Spanish、French、Italian、Japanese、Korean、Portuguese、Thai などが含まれます。発話のペーシング、話者交替 (turn-taking) の精度向上に加え、速度/音量/感情を調整できる発話制御 (speech controls) を利用できます。この機能は Amazon Connect Customer のデフォルト音声プロバイダーとして提供され、米国/欧州/アジアパシフィックの 9 リージョンで利用できます。 AWS CloudTrail で ID 別にネットワークアクティビティイベントを選択的にログ記録 AWS は CloudTrail のネットワークアクティビティイベント (VPC エンドポイント向け) に対して、IAM ユーザー ID に基づくイベントフィルタリングを追加しました。API を呼び出した ID を条件にして、ログを記録するイベントを絞り込めます。例えば信頼済み IAM ロール以外からの VpceAccessDenied イベントだけを記録する、といった設定ができます。これにより、承認済みプリンシパルからの正常なトラフィックを除外し、ログ量とコストを抑えられます。この機能は AWS Management Console、AWS CLI、AWS SDK から利用でき、CloudTrail ネットワークアクティビティイベントが対応する全リージョンで使えます。 7/21(火) Amazon RDS for SQL Server が Microsoft SQL Server 2025 に対応 Amazon RDS for SQL Server が Microsoft SQL Server 2025 (Enterprise、Standard、Developer の各エディション) に対応しました。RDS で提供される最新マイナーバージョンは 17.0.4045.5 (CU5) です。SQL Server 2025 は T-SQL から外部 REST エンドポイントを呼び出す機能をデータベースエンジンに組み込んでおり、Amazon Bedrock や Amazon SageMaker、Amazon S3、AWS Lambda といった AWS サービスとアプリケーションを再設計せずに連携できます。また native vector データ型による埋め込みベクトルの格納/検索に対応し、Standard Edition は最大 32 コア/256 GB バッファプールへ拡張され Resource Governor も利用できるようになりました。既存の RDS インスタンスは DB エンジンバージョンの変更でアップグレードでき、オンプレミスからの移行も可能です。 Amazon ECS が Action Logs を提供開始 (デプロイとオーケストレーションの可視化) Amazon ECS は、サービスデプロイと ECS Managed Daemon 更新の際に ECS がユーザーに代わって実行する操作を、タイムスタンプ付きで記録する Action Logs を提供開始しました。従来は開始状態と終了状態しか観測できなかった中間操作 (コンテナイメージのダウンロード、ロードバランサー登録、セキュリティグループ設定など) を確認できるようになりました。ログはクラスターレベルで opt-in し、CloudWatch Logs、Amazon S3、Amazon Data Firehose のいずれかへ配信できます。Amazon Q が Action Logs と連携し、circuit breaker によるロールバックなどの原因分析をコンソール内で提供します。AWS GovCloud (US) を含む全 AWS リージョンで利用できます。 Amazon SES が料金プランを導入 Amazon SES は、個別のアドオンとして販売されていたメール到達性関連の機能を 3 段階の料金プラン (Essentials、Pro、Enterprise) にまとめて提供する仕組みを導入しました。各プランは下位プランの機能をすべて含み、上位ほど機能が増えます。従来の従量課金と比べて割引が適用されます。プランはアカウント単位かつ AWS リージョン単位で選択し、中東 (UAE) および中東 (バーレーン) を除く Amazon SES 提供リージョンで利用できます。新規アカウントは 2026 年 7 月 21 日以降 Essentials から開始します。 7/22(水) Amazon EKS の EKS Auto Mode と Karpenter で EFA と Placement Group をサポート Amazon EKS の EKS Auto Mode とオープンソースの Karpenter で、ノードプールの EC2 Placement Group (配置グループ) と Elastic Fabric Adapter (EFA) のネットワークインターフェース設定に対応しました。NodeClass または EC2NodeClass の定義から、EFA-only インターフェースの構成と、cluster / spread / partition の 3 種類の配置戦略を指定できます。EFA-only インターフェースは IP アドレスを消費しないため、VPC 内の IP 使用量を抑えながら EFA の帯域を利用できます。分散学習や分散推論のスループット最適化と、本番サービスの障害範囲 (blast radius) 縮小の両方に対応します。この機能は Amazon EKS が利用可能なすべての AWS リージョンで使えます。 Network Load Balancer がカスタムトラフィックルーティング向けのリスナールールに対応 Network Load Balancer (NLB) が、送信元 IP アドレスタイプ (IPv4 / IPv6) に基づいて接続を別々のターゲットグループへ振り分けるリスナールールに対応しました。1 台のデュアルスタック NLB で IPv6 クライアントの通信を IPv6 ターゲットへ、IPv4 クライアントの通信を IPv4 ターゲットへ送り、両方のアドレスファミリでクライアント元 IP をエンドツーエンドで保持できます。従来はロードバランサーを 2 台に分ける方法か、プロトコル変換で元 IP を失う方法のいずれかを選ぶ必要がありましたが、この機能でその制約がなくなりました。既存のデュアルスタック NLB に作り直しなしでルールを追加できます。全 AWS 商用リージョンと AWS GovCloud (US) リージョンで追加料金なしで利用できます。 7/23(木) Amazon CloudWatch Logs が Application Load Balancer ログに対応 Amazon CloudWatch Logs が Application Load Balancer (ALB) のログを vended logs として受け取れるようになりました。ALB のアクセスログ、接続 (connection) ログ、ヘルスチェックログの 3 種類を CloudWatch に直接配信し、Logs Insights クエリ、メトリクスフィルタ、Live Tail で分析できます。配信先は CloudWatch Logs のほか Amazon Data Firehose と Amazon S3 (Apache Parquet 形式対応) を選択できます。CloudWatch telemetry enablement rules を使うと、既存および新規の ALB に対してログ設定を自動適用できます。ALB と CloudWatch が利用可能なすべての AWS 商用および GovCloud リージョンで利用できます。 7/24(金) aws-bench (AWS 上の AI エージェント向けオープンソースベンチマーク) を発表 AWS は 2026 年、AI エージェントが実際の AWS タスクをどれだけ正確かつ効率的に完了できるかを測定するオープンソースベンチマーク aws-bench をリサーチプレビューとして公開しました。実際の AWS 環境を都度払い出し、エージェントに調査・トラブルシューティング・インフラ作成のタスクを実行させて採点します。テストケースは自然言語クエリ、クラウドリソースの状態、正解データの 3 点で構成され、任意のエージェントやモデルを一貫した基準で比較できます。テスト環境の構築・実行・採点・リセットを行う CLI が同梱され、GitHub (Apache License 2.0) で入手できます。 AWS で Claude Opus 5 が利用可能に AWS は 2026 年 7 月 23 日に Anthropic の最新モデル Claude Opus 5 の提供を開始しました。コーディング、長時間稼働エージェント、文書量の多い業務での推論精度が向上しています。提供経路は Amazon Bedrock と Claude Platform on AWS の 2 つで、Bedrock 版はゼロデータ保持 (ZDR) がデフォルトで有効です。コンテキストウィンドウは 1M トークン、最大出力は 128K トークンで、東京リージョン (ap-northeast-1) からは Global クロスリージョン推論経由で利用できます。入力 $5 / 出力 $25 (100 万トークンあたり) の価格で、前世代 Opus 4.8 と同水準の単価に据え置かれています。 Amazon EC2 Dedicated Hosts がセルフマネージドライセンスなしでホストリソースグループに対応 EC2 Dedicated Hosts のホストリソースグループ (Host Resource Groups, HRG) を、これまで必須だったセルフマネージドライセンス (Self-Managed Licenses, SML) の作成と AMI 関連付けなしで作成できるようになりました。ハードウェアレベルの分離だけを目的とする顧客や EC2 Mac インスタンスの顧客は、AWS License Manager でのライセンス設定手順を省略できます。BYOL (Bring Your Own License) ワークロードでは従来どおり SML 付きの HRG も作成でき、起動できる AMI の制限とホスト単位のライセンス消費追跡を継続できます。HRG がサポートされる全ての AWS リージョンで利用できます。 それでは、また来週お会いしましょう！ 著者について 杉山 卓(Suguru Sugiyama) / @sugimount AWS Japan のソリューションアーキテクトとして、幅広い業種のお客様を担当しています。最近は生成 AI をお客様のビジネスに活かすためにアイデア出しやデモンストレーションなどを多く行っています。好きなサービスは仮想サーバーを意識しないもの全般です。趣味はゲームや楽器演奏です。

本ブログは 2026 年 4 月 17 日に公開された Amazon Science Blog “ Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine ” を翻訳したものです。 Isabelle/HOL は、数学的な記述の表現力、自動化、スケーラビリティのバランスによって、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。 2025 年の Amazon re:Invent カンファレンスにおいて、Amazon Web Services (AWS) は Nitro Isolation Engine (NIE) を発表しました。NIE は、お客様のデータのセキュリティを確保しながら AWS のお客様にリソースを提供する役割を担うソフトウェアモジュールです。あわせて AWS は、 Isabelle/HOL という定理証明支援系 (proof assistant) を使用して、この Isolation Engine の正当性とセキュリティ保証を形式的に検証したことも発表しました。世界初の形式的に検証されたクラウドハイパーバイザーとして、NIE はクラウドセキュリティの新しい標準を打ち立てています。 Isabelle はもともと ケンブリッジ大学 と ミュンヘン工科大学 で開発され、現在は世界中の機関や個人による数多くのコントリビューションを取り込んでいます。 定理証明支援系とは、人間のユーザーが形式的証明を構築するのを支援する自動化ツールです。その対象は、数学の定理からハードウェアやソフトウェアシステムの妥当性まで、あらゆるものに及びます。広く使われている定理証明支援系はいくつかありますが、私たちが Isabelle/HOL を選んだのは、表現力、自動化、証明の読みやすさ、スケーラビリティのバランスが私たちの用途に最も適していたからです。これは具体的にどういうことなのでしょうか? コンピュータによる論理的推論 数学に決まった言語というものはありませんが、プログラミング言語が計算タスクを表現するのと同じように、数学的推論を表現するための言語を作ることができます。そして、プログラミング言語に表現力とパフォーマンスのトレードオフがあるように、数学的言語にも表現力と自動化のしやすさのトレードオフがあります。形式的証明の構築は時間がかかり、極めて根気のいる作業であるため (ボトルの中に船を組み立てる作業に似ています)、自動化は不可欠です。 形式的証明の構築は、ボトルの中に船を組み立てる作業に似ています。厳格な論理的制約の中で、すべての部品を正確に組み立てなければなりません。Isabelle/HOL は、この緻密な作業を可能にするツールを提供します。 最も初歩的な数学的言語はブール論理です。これは、AND、OR、NOT といった論理演算子の世界です。この言語は非常にシンプルであるため、強力な自動ソルバーが存在します。2016 年、カーネギーメロン大学の Marijn Heule 教授 (現在は Amazon Scholar ) とその同僚たちは、未解決の数学的問題であるブール・ピタゴラス数問題をブール論理に符号化し、自動ソルバーを使って、200 テラバイトという 史上最大の証明 を作り上げました。 一階述語論理 と呼ばれるより豊かな数学的言語では、整数などの対象領域について語り、その領域上の関数を定義できます。また、「すべての～について」や「～が存在する」という 量化子 を主張に含めることで、ブール論理を超える表現が可能になります。この種の言語では、「2 より大きいすべての素数は奇数である」といった文を表現できます。また、Lewis Carroll による次の定理を証明することもできます。 ワルツを踊るアヒルはいない。ワルツを断る士官はいない。私の家禽はすべてアヒルである。ゆえに、私の家禽の中に士官はいない。 しかし、ほとんどの人は、プログラミングと同じように型を定義できる、さらに強力な数学的言語を好みます。 高階論理 には、 Haskell などの関数型プログラミング言語に見られるような関数型さえ存在します。高階論理は一階述語論理よりもはるかに豊かで、「 数 1 を含み、加法について閉じているすべての集合は、すべての正の整数を含む 」といった文を表現できます。数学の大部分を表現できるほど豊かであると考えられています。 最も豊かな数学的言語である 依存型理論 では、型が任意の値をパラメータとして取ることさえ可能です。例えば T(i) のように、 i を整数とすることができます。この種の言語で最もよく知られているのは Lean と Rocq です。 一階述語論理には強力な自動定理証明器が存在しますが、高階論理やそれ以上の言語では、完全な自動化は利用できません。これが表現力の代償です。 定理証明支援系 を使えば、ユーザーは部分的な自動化の支援を受けながら対話的に証明を構築でき、独自の証明探索をコーディングすることも可能です。定理証明支援系は、論理法則への厳格な準拠を強制します。これは通常、定理を作成する権限をコードの限られた部分にのみ与えるカーネルアーキテクチャによって実現されます。 定理証明支援系は、非常に大規模になり得る形式的仕様の階層を対話的に開発することもサポートします。例えば、Nitro Isolation Engine (NIE) の検証は、Graviton-5 プロセッサのアーキテクチャの仕様、ハイパーコールの Rust コードとその機能的正当性、そして証明すべきセキュリティ特性の仕様の上に成り立っています。形式的証明を構成する 25 万行の大部分は、これらの仕様が占めています。 高階論理は、密接に関連する 2 つの定理証明支援系である HOL と HOL Light でサポートされており、1990 年代からハードウェア設計、浮動小数点アルゴリズム、純粋数学の検証に使われてきました。AWS のシニアプリンシパルアプライドサイエンティストである John Harrison は HOL Light を開発し、暗号アルゴリズムの最適化バージョンを検証することで、Amazon の Graviton2 チップにおけるデジタル署名の パフォーマンスを最大 94% 向上 させました。このコードは繊細であり、網羅的なテストは 現実的ではありません 。このような重要なソフトウェアをデプロイする前に取り得る手段は、完全な機能的正当性の形式的検証しかありませんでした。しかし、ここで注目したいのは Isabelle/HOL です。 Isabelle/HOL の概要 Isabelle/HOL と他の HOL システム (いずれも高階論理に基づいています) の最も目に見える違いは、その仕様記述言語と証明言語です。ほとんどの定理証明支援系では、ユーザーは証明したいことを記述した後、一種のモグラたたきゲームのように、元のゴールを一連のサブゴールに置き換えるコマンドを次々と続けていきます。Isabelle では (Lean でもある程度は)、証明言語によって望ましい中間ゴールを明示的に書き出すことができるため、証明プロセスをより適切に制御でき、より読みやすい証明ドキュメントが得られます。 オンラインには多くの例 があります。 その他の 注目すべき機能 は以下のとおりです。 Rust 言語のかなりの部分を仕様に埋め込むことを可能にした ユーザー設定可能なパーサー 例えば + に、さまざまな数値型だけでなくマシンワードやその他の適切な文脈でも自然な意味を与える、原則に基づいたオーバーロードのための 型クラス 仕様の階層を定義し、証明の中でさえさまざまな方法で解釈できる軽量なモジュールシステムである ロケール (locales) 単純化と後ろ向き連鎖による証明探索を通じた、強力な 組み込みの自動化 さらに強力な外部の自動化にワンクリックでアクセスできる sledgehammer 実際には偽である主張を特定するための 反例発見ツール 適合性のテストに使用した、実行可能な高階仕様からの コード生成 NIE の検証にあたっては、まず 分離論理 (separation logic) と呼ばれる特化した言語を Isabelle/HOL の上に実装することから始めました。分離論理は、共有リソースを操作するプログラムコードの検証のために設計されたものです。私たちは独自の証明自動化をコーディングし、組み込みの自動化も活用しました。そのため、分離論理を使いつつ、必要に応じて通常の高階論理も使うことができました。Isabelle は、非常に巨大なサブゴールにも対処できるほど堅牢かつ効率的であることがわかりました。市販のラップトップを使って、25 万行の証明を 30 分で実行できたのです。 Isabelle/HOL の応用事例 NIE 以前の Isabelle の応用事例として最も印象的なのは、おそらく広く使われているマイクロカーネルである seL4 の検証 でしょう。この証明も最初に発表された時点では約 25 万行でしたが、現在ではさらに長くなっています。seL4 の開発者たちは、マイクロカーネルの C 実装が抽象的仕様を詳細化したものであることを証明し、コア操作の完全な機能的正当性を実現しました。そして、検証されたコード部分ではバグが一切観測されていません。ただし、未検証の部分や形式化できない一部の前提条件をカバーするために、テストは依然として重要な役割を果たしています。 Isabelle は以下のプロジェクトでも使用されました。 エラーの特定、特にその型システムの 健全性の証明 を目的とした、 WebAssembly 言語のセマンティクスの形式化 Cogent プログラミング言語のための 検証フレームワーク の作成 分散編集に使用される、競合のないレプリケートデータ型 (CRDT) のアルゴリズムの 正当性の証明 純粋数学における 数多くの結果の形式化 抽象レベルでの 暗号プロトコルの検証 Isabelle は無料のオープンソースソフトウェアであり、 ダウンロードして利用 できます。十分なメモリを備えたマシンであれば、主要なオペレーティングシステムすべてで動作します。 著者について Larry Paulson Larry Paulson は、ケンブリッジ大学の計算論理学の名誉教授であり、Amazon Scholar です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。