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