全球顶级大佬来这儿只干一件事：解题下一代操作系统！

统信软件 2023-03-28

267

中国北京

2023/3/26

3月26日，以“开源创新”为主题的第十届开源操作系统年度技术会议（OS2ATC）正式拉开序幕，本次盛会由统信软件主办，清华大学、北京大学以及鉴释科技承办。

作为OS2ATC十周年的年度旗舰级活动，大会吸引了数百位国内外一线操作系统和相关领域的学者专家莅临现场，共同探讨下一代操作系统开源生态和技术前沿。

会议当天上午，统信软件高级副总经理、CTO张磊与国内外顶级高等学府、科技企业代表坐阵主会场，向全球开源爱好者传递领域内最新科技进展。

作为主会场主持人，张磊在开场致辞中表示：

“

海纳百川成其大，人集众智成其强。操作系统的创新升级与开源协作势在必行，而每年的OS2ATC都是全球操作系统爱好者开拓技术事业，提升行业认知的良好窗口。

”

随后来自哥伦比亚大学、北京大学、蚂蚁集团、清华大学、华为欧拉等在操作系统领域卓有建树的专家学者带来了精彩的年度技术报告：

虚拟机管理程序形式化验证

哥伦比亚大学教授顾荣辉发表《Microverification of the Linux KVM Hypervisor》主题演讲，他介绍了Linux KVM 虚拟机管理程序如何进行形式化验证的方法，即采用基于retrofit的微形式化验证，将 KVM 分解为core与serv两层，证明了微改造后 seKVM 的机密性与完整性。这不仅能带来技术优势，还能创造成本和能源优势。

基于大模型的编程自动化

北京大学教授李戈对当下火热的AIGC如何与操作系统技术结合进行剖析。针对程序生成与程序理解领域，李戈教授与北京大学软件研究所团队，从底层构建深度神经网络，从而成功实现了高效率的程序处理，成为全球第一个发表基于深度学习分析代码、生成代码论文的团队，比国外同类项目领先整整7年。在最近的aiXcoder XL版本上，其参数达到了130亿，已经能以很高的命中率生成整句的正确代码，如果达到千亿级别参数，并采用领域知识优化，将达成自然语言生成代码的能力。

同时李戈教授也表示，大模型的火热为科技创新打开了一扇新窗，但这背后需要大量的算力资源，目前算力使用仍存在成本和门槛问题，“算力+各行业”的赋能发展体系尚待推动。

Rust Monitor形式化验证

在之后的演讲中，蚂蚁集团安全计算平台负责人刘双表示在不依赖特殊安全硬件的前提下，Rust Monitor基于通用安全硬件原语，提供跨平台的TEE安全能力 (如:在海光平台上运行SGX Enclave)，并兼容已有TEE工具链和应用，核心代码经过形式化证明和权威机构检测，做到了安全可控。

内核漏洞挖掘技术

继刘双在演讲中提到的安全问题，清华大学张超教授系统阐述了内核漏洞挖掘技术的发展进展，近几年来自各方面的内核漏洞攻击层出不穷，如何“未雨绸缪”成为一个很大的命题。他分析几大代表性kernel fuzzing方案的优劣，并探讨了众多可行的改进措施。此外，张超教授与团队已经在安卓服务、驱动、竞态与macOS内核展开创新性模糊测试工作，并取得显著的工作成果，为相关技术演进路径指明方向。

多样性算力时代的OS形态思考

接下来，openEuler高级工程师张攀分享演讲，他表示，xPU（以GPU为代表）取代CPU成为了操作系统的C位，因此在多样性算力时代下，硬件将围绕互联+DSA创新计算架构，加速数据流动与提高并行度。而性能、灵活度、规模是多样性算力时代下软件面临的不可能三角，软件需要在三者中找到关键平衡。

基于表达式推导的人工智能编译器

清华大学副教授翟季冬在演讲时表示，人工智能芯片成为深度学习应用的主要计算力，但是算力需求对中国是非常大的挑战，所以编译器和中间的编程框架显得至关重要。翟季冬副教授提出将深度学习中传统等价算子变换拓展到不等价优化，并展开为算式优化，从而提供更大的优化空间与更好的优化成果，让算力在模型训练、推理过程中“物尽其用”。