ADL 133 《安全系统软件》开始报名-线上线下同步举办

CCF学科前沿讲习班

The CCF Advanced Disciplines Lectures

CCFADL第133期

主题 安全系统软件

2022年11月11日-11月13日 北京

本期CCF学科前沿讲习班ADL133《安全系统软件》，将对安全系统软件的最新进展进行深入浅出的讲解，从约束求解、定理证明、安全程序设计语言等不同的学科视角和操作系统、嵌入式系统、并发反应式系统等不同系统软件领域视角为听众介绍安全系统软件的关键技术和前沿研究。相信学员经过本次讲习班，能够深入了解安全系统软件的基础技术、主要挑战和应用场景，开阔科研视野，增强实践能力。

本期ADL讲习班邀请了7位来自国内外著名高校与企业科研机构活跃在前沿领域的专家学者做主旨报告/专题讲座。第一天，钟林教授的主旨报告将讲解安全嵌入式系统挑战操作系统的基本设计原则，蔡少伟研究员将介绍可满足性问题的编码与求解，詹博华副研究员将介绍交互式定理证明的原理和应用（第一部分）。第二天，陈海波教授的主旨报告将从一个实践者的视角讨论形式化方法与系统软件，詹博华副研究员将继续介绍交互式定理证明的原理和应用（第二部分），赵永望教授将介绍并发反应式系统形式化验证的理论技术与工具案例。第三天，陈渝副教授将探讨Rust编程语言是否能挑战C在OS上的地位，李屹博士将讲解形式化验证工程化的历史，经验与愿景。通过三天教学，旨在带领学员实现对安全系统软件从基础技术，到前沿科研动态，再到典型实践场景的深入学习与思考。

学术主任：谢涛 讲席教授 北京大学 / 胡振江 讲席教授 北京大学

主办单位：中国计算机学会

协办单位：高可信软件技术教育部重点实验室（北京大学）

本期ADL主题《安全系统软件》由CCF会士、软件工程专委副主任北京大学谢涛教授和北京大学胡振江教授担任学术主任，邀请到钟林（教授，耶鲁大学）、陈海波（教授, 上海交通大学）、蔡少伟（研究员, 中国科学院软件研究所）、詹博华（副研究员，中国科学院软件研究所）、赵永望（教授，浙江大学）、陈渝（副教授，清华大学）、李屹（华为操作系统内核实验室工程师，华为）7位专家做主旨报告/专题讲座。

活动日程：

特邀讲者：

钟林，教授，耶鲁大学

讲者简介：钟林，1994至1998年在清华大学电子系无线电与信息系统专业学习；1998至2000年在线路与系统教研组，师从刘润生教授，获得硕士学位。2000至2005年在普林斯顿大学学习，获电气工程博士学位。2005至2019年在莱斯大学电气与计算机工程系任教。2020年加入耶鲁大学。以对有机发光显示驱动设计的贡献当选IEEE Fellow, 以对移动和网络系统设计的贡献当选ACM Fellow。研究工作还获得了NSF CAREER Award，ACM SIGMOBILE新秀奖，ASPLOS、MobiSys (3)、PerCom and MobileHCI最佳论文奖以及ACM SIGMOBILE的时间检验奖。

主旨报告题目： 安全嵌入式系统挑战操作系统的基本设计原则

报告摘要：主流操作系统从UNIX继承了几大设计原则：基于进程的虚拟内存，拥有特权的内核，运行时系统内检查。这些原则在硬件资源受限的嵌入式系统上很难实施。这个报告分享我们最近几年在利用Rust语言实现操作系统，重新思考这些原则的一些结果，以及如何利用Rust的类型系統降低形式化验证的工作量。

陈海波，特聘教授，上海交通大学

讲者简介：陈海波，上海交通大学特聘教授、博导，并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任，国家杰出青年基金获得者，ACM杰出科学家。主要研究领域为操作系统、分布式系统与系统安全，研究成果通过产学研深度结合被应用到十亿级设备，产生了广泛的学术与产业影响。曾获教育部技术发明一等奖、全国优秀博士学位论文奖、中国青年科技奖、CCF青年科学家奖等。目前担任OpenHarmony技术指导委员会首任主席、CCF系统软件专委会副主任、ACM旗舰杂志Communications of the ACM首位中国学者编委与领域共同主席。研究工作还获得了华为卓越贡献个人奖，ASPLOS、EuroSys、VEE等最佳论文奖以及DSN的时间检验奖。按照csrankings.org的统计，其近5年（2018～2022）在操作系统领域高水平会议（SOSP/OSDI、EuroSys、USENIX ATC和FAST）上发表的论文数居世界第一。

主旨报告题目：形式化方法与系统软件：一个实践者的视角

