はじめに：設計における2つのアプローチ こんにちは。電通総研の技術統括推進ユニット 江夏秀俊と、同じく電通総研の製造エンジニアリング本部 エンジニアリング1ユニット 齊藤智明です。 製品開発やエレキ・メカ設計の現場で、次のような状況を目にすることはないでしょうか。 「機能ブロック図などの図面（定性モデル）を作成してみたものの、その後の詳細設計への活かし方が分からない」 「外部の提案や手法に沿って構造の整理を進めたが、具体的な仕様決定やトレードオフの判断で行き詰まる」 「設計判断を迫られても数値的な根拠がなく、最終的に経験則や勘に頼って決定してしまう」 多くのエンジニアは、普段から数式や計算（定量モデル）を用いて設計業務を行っていることと存じます。しかし、導入された定性モデルとの付き合い方や、両者の役割分担に悩まれるケースも少なくありません。 本記事で最初にお伝えしたいのは、 「定性モデルは不要」と否定するつもりは一切ない ということです。設計活動には役割の異なる「定性モデル」と「定量モデル」の2つが存在し、 両者を組み合わせることで、より根拠のある設計判断が可能 と考えます。 定性モデル： 構成や機能を分解・整理・共有するためのアプローチ（例：機能ブロック図、概念図、システム構成図） 定量モデル： パラメータや物理量を計算・解明するためのアプローチ（例：数式モデル、1DCAE(Simulink、Modelica言語など)/3DCAE） ※本記事では議論の前提として、ドキュメントベースの静的な図面だけでなく、SysML等のモデリング言語による記述であっても、外部ソルバーや物理計算と自動連携されていない静的な記述に留まるものは便宜上「定性モデル」として扱います。 `【図1：定性モデルと定量モデルの役割と、両者を組み合わせた設計判断のプロセス】` 本記事では、定性モデルが持つ本来の価値を整理したうえで、なぜ定性モデル「だけ」では設計判断が難しいのかという理由と、本来必要な「定量モデル」が担う役割について解説いたします。 定性モデルの重要な役割 ～全体構造の共通言語として～ 前提として、機能ブロック図などの定性モデルは、設計活動において「全体構造の共通言語（マップ）」として機能します。 議論の土台： 既存製品やシステム全体像を俯瞰し、チームや部門間で認識を揃える。 概念の共有： 専門外のメンバー（他部署やステークホルダー等）に対し構造をわかりやすく説明する。 インターフェース整理： 機能同士の繋がりを明確にし、モジュール化や仕様のモレを防ぐ。 市販の汎用ユニットや仕様や許容範囲が明示された規格部品を組み合わせるだけのアセンブリ設計であれば、各モジュールの性能や接続条件が事前に規定されているため、定性モデル（構成図など）だけでも モジュールの選定や組み立て が成立する場合があります。 しかし、 新領域の製品開発や新規設計、極限までの性能追求が求められる開発 においては、構成図だけでは「物理的に本当に成立するか」を担保することが困難です。どれだけ綺麗な機能ブロック図を描いたとしても、それ単体で部品の寸法や仕様の数値が決まるわけではないためです。 定性モデルだけでは「設計判断」が難しい3つの理由 定性モデル「だけ」で設計判断（仕様決定やトレードオフ）を下そうとすると、次の3つの壁に突き当たると考えられます。 理由1：数値による「性能評価」が難しい 機能ブロック図の上に「冷却ファンから熱交換器へ風を送る」と定義することで、機能の定義や接続関係は明確になります。しかし、「具体的に温度が何℃低下するか」という物理量による定量的な評価が難しくなります。 その結果、「良くなりそう」という感覚だけで判断を進めてしまい、後工程の実機テストなどの段階で目標性能に届かないことが発覚し、大幅な手戻りが発生するリスクがあります。 理由2：「設計限界」の評価が難しい 「どこまで板厚を薄くしたら破壊するか」「最大荷重がかかった際に変形が許容内に収まるか」といった限界値（マージン）は、ブロック図を描くだけでは見極められません。 結果として、限界が分からないために安全側を見すぎて過剰設計となり、コスト高や重量増加を招くか、逆に限界を見誤って品質リスクを抱える懸念があります。 理由3：対象の「物理特性」の評価・追跡が難しい SysMLなどのアーキテクチャ図やブロック図の補足として、注釈テキストで V = IR（オームの法則）や F = ma（運動方程式）などといった具体的な数式が併記されているケースがあります。 しかし、モデル図やドキュメントの上にいくら数式が書かれていても、それらは人間が読むための「文字情報（注釈）」に過ぎません。モデル内の変数同士がプログラムや計算式として相互に自動連動（自動計算）されていない以上、仕様変更や異常が発生した際の静的・動的な物理応答を評価・追跡することは難しくなります。 `【図2：定性モデルの壁と定量モデルによる補完】` 定性モデルを補完し、より確かな設計判断を下すための「定量モデル」 定性モデルを補完し、より確かな設計判断を下すためには 物理現象を数学的に表現した「定量モデル（数式・シミュレーション）」 の活用が重要となります。 もちろん、定量モデルの構築にはモデル作成コストや専門知識が必要という側面もあります。だからこそ、まず定性モデル（全体マップ）で「どこを定量計算すべきか」の範囲を絞り込み、その上で「1DCAE（集中定数モデルやModelicaなどを活用したシステムレベルのシミュレーション）」や「3DCAE（構造・流体・電磁界解析など）」といった定量モデルを活用することが効率的です。 定量モデルを活用することで、3つの壁に対応した設計判断が可能になると考えられます。 1. 性能の数値化（理由1へのアプローチ） 「〇〇Wの熱が発生した際、何℃まで温度が上昇するか」といった具体的な数値を物理シミュレーションによって算出し、定量的な評価結果として性能を評価できます。これにより、試作前に性能未達リスクを低減できます。 2. 限界・境界の予測とトレードオフ評価（理由2へのアプローチ） 製品が破壊・作動不良を起こすギリギリの境界値（設計限界）を予測・評価できます。これにより、過剰設計（オーバースペック）を防ぎつつ、「軽量化と強度のトレードオフ評価（最適解の探索）」などの判断をデータに基づいて下すことが可能になります。 3. 物理特性（動作）のトレースと実測検証（理由3へのアプローチ） 変数同士が計算結合されたモデルを用いることで、仕様変化に伴う定常応答や、時間経過に伴う動的な過渡応答を数学的にトレースできます。また、実測データ（ベンチテスト）と比較することで、モデルの妥当性の確認（バリデーション）やトラブル原因の分析に活用できます。 まとめ：定性で共有し、定量で判断する 「機能ブロック図を作成して完結した気になってしまう（その後の使い道が見えない）」という課題に対する有効なアプローチは、両者の役割分担を正しく理解することだと考えます。 定性モデルは「認識合わせのツール」： システム全体の構造や機能を関係者間で共有し、共通言語を作るために使う。 定量モデルは「設計判断のツール」： 物理的な数値根拠を導き出し、仕様決定やトレードオフ評価を行うために使う。 機能ブロック図などの定性モデルの上に、単に結果の数値を注釈としてメモするだけでは、計算可能な形で定量化されたとは言えません。定性モデルで全体像を可視化しつつ、その裏側にあるシミュレーション等の定量モデルと連携させて数値的な根拠に基づく設計判断を下す。この「両輪のアプローチ」を正しく機能させることが、手戻りの低減や、より確かな設計判断へ繋がる一助になるのではないかと考えております。 私たちは一緒に働いてくれる仲間を募集しています！ 電通総研 キャリア採用サイト 電通総研 新卒採用サイト 執筆： @koka.hidetoshi レビュー： @miyazawa.hibiki （ Shodo で執筆されました ）

