报告题目：网络安全协议通用全自动形式化验证系统SmartVerif

报告时间：2021年12月11日（周六）下午3：00

报告地点：翡翠科教楼A座二楼第七会议室

报告人：熊焰

工作单位：中国科学技术大学

报告人简介：

熊焰，男，留美博士后、中国科学技术大学计算机学院教授、博士生导师，国际计算机学会ACM中国理事会常务理事、电子学报常务编委、中国通信学会通信软件专家委员会委员。1983年、1986年分别获得科大学士、硕士学位，1990年成为科大计算机系博士，1992-1994年任科大计算机系副主任，1995-1997年赴美UMKC大学计算机科学与通信学院做博士后研究。曾获得省部级科技进步奖二等奖2项、三等奖1项，安徽省青年科技奖1项。至今已在国内外核心期刊和学术会议上发表论文200多篇。先后主持的项目有国家自然科学基金项目、国家自然科学基金重点项目、国家863重大专项、国家863重大项目、国家863项目、国家973专题、中科院重大专项以及中科院国防创新基金等40多项国家和省部级项目。

报告摘要：

该报告简单介绍了网络安全协议的基本概念和典型的安全威胁；给出了安全协议最高安全评估标准的形式化验证三种方法以及国际上相关工作；描述了一个网络安全协议通用全自动形式化验证系统SmartVerif的基本思路、实现方法以及对比实验；该系统对于任意一个网络安全协议，给定一个安全目标，均可自动挖掘出其所有安全漏洞；它突破了网络有史以来安全协议无法通用全自动形式化验证的壁垒；最后，报告了该系统在区块链的应用情况以及未来软件和芯片自动形式化验证的进展。