报告题目：操作系统并发内存管理的形式化验证技术
报告人：赵永望 教授 浙江大学
报告时间：2020年12月15日 16:00—17:30
报告形式：线上报告
腾讯会议号：668 129 268
报告摘要：操作系统位于计算机系统软件栈的底层，其内存挂历Bug可能导致系统崩溃、被攻击、时间不确定性等问题，设计safety、security和real-time等问题。其次，操作系统的内存管理模块，它的算法和数据结构复杂，涉及复杂的内存计算、并关中断、任务调度等，内存管理代码的调试和测试难度大。一些隐藏的错误，尤其是并发性错误，用通畅的软件测试技术难以发现。本报告介绍一种并发操作系统形式化验证框架，支持功能正确性、功能安全和信息安全验证，并对Linux基金会Zephyr RTOS的并发内存管理进行了完整的形式化验证，发现了C代码中的3个严重bug。Zephyr内存管理模块采用基于开关中断的细粒度锁，支持多任务并发的内存分配与回收。本报告的工作是全球第一个对并发内存管理算法和C代码的形式化验证工作，最终提供了一套正确性和安全性的形式化证据。
报告人简介：林永望，浙江大学教授、博士生导师，曾任国际标准化组织ISO/IEC JTC1 SOA研究组组长、国家信标委分委会委员，起草4项ISO国际标准、12项国家标准。主要研究方向包括操作系统安全、形式化验证、编程语言等。提出了操作系统形式验证的系统性理论和方法，突破了覆盖单核到多核、标准到产品、模型到源码的形式化验证关键技术，完成了10多个国内外操作系统的形式验证工作，显著提升国产系统的安全可靠性。