本文针对高保证密码学协议形式化验证实现中存在的性能瓶颈问题，提出了一套通用的优化方法。以 Line-Point 零知识证明（LPZK）协议为案例，首先在 EasyCrypt 中实现了一个形式化验证的 LPZK 实现（未考虑性能），然后通过三步优化获得高达 3000 倍的加速，最终性能与手动优化版本 lpzkv2 相当。三步优化包括：修改算法规范以减少计算复杂度、采用可证明安全的并行执行模型、以及优化内存访问结构。每一步优化都在 EasyCrypt 中形式化验证，并自动合成可执行代码。论文详细分析了每步优化带来的性能提升，并讨论了自动化安全证明和代码合成面临的挑战。该工作表明，通过系统的形式化优化，可以在不牺牲安全性保证的前提下显著提升验证密码学实现的性能，为高保证密码学的大规模应用提供了可行的技术路径。

本文研究了在 Blackwell GPU 机密计算（GPU-CC）环境下，LLM 推理服务性能显著下降的根本原因。作者在 NVIDIA RTX Pro 6000 和 B300 HGX 两个平台上进行了实验，发现性能瓶颈并非来自 GPU 计算本身（B300 上 BF16 矩阵乘法性能几乎无损失），而是来自机密虚拟机与 GPU 之间的通信桥接。在 Intel TDX 和 GPU-CC 的联合部署下，LLM 服务吞吐量损失 13-27%，KV-cache 恢复延迟增加一倍以上。通过深入分析，作者指出 GPU-CC 将主机与设备之间的数据传输变成了一个串行化、高设置开销的通道：安全拷贝无法获得 CUDA 流内的并发性，异步传输在运行时边界阻塞，小规模数据交换需要固定的开销。这与现代推理运行时（如 vLLM）依赖廉价、并发、异步 DMA 的假设相悖。在 vLLM 密集解码场景中，差距主要来自 44 倍更慢的小分配和拷贝操作；通过针对性补丁排除了其他原因。作者提出了一种调度标志（恢复 57% 的差距）和工作线程排空（在高并发下最多恢复 92% 的差距）两种方法。同样的桥接模型也解释了 KV 恢复惩罚增加 131% 和模型加载速度减慢 34 倍的现象。此外，论文还验证了 Blackwell 平台上多 GPU 机密租户（包括 CVM 内 510 GB/s NVLink P2P 和并发隔离租户）的能力，并指出了生产级机密 AI 平台尚需解决的远程证明缺口。本文适合系统安全工程师、AI 基础设施开发者和云服务提供商阅读。