报告摘要：对高可靠性系统软件的需求不断增加使得形式方法在工业界引起了广泛的兴趣。微软、亚马逊、华为等企业纷纷加强对形式方法领域的投入。在这个报告中，我将介绍近年来我和同事们在将形式化方法应用在系统软件的一些实践与体会。具体来说，我将介绍形式化方法在设计和实现操作系统、同步原语、文件系统、数据库系统和共识协议等方面的尝试。基于这些实践，我将进一步描述在大规模系统中应用形式化方法的经验和教训，并讨论在促进学术界和工业界之间更好的协同作用方面可能面临的挑战和机遇。

蔡少伟，研究员，中国科学院软件研究所

讲者简介：蔡少伟，中科院软件所研究员、博导、中科院优秀导师，获得国家优秀青年基金资助。主要研究约束求解、组合优化以及EDA（电子设计自动化）验证工具。在命题逻辑可满足性问题（SAT）、可满足性模理论（SMT）问题、最大可满足性问题（MaxSAT）等国际比赛多次获得冠军，在国际EDA比赛获得亚军；提出可满足性问题的混合搜索方法，解决了命题逻辑推理与搜索方向十大挑战的第7个挑战，获得SAT会议最佳论文奖。在EDA、软件验证、云计算、排班、智慧园区等领域展开了系列项目。相关成果发表在CAV，ICSE，IJCAI，CP，SAT等会议和Artificial Intelligence等期刊上。

专题讲座题目： 可满足性问题：编码与求解

讲座摘要：可满足性问题要求判定一个逻辑公式是否存在使之为真的赋值。其中命题逻辑可满足性（SAT）是计算机科学的核心问题之一，可满足性模理论（SMT）问题是限定背景理论的一阶逻辑公式判定问题。SAT和SMT求解器作为形式化工具的底层引擎，在软硬件验证中有重要作用。本报告介绍SAT和SMT的编码以及求解技术，主要包括CDCL方法和局部搜索方法，并介绍相关的前沿进展和挑战。

詹博华，副研究员，中国科学院软件研究所

讲者简介：詹博华的研究方向是形式化方法。2014年博士毕业于普林斯顿大学数学系，之后在麻省理工学院和慕尼黑工业大学任博士后。2018年加入中科院软件所，现任副研究员。主要工作包括证明自动化方法和交互式定理证明器的设计与实现，嵌入式系统的建模与验证方法，以及在程序验证、操作系统、分布式系统、量子程序验证的应用。在CAV, IJCAR/CADE, TACAS, ITP, J. Automated Reasoning等形式化方法领域的主要会议和期刊发表文章30余篇。

专题讲座题目：交互式定理证明：原理和应用

讲座摘要：交互式定理证明指的是通过用户和计算机之间的交互构造数学证明。这些证明可以关于数学定理，也可以关于各种计算机软硬件系统的正确性和安全性。交互式定理证明已被用于验证非常复杂的计算机系统，包括整个操作系统微内核和编译器。本报告将介绍交互式定理证明的底层原理和现有应用，希望回答以下常见问题：为什么我们可以信任在交互式定理证明器中完成的证明？相比于其他验证技术，交互式定理证明有哪些优势和局限性？未来需要什么样的技术来突破这些局限性？

赵永望，教授，浙江大学

讲者简介：赵永望，浙江大学 教授、博士生导师，移动终端安全浙江省工程研究中心主任，工信部重大专项首席科学家，CCF杰出会员，CCF系统软件专委、形式化方法专委和抗恶劣计算专委执行委员，国际ARINC653操作系统标准委员会成员等。主要研究方向为形式化验证、系统安全、编程语言等，主持和参与工信部重大专项、国家自然基金重点项目、载人航天工程重点项目、浙江省尖兵计划项目等二十余项，获省部级科技进步一等奖2项。相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。提出了操作系统形式验证的系统性理论和方法，已应用到十多个国产操作系统和国外工业/开源操作系统中，显著提升国产系统的安全可靠性。

专题讲座题目： 并发反应式系统形式化验证：理论技术与工具案例

讲座摘要：系统多核化、网络化、服务化的发展趋势下，现代高安全系统大多是并发反应式系统，例如操作系统、控制系统、业务流程系统等。这类系统的形式化验证仍然面临很多的挑战，包括复杂多样的并发系统机制，支持多语言集成以覆盖需求、设计、源代码等层面，真实并发系统验证所需的强大工具支持等。针对这些问题，本报告介绍一种并发反应式系统验证的方法PiCore，采用事件驱动的方式支持抢占、中断、资源锁等并发机制的建模，同时提出PiCore语言的并发霍尔逻辑，支持Rely-Guarantee方式的组合验证。其次，在Isabelle/HOL定理证明器中实现了PiCore语言及其逻辑系统，采用“适配器”的设计模式，实现了多种形式化语言的“零修改”集成，目前已集成了Isabelle/HOL工具的HOL-Hoare_Parallel库、并发编程和验证语言CSimpl。最后，介绍两个真实案例：Zephyr RTOS并发内存管理的形式化验证、业务流程语言BPEL到PiCore的编译及正确性验证。

