蒲戈光

个人简介：华东师范大学教授博导，CCF 形式化专委副主任 研究方向为形式化方法、软件工程。承担了科技部重点研发、核高基等 10 余项目，近五年在软工与形 式化方法顶会发表论文 20 余篇，曾获 ACM 杰出论文奖。获上海市科技进步特等奖、教育部自然科学 一等奖等多项省部级奖项。

贺 飞

个人简介：清华大学副教授，CCF 形式化专委常委 研究方向为形式化验证理论、方法及应用。在包括 POPL, CAV, PLDI, OOPSLA 等在内的国际重要会议 和期刊上发表论文 60 余篇。获 ACM SIGSOFT 2018 杰出论文奖，入选北京市高等学校"青年英才计划"。

赵永望

报告题目：安全攸关操作系统形式化验证：技术与应用实践

报告摘要：安全攸关操作系统主要应用于航空、航天、轨道交通、无人系统等领域，它位于计算机系 统软件栈的底层，操作系统的错误可能导致系统崩溃、被攻击、时间不确定性等问题，涉及功能安全、 信息安全等问题。操作系统功能结构复杂，多核多任务的并发度高，开发与调试都十分困难，一些隐 藏的错误用常见的软件测试技术难以发现，而形式化验证可帮助软件开发人员发现深层的错误，确保 操作系统的高安全可靠性。本报告主要讨论操作系统形式化验证的背景意义、国内外现状和面临的挑战， 介绍我们团队提出的系统方法、理论技术以及真实应用实践。

个人简介：担任 ARINC653 国际操作系统标准委员会委员、国际信息技术安全评估标准 (Common Criteria,CC) 操作系统内核技术委员会委员、CCF 系统软件专委会和形式化方法专委会委员。主要研究 方向包括操作系统安全、形式化验证、编程语言等。提出了操作系统形式验证的系统性理论和方法， 突破了覆盖单核到多核、标准到产品、模型到源码的形式化验证关键技术，完成了 10 多个国内外操作 系统的形式验证工作，显著提升国产系统的安全可靠性。相关研究成果得到美国波音、法国空客和国 际知名实时操作系统厂商的认可，被纳入国际标准，并在开源实时操作系统社区产生影响力。

吴志林

报告题目：安全协议的状态机建模、验证与代码生成

报告摘要：本报告将介绍形式化方法在安全协议 (security protocol) 开发中的应用。我们开发了一个使 用状态机对安全协议进行建模、验证和代码生成的集成工具套件 ISADT。ISADT 允许对安全协议的控 制逻辑和交互流程使用状态机进行建模，然后使用开源工具 Proverif 对安全协议的信息安全性质进行 形式验证，最后从安全协议的状态机模型自动生成最终的代码。ISADT 通过形式验证保证安全协议设 计的安全性，通过代码自动生成提高了开发效率，并且减少了人工编码所导致的实现缺陷。我们使用 ISADT 针对一些典型的安全协议进行了实例研究，发现了一个终端高安全接入控制协议的设计缺陷， 并得到了协议设计者的确认。

个人简介：中国科学院软件研究所计算机科学国家重点实验室研究员，博士生导师， "CCF-IEEE CS" 青年科学家奖获得者。博士毕业于中国科学院软件研究所计算机科学国家重点实验室，先后在中国科 学院自动化研究所中法计算机科学、自动化与应用数学联合实验室和法国波尔多第一大学 LaBRI 实验 室从事博士后研究。2014-2015 在巴黎第七大学 IRIF 实验室担任国家留学基金委公派访问学者。长期 从事计算逻辑、自动机理论、程序验证相关的研究，在知名国际会议和期刊上发表论文 30 余篇，包括 LICS、POPL、CAV、Information and Computation、IJCAR、CADE、CONCUR 等。先后主持多项国 家级项目，包括"十三五"全军共用信息系统装备预先研究项目、国家自然科学基金面上基金等；同时 参与国家重点研发计划项目和国家自然科学基金面上基金项目多项。中国计算机学会形式化方法专业 委员会委员，国际会议 ATVA、ICECCS、LATA、GandALF 等国际会议的程序委员会委员。

