计算机应用研究

作者：葛艺,黄文超,熊焰,

单位：中国科学技术大学计算机科学与技术学院,合肥230000；

关键词：形式化验证,形式化建模,协议代码,污点分析,Tamarin,

基金：国家自然科学基金面上项目(61972369)；国家自然科学基金青年项目(62102385)；安徽省自然科学基金资助项目(2108085QF262)；；

随着安全协议形式化分析技术的不断发展，利用工具自动验证虽已得到实现，但建模环节仍需依赖专业人员手工建模，难度大且成本高，限制了此技术的进一步推广。为了提高建模的自动化程度，提出了依据安全协议代码进行形式化模型辅助生成的方案。首先，使用污点分析获取协议的通信流程，并且记录密码学原语操作；然后，根据通信流程之间的序列关系构建协议通信状态机；最终，根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明，此方案可以生成形式化模型中的关键部分，提高了形式化建模的自动化程度，为形式化分析技术的推广作出贡献。

来源：2023年第4期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2023年第4期