简介
论坛将主要研讨机密计算对工业界AI产业的价值与影响。着眼于机密计算辅助AI计算的安全-性能-开销平衡这一重要问题。当前，大模型等AI应用逐渐成为互联网产业的潮流，工业界也逐渐注重AI对其产业发展（例如信息处理、代码编程、智能交互）的重要性，然而在该过程中，难免存在机密信息泄露等问题。因此，本论坛将“机密计算与AI产业结合”这一面向实际场景的、影响广泛的作为论坛选题，将着重讨论机密计算这一系统安全领域重要技术与大语言模型等AI产业结合的现实问题，机密计算对大语言模型中token、隐私保护的重要性，将机密计算实际落地部署于企业云平台的难点与挑战，并为国内互联网产业数据安全发展提供重要参考。
简介为官网原文，部分内容可能未写完。
人员
主席
- 冯登国 · 中国科学院软件研究所
- 张锋巍 · 南方科技大学
嘉宾
- 秦宇 · 中科院软件研究所
- 丁滟 · 国防科技大学
- 赵永望 · 浙江大学
- 张磊 · 南湖实验室
- 郭力维 · 电子科技大学
- 侯锐 · 中国科学院信息工程研究所
- 郭御风 · 飞腾信息技术有限公司
- 闫守孟 · 蚂蚁集团
- 吴烨 · 字节跳动
- 金意儿 · 华为技术有限公司
- 应志伟 · 海光信息技术股份有限公司
报告安排
开场致辞
冯登国 · 中国科学院软件研究所
面向零信任的机密AI技术与系统
秦宇 · 中科院软件研究所
简介
自2019年机密计算联盟成立推动标准化以来，机密计算技术与人工智能融合发展，逐步从理论走向产业实践。当前机密AI已进入快速发展阶段，苹果、谷歌、Anthropic等科技巨头相继推出基于硬件TEE的端云协同机密AI产品，如苹果的PCC、谷歌的PAC和Claude机密推理系统CIS，实现大模型推理的数据可用不可见，以及模型+数据双重机密性保护。同时多条CPU/GPU TEE技术路线并行发展，机密计算正深度融入AI推理、Agent可信执行等核心应用场景，成为保障大规模敏感数据处理的关键技术底座。本报告聚焦机密AI的安全防护技术和系统，一方面通过TEE与TPM双信任根确保AI推理环境可信，实现用户推理上下文的隔离与封装存储；另一方面提出面向机密Agent的零信任架构，实现机密Agent复合身份认证与差分证明，最后介绍我们在这一研究领域的部分技术实现和系统成果。
面向大模型推理的机密计算技术研究
丁滟 · 国防科技大学
简介
随着大模型与智能体技术的广泛落地，其安全性问题日益凸显。基于处理器可信执行环境（TEE）的机密计算技术，为保障智能计算中的模型资产安全与数据隐私提供了切实可行的方案，正成为当前的研究热点。本报告将重点介绍团队在该领域取得的关键进展，主要包括：大模型推理过程的TEE机密保护方法、面向智能计算的TEE环境性能优化，以及基于新一代ARM CCA架构的轻量级机密容器构建等技术，有效构建面向大模型的机密智能计算技术体系，并积极推进在国产处理器平台上的应用落地。
面向 GPTEE 标准的可信执行环境形式化验证技术
赵永望 · 浙江大学
简介
可信执行环境（Trusted Execution Environment，TEE）作为现代计算系统中的核心安全机制，通过提供隔离执行环境来保护敏感数据与关键计算过程，其安全性直接关系到用户隐私与系统可信度。尽管已有多种 TEE 产品被提出并广泛应用于移动支付、指纹识别与数字内容保护等关键场景，但现有实现普遍缺乏严格、系统化的安全保障机制。近年来，研究者逐步将形式化方法引入 TEE 安全分析，通过严格的数学证明以实现信息流安全等关键性质的保障，但从安全规范到系统实现的全链路形式化仍面临一系列关键挑战。本报告从GPTEE PP安全规范建模与验证、GPTEE系统及MiTEE实例建模与验证、到自动化证明三个层面系统性地研究了面向GPTEE标准的 TEE 的形式化验证问题。首先，针对 GPTEE PP 缺乏形式化语义的问题，提出了 ProveriT，一个参数化、可组合且经过形式化验证的安全规范模型，通过基于横向演算与纵向演算的可组合框架，对规范中的推导关系进行了全面验证，并在此过程中发现并修正了 8 个潜在问题，保障了GPTEE PP的正确性与一致性。其次，针对GPTEE系统建模验证复杂的问题，本报告提出了 Tacco框架。该框架面向CC认证需求，引入基于域切换的建模机制。同时，通过参数化方法统一建模可信应用，支持多 TA 协同与生命周期管理。基于该框架，我们建模并验证了GPTEE及其实例MiTEE，并在验证过程中发现了4 个关键安全漏洞并修复。该研究帮助 MiTEE 通过了 CC EAL 5+ 认证。最后，针对形式化验证过程中证明成本高的问题，本报告提出了 HybridProver，一种结合大语言模型的自动定理证明框架。HybridProver 采用双模型协同机制，将完整证明生成与基于策略的逐步生成方法相结合，并结合自动化证明工具进一步提升正确性与效率。通过在 Isabelle 环境下进行实验，HybridProver 在 miniF2F 数据集上取得了 59.4% 的证明成功率，达到领先水平，并将该框架应用于前述 TEE的安全规范和系统的形式化建模与验证任务中，有效降低了人工证明成本。
面向大模型的机密计算集群框架技术与应用
张磊 · 南湖实验室
简介
本报告介绍面向大模型推理的机密计算集群框架。基于机密集群管控面机制、统一化的远程证明、集群透明加解密等多维技术，有效解决了集群管控面与节点运行性能、安全与兼容问题。框架应用于大模型推理、知识库运营、机密Token等各类实际应用场景。
机密设备驱动
郭力维 · 电子科技大学
简介
Arm可信执行环境（Trusted Execution Environment，TEE）普遍缺乏对于复杂多元IO设备的驱动支持，难以在TEE内端到端访问复杂IO设备，实现安全IO。为解决该问题，我们提出了一种全新的TEE设备驱动设计思想—最小可用设备驱动，即微驱动。有别于设备驱动移植等传统软件复用手段，微驱动将设备驱动按照不同的IO功能垂直划分，通过记录重放的方式复用其IO功能对应的软硬件交互事件；该方式隐式地复用了设备内部状态机的状态转换路径，从而达到实现相同IO功能的效果。微驱动首次在Arm TEE中实现了对MMC、CSI摄像头以及多个USB设备类总计共10个不同设备的完整访问，相关成果发表于EuroSys、OSDI等CCF-A类会议
思辨环节---产业落地panel主持人
侯锐 · 中国科学院信息工程研究所
思辨环节---产业落地panel
郭御风 · 飞腾信息技术有限公司
思辨环节---产业落地panel
闫守孟 · 蚂蚁集团
思辨环节---产业落地panel
吴烨 · 字节跳动
思辨环节---产业落地panel
金意儿 · 华为技术有限公司
思辨环节---产业落地panel
应志伟 · 海光信息技术股份有限公司