民間ロケット制御用セキュア通信向け合成体乗算回路の形式検証

• Item type: Symposium(1)
• 公開日: 2024-08-21
• タイトル: 民間ロケット制御用セキュア通信向け合成体乗算回路の形式検証
• タイトル / 言語: en
• タイトル: Formal Verification of Composite Field Multiplier Circuits for Secure Spacecraft Communication
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: セキュリティ
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: インターステラテクノロジズ(株)
• 著者所属: 法政大学
• 著者所属: 情報通信研究機構
• 著者名: 森岡, 澄夫; 尾花, 賢; 吉田, 真紀
• 著者名(英): Sumio, Morioka; Satoshi, Obana; Maki, Yoshida
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 民間宇宙ロケットの制御通信には高いセキュリティが求められ，計算量的安全性ではなく情報理論的安全性を達成できる秘匿・認証アルゴリズム (情報論的暗号と呼ぶ) の利用が理想的である．情報理論的暗号では有限体 GF(2n) 上の乗算が主要演算として用いられるが，通信速度や放射線耐性等の観点から小規模組み合わせ回路実装が，設計品質保証の観点から実装の正当性検証が望まれる．現時点で求められるセキュリティレベル n = 128 に対して，2 次拡大を 7 回繰り返した合成体GF(((((((22)2)2)2)2)2)2) 上の乗算器が知られている限り最小規模であるが，一般的な動的検証では正しいテストデータの生成が容易ではなく総当たりも不可能である．また将来的にはセキュリティレベルの増大も想定されるため，効率的な設計と形式検証を可能とする方法論が不可欠となる．そこで本稿では，合成体上の乗算と単一拡大体上の乗算が同型であることに着目し，AND-XOR 論理関数の等価性判定を利用して同型性を調べる形式検証手法を提案する．提案法では検証の効率化のため，リファレンス回路を体の拡大が一度の単純な構造をもつGF (2 128 )演算器としている．そして，n = 128 に対して実装した回路の正当性を 2 日以内という実用時間で自動検証できることを実証した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: High security is required for the control communication of private space rockets, and the use of cryptographic algorithms achieving information-theoretic security rather than computational security is ideal. We have proposed a cryptographic protocol that guarantees information theoretic security and uses multiplication over finite field GF(2n) as the primary operation. To achieve all of high throughput, small circuit size and high tolerance against soft error, a composite field multiplier is more preferable than a multiplier over a single-extension field, where a composite field is a finite field constructed by multiple extensions. However, a critical obstacle to adopting a composite field multiplier with a large size is the difficulty of verifying its functional correctness with conventional dynamic testing methods (e.g., exhaustive testing) because it is difficult to generate correct test data and finish the test in feasible time. Moreover, considering future increases in security levels, a methodology enabling efficient design and formal verification is required. Therefore, this paper proposes a design and formal verification methodology that examines the isomorphism between a multiplier over a composite field and a multiplier over a single extension field, using equivalence check of AND-XOR logic functions where the reference circuit is the latter multiplier which generally has a much simpler structure. We demonstrated that it is possible to automatically verify the functional correctness of the implementation within two days for n = 128 which currently achieves a satisfactory security level.
• 書誌情報: DAシンポジウム2024論文集; 巻 2024, p. 14-21, 発行日 2024-08-21
• 出版者 / 言語: ja
• 出版者: 情報処理学会