苏 亭

报告题目：移动应用软件的自动化测试：从崩溃错误到功能错误

报告摘要：移动应用软件是一类以图形界面为交互、事件驱动的软件，其功能多样、运行环境复杂（如 不同设备型号、系统版本和资源限制）。该类软件用户基数往往很庞大，市场竞争激烈，保证其可靠 性和正确性对商业成功、团队信誉、用户忠实度具有重要意义，然而对其实现自动化测试极具挑战性。 以安卓软件为例，截至 2020 年 1 月，安卓系统已占据移动市场超过 74% 的份额，每月全球活跃用户数 超过 20 亿，每个月新增移动软件超过 2 万多个，自动化测试需求巨大。本报告将介绍我们团队在该领 域内多年的研究成果，重点介绍我们提出的两类自动化测试方法、技术和工具，分别用于发现移动应 用软件中的崩溃错误和功能错误。这两类测试方法已帮助众多安卓软件发现了大量未知软件错误。

个人简介：现为华东师范大学软件工程学院教授。主要的研究方向为软件工程、程序语言和软件安全， 并一直致力于解决各类复杂软件系统的可靠性问题，特别是针对移动应用软件、工控嵌入式软件、编 译器和程序分析软件的自动化测试和验证。目前已发表 20 篇国际顶级会议和期刊论文（CCF-A），包 括 PLDI、ICSE、ESEC/FSE、ASE、TSE、CSUR。研究成果获得了三项 ACM SIGSOFT 杰出论文奖（ICSE 2018, ASE 2018, ASE 2019）。针对移动软件的研究获得了 Google 教授研究奖（2019）、ACM SIGSOFT 杰出论文奖（ICSE 2018）、全国软件原型工具竞赛一等奖（NASAC 2017）、ACM 学生学术竞赛第一 名（ICSE 2016）；帮助腾讯微信、Google Gmail/Google+ 发现了多个软件错误。针对工控嵌入式软件 的研究成果已转化为 SmartRocket Unit 单元测试工具，服务于十余家国内大型企业的软件生产部门。

赵 鲁

报告题目：杜绝关键安全漏洞——形式化验证无缓冲区溢出的应用实践和挑战

报告摘要：业界常用渗透测试和静态源码分析来检测软件产品中的安全漏洞，可是这些方法都存在无 法忽视的漏报和误报。对于软件系统里面有着高安全风险的模块来说，如何保证它们没有某些特定的 高危漏洞是一个学术界和业界共同的研究和实践难题。本工作介绍 SecVerifier 验证平台，它用形式化 验证技术来保证华为产品代码里面没有缓冲区溢出这一安全风险极高、后果极严重的漏洞。它完成了 十几万行代码的自动验证，发现了 60+ 缓冲区溢出和 30+ 空指针引用漏洞。它验证成功的代码保证了 没有缓冲区溢出问题。尽管如此，我们依然面临着复杂的技术挑战，希望和有关的研究人员共同解决 这些难题。

个人简介：2012 年在尤他大学获得计算机博士学位。曾先后在硅谷担任 HP Fortify 高级应用安全工程师， Oracle/NetSuite 担任首席应用安全工程师，和创业公司 Secregen 的 CTO。主要工作和研究方向为应用 程序的安全分析，包括形式化验证、静态和动态程序分析技术，和它们在程序安全分析中的综合应用。 作为核心成员参加业界领先的静态源码分析工具 Fortify SCA 研发，主持了 NetSuite 云服务安全代码审 核周期和流程，开发了独立企业证书管理和通信系统。曾获得多个在软件安全分析领域的美国和国际 专利。引领华为的形式化验证软件安全项目和静态安全分析工具项目。