CCF软件大会2026 | Rust与系统软件论坛

二、论坛组织委员会

• 陈   渝     （清华大学）

• 冯   洋     （南京大学）

• 徐   辉     （复旦大学）

三、论坛安排

日程安排：

时间：2026年11月6日，09:00~12:00

地点：天津市社会山国际会议中心酒店  四层5号多功能厅

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：张毅  vivo系统研发总监

题目：Rust筑牢底座，AI驱动未来：vivo蓝河操作系统的探索与实践

摘要：vivo蓝河操作系统的Rust全栈落地实践，探索AI时代操作系统研发之道。蓝河操作系统是vivo面向通用人工智能时代自主研发的智慧操作系统。本次演讲将深入介绍蓝河操作系统基于Rust语言实现全栈落地的架构设计思路和工程化实战经验，涵盖操作系统内核、Harness、图形、UI框架、工具链等关键技术的探索与成果。听众将了解Rust在操作系统全栈研发中的架构设计、工程实践与性能优化经验，并获得关于AI时代操作系统研发方向的思考与启示。

简介：张毅，vivo系统研发总监。拥有10多年的操作系统研发经验，负责vivo蓝河操作系统（BlueOS）的架构设计及研发工作。作为团队核心成员，长期专注于蓝河操作系统核心方向的技术架构设计和中长期规划，积极推动Rust语言在软硬件生态中的融合应用，并致力于促进蓝河操作系统技术与产业实践的结合。

2. 报告人：刘昱玮 博士 蚂蚁技术研究院助理研究员

题目：大模型驱动的 Rust 形式化验证：从证明生成到验证工程自动化

摘要：形式化验证能够为系统软件提供严格的正确性保障，但在真实软件仓库中，规约编写和证明构造仍需要大量人工投入。特别是对于 Rust 操作系统等复杂系统软件，跨模块依赖、项目特定的证明知识以及验证工具链的持续演进，使得大规模自动化验证面临诸多挑战。本报告将介绍 KVerus，一种面向仓库级 Rust 程序的大模型辅助形式化验证方法。KVerus 通过依赖感知的代码上下文构建、语义化证明知识检索以及验证器反馈驱动的迭代修复，实现复杂代码仓库中的自动化证明生成，并已在真实 Rust 操作系统 Asterinas 的验证实践中取得成效。

在此基础上，报告还将介绍 KVerus 的后续改进，包括将验证能力封装为可组合的智能体 Skills、自动生成程序规约代码（Specification）与证明代码（Proof），以及通过验证器反馈精简冗余证明代码。最后，结合 Asterinas 的形式化验证仓库 VOSTD 的实际验证实践，探讨大模型辅助形式化验证从单一证明生成走向完整、可维护的验证工程自动化的机遇与挑战。

简介：刘昱玮，博士，蚂蚁技术研究院研究人员。2024 年获中国科学院大学软件工程博士学位，曾在蚂蚁科技集团博士后科研工作站与中国科学院软件研究所联合开展博士后研究。

主要研究方向包括系统软件可靠性、漏洞挖掘、程序分析与形式化验证，近年来重点关注大语言模型驱动的系统软件分析、自动化测试与形式化验证技术。相关研究成果发表于 S&P、CCS、ICSE、ASE 等系统安全与软件工程领域国际学术会议。

3. 报告人：周睿 中级工程师

题目：内核界的“乐高”：用 Rust 组件按需拼装多形态内核

摘要：面向嵌入式、AI 边缘计算及智能体任务执行对轻量、高效、可裁剪内核的需求，TGOSKits 以 Rust 可复用组件为基础，支撑 Unikernel、Linux 兼容内核与 Hypervisor 等系统形态，通过编译期装配和清晰接口实现按需定制与跨系统复用。项目以单向依赖、能力接口和安全责任分层组织组件，收敛高风险操作与 unsafe 边界，并结合项目规则、领域技能和自动化验证，为人工与大模型提供职责明确、约束清晰的开发环境。本报告重点介绍其如何以可组合架构降低内核定制复杂度，以安全边界和工程约束降低人机协同开发风险。

简介： 泉城省实验室工程师，TGOSKits 开源项目负责人，资深 Rust 开发者。主要研究方向包括操作系统内核、虚拟化、驱动框架及系统软件架构，长期活跃于 Rust 开源生态，具有丰富的底层系统研发与开源项目实践经验。

4. 报告人：饶子豪 复旦大学博士生

题目：基于安全属性的 Rust 程序验证

