2024-03-28T20:48:41Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000867372023-11-14T00:51:14Z06164:06165:06462:06909
PPRMベース形式手法を用いたAES内演算回路の最適化検証Verification of AES component H/W optimization using a PPRM-based formal methodjpnAES,回路実装,形式検証,PPRMhttp://id.nii.ac.jp/1001/00086722/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=86737&item_no=1&attribute_id=1&file_no=1Copyright (c) 2012 by the Information Processing Society of JapanNEC 中央研究所森岡, 澄夫AES暗号回路の実装に誤りがない事を100%保証したい.個別演算器の検証に絞っても,MixColumns,マスキングなどサイドチャネル攻撃対策を施した演算器,用いる基底を変えた演算器等では,総当りが依然難しかったり正しい仕様(リファレンス)をどのように作るかが問題となったりする.従来,有限体が多用される暗号回路向けの形式検証手法はほとんどなかったが,近年,本間らがGrobner基底を用いた手法を提案するなど,報告が増え始めた.本稿では,リファレンスをボトムアップ構築しつつ,論理式のPPRM(Positive Polarity Reed-Muller)変換を用いて,演算器が正しく最適化されている事を短時間で検証した事例を示す.In this paper, we propose a formal verification (FV) method which is suitable for AES H/W verification. Exhaustive testing based on dynamic simulation, even for partial components such as MixColumns, side-channel resistant masked operators and some other optimized operators, is difficult. Another important issue is how to construct correct specifications, or reference, of these components. In this paper, we demonstrate (i) bottom up construction of the reference and (ii) fast correctness proof of optimized AES components. A simple decision procedure which convert logic formula into PPRM (Positive Polarity Reed-Muller) form is used.コンピュータセキュリティシンポジウム2012論文集201237657722012-10-232012-11-02