陈渝，副教授，清华大学

讲者简介：陈渝，国防科学技术大学本硕博毕业，清华大学计算机系长聘副教授，博导，MIT 访问学者，CCF 系统软件 专委常务委员。主要研究方向操作系统，编译原理，程序分析，系统可靠性与性能优化等。先后负责和参与了二十多余项国内外课题的开发，包括国家自然科学基金项目、863 项目、核高基项目等，获得国家科 技进步二等奖和省部级一等奖。发表高水平学术论文 50 余篇，担任国内外有影响力学术会议的主席和程序 委员会委员等。承担清华大学计算机系的操作系统、编译原理、高级操作系统等课程的教学工作。

专题讲座题目：Rust编程语言与操作系统 -- Rust能挑战C在OS上的地位吗？

讲座摘要：介绍编程语言与硬件系统结构的历史与发展对操作系统内核及其应用的影响；分析操作系统内核在语言层面当前面临的挑战和解决方法；介绍基于Rust系统编程语言的操作系统的特点；最后讨论编程语言关联的系统软件研发与应用的新趋势，以及对如何建立操作系统生态环境的一些思考。

李屹，华为操作系统内核实验室工程师，华为

讲者简介：李屹，华为操作系统内核实验室工程师，博士毕业于北京大学数学科学学院信息科学系。主要研究方向包括软操作系统形式化验证，超低时延软件开发，模型驱动开发等方向。

专题讲座题目：形式化验证的工程化：历史，经验与愿景

讲座摘要：使用形式化验证来保障软件的安全性，是一个经久不衰的课题。但是形式化验证在实际工程中如何更好地运用，造福开发者或产生商业价值，目前仍然处在“百家争鸣”的状态。操作系统是基础软件栈的底座，利用形式化验证技术来提升操作系统的安全性和可靠性在实践中有很重要的意义。华为操作系统内核实验室在操作系统内核形式化验证方面有着多年的投入和积累，我们结合自身的实践，分享在形式化验证工程化中所遇到的挑战以及我们的相应对策与思考，希望与大家交流共勉。

学术主任：

谢涛，讲席教授，北京大学

谢涛，北京大学讲席教授，高可信软件技术教育部重点实验室（北京大学）副主任。曾任美国伊利诺伊大学香槟分校（UIUC）计算机科学系正教授。当选欧洲科学院外籍院士、国际计算机学会（ACM）会士、电气电子工程师学会（IEEE）会士、美国科学促进会（AAAS）会士、中国计算机学会（CCF）会士。曾获科学探索奖，国家自然科学基金委海外杰青及其延续资助，ACM软件工程领域（SIGSOFT）杰出服务奖，IEEE软件工程领域（TCSE）杰出服务奖等。担任CCF软件工程专委会副主任，2020年中国计算机大会程序委员会主席，ICSE 2021程序委员会共同主席，《软件测试、验证与可靠性（STVR）》Wiley期刊联合主编等。

胡振江，讲席教授/计算机学院院长，北京大学

胡振江，北京大学讲席教授、计算机学院院长。日本东京大学信息工学专业博士，先后担任东京大学情报理工学研究科助理教授和副教授，日本国立信息学研究所教授/系主任， 东京大学情报理工学研究科教授，是海外杰出青年科学基金获得者，胡振江长期从事程序设计语言和软件科学与工程的研究，并取得了突出的研究成果，被评为21世纪先驱科学家（日本科学技术振兴机构），日本工学会会士，国际计算机学会（ACM）杰出科学家，电气与电子工程师协会（IEEE）会士，欧洲科学院院士，日本工程院院士。

时间：2022年11月11日-13日

线下地址（疫情允许的情况下）：北京•中科院计算所四层报告厅（北京市海淀区科学院南路6号）

线上地址：报名交费成功后，会前三天通过邮件发送线上会议号和密码。

报名须知：

1、报名费：CCF会员2800元，非会员3600元。食宿交通费用自理。根据交费先后顺序，会员优先的原则录取，额满为止。疫情期间，根据政府疫情防控政策随时调整举办形式（线上线下同步举办、线上举办），线上线下报名注册费用相同。

2、报名截止日期：11月9日。报名请预留不会拦截外部邮件的邮箱，如qq邮箱。

3、咨询邮箱 : adl@ccf.org.cn

缴费方式：

在报名系统中在线缴费或者通过银行转账：

银行转账（支持网银、支付宝）：

开户行：招商银行北京海淀支行

户名：中国计算机学会

账号：110943026510701

请务必注明：ADL133+姓名

报名缴费后，报名系统中显示缴费完成，即为报名成功。

报名方式：请选择以下两种方式之一报名：

1、扫描（识别）以下二维码报名：

2、点击报名链接报名：https://conf.ccf.org.cn/ADL133

相关阅读：

ADL132《数字前端设计综合EDA技术》开始报名-线上线下

ADL135《智能语音交互技术》开始报名-线上线下同步举办