12月15日:赵永望
发布时间:2020-12-14  阅读次数:1129

报告题目操作系统并发内存管理的形式化验证技术

报告人:赵永望 教授  浙江大学

报告时间:2020121516:0017: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多个国内外操作系统的形式验证工作,显著提升国产系统的安全可靠性。

华东师范大学软件工程学院
www.sei.ecnu.edu.cn Copyright Software Engineering Institute
院长信箱:yuanzhang@sei.ecnu.edu.cn | 院办电话:021-62232550 | 学院地址:上海中山北路3663号理科大楼