基于COQ的有限域GF(2n)的形式化研究  

Formalization of Finite Field GF(2n)Based on COQ

作　　者：范永乾 陈钢 崔敏 FAN Yong-qian;CHEN Gang;CUI Min(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronauitcs,Nanjing 211000,China;Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211100 [2]高安全系统的软件开发与验证技术工信部重点实验室,南京211106

出　　处：《计算机科学》2020年第12期311-318,共8页Computer Science

摘　　要：有限域GF(2n)是多种安全关键性算法的基础,包括AES加密算法、椭圆曲线加密和感染函数掩码等。相关资料表明,有限域上的运算因为自身的复杂性而容易出错,从而导致系统问题。基于测试和基于模型检测的验证方法只能在n固定的特定有限域上进行验证,而且计算量往往超出计算机的能力。基于交互式定理证明器的形式化验证为有限域性质的通用验证提供了可能性,但这方面的工作难度较大。已有研究主要针对有限域的抽象性质进行形式化验证,但计算机领域更关心的是有限域的构造性定义及相关性质的验证。针对这些问题,借助定理证明器COQ,建立了有限域GF(2n)并给出了其基本运算的构造性定义,同时对一组与有限域有关的基本性质进行了形式化验证,包括有限域加法基本性质的验证、多项式乘法基本性质的验证等,其中多项式乘法是有限域乘法的基础。这项工作为有限域的完整的形式化及基于有限域的算法的形式化验证奠定了基础。The finite field GF(2~n) is the basis of many security-critical algorithms,including AES encryption algorithms,elliptic curve cryptography,infection function masks,and so on.There is data that the operations on the finite field are prone to errors due to their complexity,which causes problems in the system.Verification methods based on testing and model checking can only be applied on specific finite field with fixed by n,and the computation time for the verification often exceeds the capability of the computer.Formal verification using interactive theorem provers provides the possibility for generic verification of finite field pro-perties,but working in this direction fairly challenging.The existing researches mainly focused on the formal verification of abstract properties of finite fields,however,solving practical problems require the use of constructive definitions of finite fields and the verification of its properties.In response to this requirement,this paper uses the theorem prover COQ to develop a constructive and generic definition of finite field GF(2~n),and formally verified a large amount basic properties of finite fields,including verification of the basic properties of finite field addition,verification of the basic properties of polynomial multiplication which is the buliding block of finite field multiplication,as well as verification of other related properties.This work lays a foundation for the complete formalization of finite fields,which will support formal verfications of various algorithms using finite field.

关 键 词：有限域 COQ 形式化验证 定理证明 多项式运算 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]