本ブログは 2026 年 6 月 11 日に公開された AWS Blog “ AWS Nitro Isolation Engine: Formally verifying the hypervisor in the AWS Nitro System ” を翻訳したものです。 Ali Saidi は AWS の VP 兼 Distinguished Engineer です 何百万ものお客様が、最も機密性の高いワークロードの保護に AWS Nitro System を利用しており、AWS はお客様のデータを保護するイノベーションにおいて業界をリードしています。お客様のデータの安全性と機密性を守ることは AWS の最優先事項であり、データの分離と保護のための専用ハードウェアとソフトウェアへの投資を継続しています。 2017 年、AWS は Nitro System をリリースしました。これは、ゼロオペレーターアクセス (オペレーターがお客様のデータに一切アクセスできない状態) を前提に設計された、初の主要なクラウドプラットフォームです。Nitro System は、次世代のすべての Amazon EC2 インスタンス の基盤となる専用のハードウェアとソフトウェアであり、仮想化、ストレージ、ネットワーキングの機能を専用ハードウェアと最小限のハイパーバイザーにオフロードします。Nitro System では、最も高い権限を持つ AWS オペレーターであっても、認証と監査が行われる管理用 API を通じてのみシステムとやり取りでき、これらの API からお客様のワークロードにアクセスすることはできません。このアーキテクチャはクラウドセキュリティの業界標準を確立し、NCC Group などの第三者機関が独立した立場でこのアプローチの妥当性を確認してきました。 そして今、AWS はさらに水準を高めます。AWS Nitro System の主な役割の 1 つは、インスタンスを互いに分離し、AWS オペレーターからも分離することです。これは 10 年以上にわたり Nitro System アーキテクチャの基盤となってきました。AWS Nitro Isolation Engine は、AWS re:Invent 2025 で初めて発表され、本日 (2026 年 6 月 11 日) よりすべての Graviton5 ベースのインスタンスで一般提供を開始しました。これは Nitro Hypervisor 内の専用コンポーネントであり、この分離を実施し、それを数学的な厳密さで証明する役割を担います。Nitro Isolation Engine は形式的検証を採用しています。形式的検証とは、ハードウェアやソフトウェアが特定のテストケースだけでなく、あらゆる状況で意図したとおりに動作することを数学的に証明する手法です。この徹底的な検証手法により、Nitro は形式的に検証された初のクラウドハイパーバイザーとなり、数学的に証明されたクラウドセキュリティの新しい標準を確立しました。 AWS Nitro Isolation Engine Nitro System において、AWS Nitro Hypervisor は、すべての仮想マシンについて、権限のないエンティティがお客様のデータを読み取ったり変更したりできないように設計されています。Nitro Isolation Engine は Nitro Hypervisor の専用コンポーネントであり、これらの仮想マシン間の分離を実施します。仮想マシンのメモリ、CPU レジスタの状態、および I/O デバイスへのすべてのアクセスを、Nitro Hypervisor の他の部分に公開される最小限の API セットを通じて仲介します。Nitro Isolation Engine は、お客様のデータへのアクセスを仲介する唯一のシステムコンポーネントです。Nitro Hypervisor の他のコンポーネントは、この制限されたインターフェイスを通じて動作する必要があり、お客様のワークロードに直接アクセスすることはできません。Nitro Isolation Engine のコードベースは最小限に抑えられているため、人による監査が容易になり、バグが混入し得る範囲が減り、その設計と実装に形式的検証を適用することが現実的になっています。 形式的検証 形式的検証は、数学的証明を用いて、システムの形式的モデルの特性が、あり得るすべてのシステム状態とすべての入力において成立することを示します。これは、あり得る状態と入力のうち (場合によっては大規模な) 一部に対してシステムの動作を確認するテストとは対照的です。形式的検証は、従来のテストよりも正確性についてはるかに強い根拠を提供します。Nitro Isolation Engine の場合、分離特性は、あり得るすべてのシステムの動作にわたって保証されます。テストと検証は相互補完的な関係にあります。検証はテストを補強し、テストはまだ検証されていないシステムの領域をカバーして、システムが意図したとおりに動作しているという経験的な裏付けを与えます。 お客様にとって、分離を実施するコードが形式的に検証されていることは、包括的なテストを超える保証となります。テストは引き続き不可欠であり、AWS はテストにおいても高い基準を維持していますが、テストで確認できるのは特定のシナリオに限られます。形式的検証はこれを補完するものであり、テストでカバーされるシナリオだけでなく、あり得るすべてのシナリオにわたって分離特性が数学的に保証されることを意味します。 形式的に検証された特性 Nitro Isolation Engine の形式的検証により、4 つの主要な特性が確立されます。 1. 機密性と完全性 – Nitro Isolation Engine は、ゲスト仮想マシン (VM) の機密性と完全性を維持します。機密性とは、ゲスト VM のプライベートデータが権限のないエンティティによって読み取られないことを意味し、完全性とは、ゲスト VM のプライベートデータが権限のないエンティティによって変更されないことを意味します。 2. 機能的正確性 – 検証されたすべてのハイパーコールは、仕様で定義された期待される動作と一致します。仕様には各ハイパーコールの事前条件と事後条件が記述されており、証明によって、実装がそれらから決して逸脱しないことが立証されます。 3. ランタイムエラーが発生しないこと – コードがランタイムエラーに遭遇することはなく、実装は仕様どおりに動作します。これらの特性の形式的検証を組み合わせることで、検証の対象となるあらゆる一連のイベントに対して Nitro System が分離を維持することが、数学的に厳密に保証されます。現時点では、この検証は、VM の起動、実行、および終了を担う VM のコアライフサイクルのハイパーコールを対象としています。 4. メモリ安全性 – バッファオーバーフロー、NULL ポインタ逆参照、範囲外アクセスなどのメモリ安全性違反が存在しないことを立証します。すべての検証済みソフトウェアと同様に、Nitro Isolation Engine の証明は、Rust コンパイラやハードウェアの正確性などの前提に基づいています。これらの前提、およびエンジニアリングと検証に対する AWS のアプローチについては、Nitro Isolation Engine のホワイトペーパーで詳しく説明されています。 Rust による実装 Nitro Isolation Engine は Rust で実装されています。Rust は、機密性の高いソフトウェアにおけるセキュリティ脆弱性の根本原因となってきた、よくあるプログラミング上の落とし穴を防ぐように設計されたシステムプログラミング言語です。Nitro Isolation Engine に Rust を採用したことで、複数の種類のバグを設計上まとめて排除しています。Rust が適している理由はその型システムにあります。型システムが厳格な所有権規則を適用するため、形式的検証の一部が容易になり、コンパイル時に第一段階の保証が得られます。 まとめ Nitro Isolation Engine は、お客様のデータの機密性を守るという AWS の継続的なコミットメントを体現するものです。そして、これはまだ出発点にすぎません。AWS は、セキュリティに影響を与える Nitro Isolation Engine のすべての主要コンポーネントに形式的検証を拡張し、新機能が導入されてもそれらの証明を維持し続けます。さらに、Nitro Isolation Engine のソースコードと形式的証明を第三者に提供し、独立した検査およびレビューを受けられるようにする予定です。このレベルの透明性は、クラウドプロバイダーが開かれた姿勢、コード品質、形式的検証をどのように示せるかについて、新しい標準を確立するものと考えています。 AWS Nitro System とコンフィデンシャルコンピューティングの詳細については、以下のリソースをご覧ください。 AWS Nitro Isolation Engine Whitepaper コンフィデンシャルコンピューティング： AWS の視点 (2021) AWS Nitro System のコンフィデンシャルコンピューティングに対する第三者評価の獲得 (2023) AWS Nitro Whitepaper AWS re:Invent 2025 presentation – Introducing Nitro Isolation Engine: Transparency through Mathematics 著者について Ali Saidi Ali は Amazon Web Services (AWS) のバイスプレジデント兼 Distinguished Engineer です。ミシガン大学でコンピュータサイエンスおよび工学の博士号を取得しています。2017 年に AWS に入社して以来、AWS Nitro System、AWS Graviton、および幅広い EC2 インスタンスファミリーのポートフォリオの設計と開発に注力しています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

