セキュリティハードウェアの形式的設計・検証理論の深化と展開

深化和发展安全硬件的形式化设计和验证理论

基本信息

批准号：
21H04867
负责人：
本間尚文
金额：
$ 26.29万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (A)
财政年份：
2021
资助国家：
日本
起止时间：
2021-04-05 至 2026-03-31
项目状态：
未结题

项目摘要

本年度は，ガロア体上の算術演算（ガロア体算術演算）のZDD（Zero-suppressed Decision Diagram）表現を用いた形式的検証手法の開発を推進した．特に，前年度から開発を推進してきた冗長表現と非冗長表現が混在するガロア体算術演算回路の形式的表現手法に対応する（機能検証の対象となる）HDL記述の等価性を判定する検証手法に関する理論を構築した．ここでは，提案する形式的表現による回路仕様と任意のHDL記述の等価性判定問題をいかに代数的問題（多項式イデアル所属問題）に帰着させるかが重要となる．そこで，開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出した．ここで，特に，特殊な変数順序（逆トポロジー項順序）で多項式をZDDに変換することを見出した．この変数順序で変換されたZDD集合はグレブナー基底と等価なことを数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できるという特長を有する．その上で，その動作検証を目的として，簡易なガロア体演算回路（32ビットガロア体乗算器等）の仕様と回路記述から得られたZDD集合間の等価性判定を実行した．その結果から，考案手法により高速かつ完全な検証が可能となる見通しを得た．さらに，考案した形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．以上，当初計画していた形式的検証手法の見通しが得られた．

今年，我们推动了一种使用 ZDD（零抑制决策图）表示伽罗瓦域算术运算（伽罗瓦域算术运算）的形式化验证方法的开发。特别是，我们一直在开发一种验证方法，用于确定 HDL 描述的等价性（经过功能验证），该方法对应于具有冗余和非冗余表示混合的伽罗瓦域算术电路的形式表示方法，我们有自去年以来我们一直在发展一种理论。这里，重要的一点是如何将使用所提出的形式表示的电路规范与任意HDL描述之间的等价确定问题减少为代数问题（多项式理想隶属度问题）。因此，在开发方法中，我们首先将待验证的电路规范和电路描述视为多项式集，并推导出它们的范式，即Gröbner基。特别是，我们发现一个特殊的变量阶（逆拓扑项阶）将多项式转换为 ZDD。由于可以在数学上保证用这个变量阶数变换后的ZDD集合等价于Gröbner基，因此它的优点是省略了单独推导Gröbner基所需的大量计算。然后，为了验证其操作，我们对从简单伽罗瓦域运算电路（32位伽罗瓦域乘法器等）的规范和电路描述中获得的ZDD集之间进行了等价性确定。从结果来看，我们预计使用所设计的方法可以进行快速且完整的验证。此外，我们制定了所提出的形式验证方法并开发了其原型软件。如上所述，我们对最初计划的形式化验证方法有了一个展望。