C2P:基于Pi演算的协议C代码形式化抽象方法和工具

作     者：张协力 祝跃飞 顾纯祥 陈熹 ZHANG Xie-Li;ZHU Yue-Fei;GU Chun-Xiang;CHEN Xi

作者机构：数学工程与先进计算国家重点实验室河南郑州450001 网络密码技术河南省重点实验室河南郑州450002 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2021年第32卷第6期

页      面：1581-1596页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家重点研发计划(2019QY1302)。 

主　　题：协议实现 形式化验证 Pi演算 模型抽取 ProVerif 

摘      要：形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.