本ブログは 2026 年 6 月 10 日に公開された Amazon Science Blog “ EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation ” を翻訳したものです。 「分離カーネル (separation kernel)」を Nitro セキュリティシステムの他の部分から切り離し、Rust プログラミング言語のサブセットのみを使用して実装したことで、形式的検証が可能になりました。 本日 (2026 年 6 月 10 日)、AWS は Amazon Elastic Compute Cloud (Amazon EC2) の新しい M9g および M9gd インスタンスの一般提供開始を発表しました。これらは、汎用 CPU の最新世代である Graviton5 を搭載した初のインスタンスタイプです。Graviton5 では、コア数が前世代の 96 から 192 に倍増しています。 また、これらは新しい Nitro Isolation Engine を使用する初のインスタンスタイプでもあります。Nitro Isolation Engine は Nitro Hypervisor のコンポーネントであり、その唯一の役割は仮想マシン (VM) を相互に分離することです。この記事では、推論の各ステップが論理法則に従っているかを機械的にチェックするソフトウェアである Isabelle/HOL (高階論理) 定理証明支援系 (proof assistant) を使って、Nitro Isolation Engine が正しく動作し、VM 間の分離を強制することをどのように証明したかを解説します。Nitro Isolation Engine は、商用クラウド環境にデプロイされた初の形式的検証済みハイパーバイザーの重要なコンポーネントです。 Isabelle/HOL によるモデルと証明は、機械的に検証された 330,000 行の数学的記述から成ります。これは、現実的なオペレーティングシステムの検証が実現可能であることを初めて実証した画期的なプロジェクトであり、私たちの取り組みの着想源ともなった seL4 に匹敵する規模です。ただし seL4 とは異なり、Nitro Isolation Engine は商用クラウド環境向けに設計されており、Graviton5 のユーザーに対して常時有効な機能として本番ハードウェア上で提供されます。 2025 年の Amazon re:Invent カンファレンスで行った 講演 では、形式的検証の方法論を紹介しています。また、 ホワイトペーパー では、検証の範囲や前提条件など、結果の重要な側面をより詳しく解説しています。このブログ記事では、形式的検証の取り組みにおける主要な要素と、それらがどのように組み合わさっているかの概要を、わかりやすくご紹介します。 分離カーネルとは何か 「分離カーネル」という用語は、John Rushby 氏が 1981 年に生み出しました。これは、システムを分離されたコンパートメントに分割する最小限の OS コンポーネントを指します。重要なアイデアは、 ポリシー と メカニズム の分離です。分離カーネルは、何を分離するか、リソースをどう割り当てるか、どの VM をスケジュールするかを決定しません。それらの決定は別の場所で行われます。その代わり、分離の強制だけに専念します。この目的の明確さにより、分離カーネルはフル機能の OS カーネルよりもはるかにシンプルに実装できます。 2017 年の導入以来、Nitro Hypervisor は Amazon EC2 における分離の強制を担ってきましたが、同時にビジネスロジック、デバイスドライバー、AWS 固有の機能も処理しています。この複雑さが、正当性の証明を大幅に難しくしています。さらに、Nitro Hypervisor は当初から検証を想定して設計されたものではありませんでした。 ハイパーバイザーの重要な分離ロジックを Nitro Isolation Engine という最小限のコンポーネントに抽出したことで、検証と監査が可能な小さなサイズになり、分離がどのように強制されているかについて、お客様はかつてないレベルの可視性を得られます。また、Nitro Isolation Engine は、形式的検証との相性がより良い言語である Rust で記述しました。 Nitro Hypervisor は引き続きポリシー (VM の作成、リソース割り当て、移行、スケジューリング) を処理しますが、現在は権限が引き下げられており、ゲストの状態に触れるあらゆる操作を Nitro Isolation Engine に依頼する必要があります。Nitro Isolation Engine は、実行前にすべてのリクエストをチェックします。 Nitro Isolation Engine を有効にしたサーバーのシステムアーキテクチャ。 仕様と証明 この取り組みの 2 つの重要な要素は、仕様と証明です。形式仕様はシステムに期待される動作を正確に記述し、証明は実装がその仕様を満たしていることを立証します。 Nitro Isolation Engine に関する定理は、次の 4 種類の性質を対象としています。 機密性と完全性。 許可された情報フローのみが発生します。例えば、ゲストに割り当てられたメモリ領域は、再利用の前に必ずスクラブされます 機能的正当性。 実装は仕様どおりに正確に動作します ランタイムエラーの不在。 Rust における None オプション値の unwrap (プログラムの実行を停止させる誤ったコマンド呼び出し) のようなランタイムエラーが存在しません メモリ安全性。 バッファオーバーフローや NULL ポインタ参照といった問題が存在しません 実際には、後者の 3 つの性質は機能検証の結果としてまとめて扱い、機密性と完全性は別途扱います。これは、それぞれに異なる証明手法を用いるためです。 機能検証 機能検証における重要な要素は次のとおりです。1 つ目は μRust (マイクロ Rust) と呼ばれる Rust 言語のコアサブセットの形式化、2 つ目は仕様を正確に記述するための分離論理 (Separation Logic) を用いた表現力の高い仕様記述言語、3 つ目はプログラムが仕様に対して正しいことを証明するための検証手法である最弱事前条件計算 (weakest-precondition calculus) と独自の証明自動化です。これらはいずれも汎用的な証明インフラストラクチャの一部であり、2025 年に AutoCorrode ライブラリ としてオープンソース化しました。 より詳しく説明すると、μRust は Rust プログラミング言語の制限されたサブセットで、Nitro Isolation Engine を記述するのに十分な表現力を持ちながら、形式的な推論にも適しています。これは、トレイトや動的ディスパッチといった高度な Rust の機能を意図的に除外しているためです。μRust の形式的意味論は、Isabelle/HOL への 浅い埋め込み (shallow embedding) として定義されています。つまり、μRust の意味は、Isabelle/HOL の「ホスト言語」である高階論理を使って定義されます。 μRust プログラムの仕様は、事前条件と事後条件を持つ契約として定義されます。これらは、プログラム実行前後のシステム状態に関する表明です。この契約は「全正当性 (total correctness)」を規定しています。つまり、事前条件を満たすすべての状態において、プログラムは必ず終了し、その結果の状態は事後条件を満たします。この全正当性の条件は、プログラムがメモリ安全であり、ランタイムエラーがないことも意味します。仕様は、低レベルのポインタ操作プログラムについて推論するために設計された論理である 分離論理 を使って記述されています。 分離カーネルは比較的シンプルとはいえ、Nitro Isolation Engine の検証は、形式的検証で可能な範囲の限界に近い取り組みであり、仕様も証明も非常に大規模になります。例えば、以下の仕様は、実行中のゲスト仮想 CPU が自分自身の電源をオンにしようとした場合 (誤ったリクエスト) に何が起こるかを記述したものです。 対象の CPU をオンにするための電源状態関数 PSCI_CPU_ON の仕様。 上記の仕様は複雑ですが、その内容は直感的にはシンプルです。この状況では、Nitro Isolation Engine は、呼び出し元として動作するには当該の仮想 CPU が既にオンになっているはずだと判断し、定義済みのエラーコード AlreadyOn を返します。それ以外のシステム状態はすべて変更されません。仕様の複雑さは、モデリングの深さと、Nitro Isolation Engine の実装においてこの時点に到達するまでに他の複数のエラーチェックが既に実行されているという事実を反映したものです。 μRust プログラムが仕様に対して正しいことを証明するには、標準的な 最弱事前条件計算 を使用します。最弱事前条件計算とは、特定の操作の後のプログラムの状態が、指定された状態の範囲から外れないことを保証できる、最も制約の少ない条件を体系的に特定する方法です。例えば、式 x + y の最弱事前条件は、 x と y の値の加算がオーバーフローしない状態です。そのうえで、契約の事前条件が計算された最弱事前条件を含意することを示すのが証明義務となります。 機密性と完全性 機密性と完全性に関する 1 つ目の重要な要素は、Nitro Isolation Engine の動作を遷移関係として記述する高レベルの仕様です。ここでは、システムの各「高レベル」ステップ (ハイパーコールなど) が 1 つのアトミックな遷移となります。この仕様は、リファインメント (Refinement) と呼ばれる別の証明のアイデアを用いて、機能検証の結果で使用されるより具体的な分離論理の仕様と厳密に結び付けられています。2 つ目の重要な要素は、 非干渉性 (noninterference) という考え方です。 非干渉性とは、機密性と完全性を数学的に厳密なものにするために使用する、識別不能性の保存という考え方です。あるステップの前に 2 つの状態が観測者にとって識別不能であれば、ステップの後も識別不能なままでなければならない、というものです。これが機密性を表す直感的な理由は、そのステップによって観測者が新しい情報を何も得ていないためです。 識別不能性の保存がなぜ機密性を保証するのかは、少しわかりにくいところです。パブリックレジスタとプライベートレジスタを 1 つずつ持つ、2 つのシンプルなマシン A と B を考えてみましょう。プライベートレジスタは隠されているため、観測者は、パブリックレジスタが一致していれば 2 つのマシンを識別不能とみなします。以下の図では、A と B は識別不能です。 機密性違反の例。 ここで、プライベートレジスタの値によって分岐し、パブリックレジスタに 1 を代入するプログラムを実行するとどうなるかを考えてみましょう。結果として得られるマシン A’ と B’ は、パブリックレジスタの値が異なるため、 識別可能 になってしまいます。賢い観測者はこれを利用して元のプライベートレジスタの値を導き出せてしまいます。つまり、識別不能性が保存されないということは、観測者への不正な情報フローが生じていることを意味します。 今後の展開 ここまで、検証の取り組みにおける主要な要素の概要をご紹介しました。この取り組みには、適合性テストや、並行コードに関する推論の扱い方など、他にも多くの側面があります。今後の記事でお伝えできることを楽しみにしています。 著者について Dominic Mulligan Dominic Mulligan は、Amazon の Automated Reasoning Group の principal applied scientist です。 Nathan Chong Nathan Chong は、Amazon の Automated Reasoning Group の principal applied scientist です。並行システムコードの正当性、特にハードウェアとソフトウェアの境界領域を専門としています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。