时间：2022年11月28日 19：30—21：00
地点：腾讯会议 302-776-585
主讲人：赵永望，浙江大学计算机科学与技术学院教授
主持人：张倩颖，首都师范大学beat365官网副教授
主办单位：beat365官网
主讲人简介：
赵永望，浙江大学 教授、博士生导师，移动终端安全浙江省工程研究中心主任，工信部重大专项首席科学家，CCF杰出会员，CCF系统软件专委、形式化方法专委和抗恶劣计算专委执行委员，国际ARINC653操作系统标准委员会成员等。主要研究方向为形式化验证、系统安全、编程语言等，主持和参与工信部重大专项、国家自然基金重点项目、载人航天工程重点项目、浙江省尖兵计划项目等二十余项，获省部级科技进步一等奖2项。相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。提出了操作系统形式验证的系统性理论和方法，已应用到十多个国产操作系统和国外工业/开源操作系统中，显著提升国产系统的安全可靠性。
主讲内容简介：
在安全关键领域，IEC 61508、DO-178C、Common Criteria等标准对关键系统的安全性提出很高的要求，其中，形式化方法是高安全级别认证的必要手段。形式化方法是采用数理逻辑方法进行系统规约、开发和验证的一种方法，已经在航空航天等关键领域得到成熟应用，近年来也逐步应用到互联网领域，包括Amazon、Google、Microsoft等都在规模化地使用该方法。本报告主要介绍软硬件系统安全的概念、要求和面临的挑战，分析对比各类系统安全验证方法。然后，介绍形式化方法的技术框架，以及国内外最新的发展趋势和应用情况。最后，分析当前系统安全形式化验证面临的问题，从自动化的角度讨论可能的研究方向以及我的一些探索。