摘要：Rust 中 unsafe 操作的正确使用需要满足指针有效性、内存初始化、访问边界等安全条件。这些条件往往以自然语言描述，且涉及复杂的控制流程与对象状态变化，难以直接用于自动化验证。本报告围绕安全属性的表达、传播与检查，介绍基于安全属性的 Rust 程序验证方法。通过结构化建模将安全要求转化为可检查的规约，明确接口前置条件与类型不变量；结合程序依赖分析，追踪相关属性在函数调用和状态变化中的建立与保持；利用路径敏感分析与约束求解，检查程序实现是否满足安全契约。报告将结合标准库及开源项目中的典型案例，展示从属性规约到验证条件生成与检查的过程，并讨论方法的适用范围。此外，将探索接入大语言模型，辅助规约理解与验证结果分析。

简介：饶子豪，复旦大学计算机科学与技术专业博士研究生，研究方向为程序设计语言与软件工程，重点关注 Rust 程序安全、静态分析及人工智能辅助软件工程，开展安全属性建模、缺陷检测与自动化验证研究。曾获上海开源创新卓越成果奖特等奖、开放原子大赛 Rust 语言研究与创新应用赛一等奖。

5. 报告人：马全一 前华为和腾讯的高级技术专家

题目：基于 Rust 的 Monorepo 架构体系实现

摘要：在 Agent 时代，以 Git 为体系的版本管理体系受到巨大的冲击，Monorepo 成为主流的选择。从 Google 到 Meta 等传统互联网巨头、从  Anthropic 到 OpenAI 等 AI 时代新贵，都不约而同的选择了 Monorepo 作为内部的版本管理方案。但是当前业界并没有 Git 兼容的 Monorepo 开源解决方案，本次演讲讨论如何使用 Rust 编程语言构建 Git 兼容的 Monorepo 解决方案，并且尝试构建 Rust 编译器开发环境的实践。

简介：马全一，前华为和腾讯的高级技术专家，开源社区运营总监，专注在云原生、操作系统、Rust 编程语言、版本管理等技术领域。

五、论坛组织委员会简介

1. 论坛组委会：陈渝 长聘副教授

简介：陈渝老师长期从事操作系统、系统软件与安全关键基础设施方向研究，在操作系统结构、系统可靠性以及面向新型系统编程语言的系统构建方法方面具有深厚积累。其研究强调通过语言机制与系统机制协同设计提升系统软件的安全性与可验证性，推动将Rust引入操作系统与基础软件栈，在保证性能的同时降低传统C/C++系统软件中的内存错误与未定义行为风险。相关工作聚焦系统级抽象、运行时支撑以及安全关键软件工程方法，为Rust在高可信系统中的落地提供了重要的系统化视角。

2. 论坛组委会：冯洋 准聘副教授

简介：冯洋老师的研究聚焦Rust软件工程、编译与程序分析、自动化测试与缺陷检测等方向，致力于构建面向Rust生态的质量保障技术体系。其工作探索如何利用静态分析、语言服务器信息及智能化方法，从Rust API与注释中提取语义约束并生成高质量测试，以提升Rust软件的工程可靠性与可维护性。冯洋老师的相关研究以“语言机制 + 工程工具链”为核心，关注Rust在真实工业项目中的可测试性、语义理解与自动化质量保障问题，是推动Rust从“安全语言”走向“可规模化工程语言”的重要研究内容。其研究对于提升系统级软件的可靠性、质量和语言特性适配实践具有重要指导意义，与 Rust 语言在系统软件领域追求安全性与高可靠性的目标高度契合。

3. 论坛组委会：徐辉 准聘副教授

简介：徐辉长期从事Rust安全性分析、程序分析与系统安全方向研究，是国际上较早系统性研究Rust真实安全问题的学者之一。其代表性工作通过分析Rust生态中全部已知内存安全漏洞案例，发现内存安全问题仍可能出现在不安全代码或抽象误用场景，并总结出典型缺陷模式，为Rust安全工程提供实证基础。进一步研究提出面向Rust资源管理语义的静态分析方法（如SafeDrop）以检测错误释放问题，表明Rust所有权模型在自动资源回收场景下仍需工程化验证与工具支持。此外，相关工作还研究Rust与C/C++通过FFI交互时的跨语言内存管理缺陷，并设计静态分析工具检测边界错误。这些成果揭示Rust并非“天然安全即可放心使用”，而是需要系统化的软件工程方法来支撑其在关键系统中的正确应用。