本文针对可信执行环境（TEE）与低层语言（如 LLVM IR）结合时面临的安全分区问题展开研究。TEE 通过 enclave 提供硬件级隔离，但仅依靠它无法保证信息流安全；LLVM 这类语言允许不受限制的指针操作和非结构化控制流，进一步加剧了信息泄漏风险。同时，手工将应用划分成 enclave 部件与非 enclave 部件既繁琐又易错，且缺乏细粒度控制。作者提出一种三步走方案：首先形式化基于 LLVM IR 的 enclave 无关演算 SIR，设计新型宽松类型系统，结合信息流控制与安全感知的粗粒度内存安全，以抵御低级攻击者；然后将 SIR 扩展为 enclave 感知演算 SIREN，其非干涉性保证能抵御可观察任意非 enclave 内存的更强攻击者；最后实现类型驱动、类型保持的 SIR 到 SIREN 编译，自动生成安全的 enclave 感知程序，消除了手工分区过程，同时保持对 host-enclave 边界的细粒度控制。文中实现了 SPLITR 工具，并在 Intel SGX 硬件上用 13 个微基准和现实负载（包括 SGXGauge 应用）进行评测；SPLITR 能扩展到 OpenSSL（425,953 条 LLVM IR 指令），支持在 enclave TCB 大小、host-enclave 转换次数、边界数据移动量等目标之间权衡。对于 OpenSSL，面向转换次数优化可将其从 393 降为 187。运行时开销方面，短时运行负载主要被固定的 enclave 开销主导，而长时运行应用能更好地摊销这些开销，接近原生性能。该研究的最重要贡献是首次为 LLVM 系语言提供安全构造的自动分区形式化框架，并为编译优化、硬件隔离结合信息流控制提供了可行的工程验证。

本文面向可信执行环境（TEE）中飞地程序的安全性问题，特别是状态连续性（State Continuity）的验证，提出了一种形式化验证方法。状态连续性指飞地程序在执行过程中，即使遭遇异常中断、迁移或恶意系统软件干扰，其内部状态仍能保持一致和完整。作者基于程序逻辑和定理证明技术，构建了状态连续性的形式化模型，定义了验证规则，并可能使用了自动化工具进行验证。该研究有助于从数学上保证飞地程序的状态安全，防止回滚、重放等攻击。论文的主要贡献包括状态连续性属性的精确刻画、验证框架的设计与实现，以及基于典型飞地应用的案例研究。这项工作对TEE安全研究者和开发可信应用的安全工程师具有重要参考价值。

该论文围绕机密 Serverless 计算中的安全挑战，提出了一种“可复用 Enclave”机制。在无服务器计算场景下，每次函数调用通常需要创建或加载一个受信任执行环境（TEE/Enclave），这带来显著的启动延迟和资源开销；同时，不同函数之间的隔离策略也影响安全性和性能。论文的核心思路是让多个租户或函数安全地复用同一个 Enclave 实例，通过细粒度的内存隔离、密钥管理和生命周期控制，在保证机密性和完整性的前提下减少冷启动成本。文中可能设计了一套运行时架构和调度协议，并基于主流 TEE 平台（如 Intel SGX）进行原型实现。实验部分可能通过微基准测试和端到端工作负载对比，证明该方法能有效降低函数调用延迟、提升吞吐量，同时维持与独立 Enclave 相当的安全边界。该研究对构建高效、可扩展的机密 Serverless 平台具有参考价值，也引发了关于共享 Enclave 中攻击面扩张、侧信道隔离和故障隔离的进一步讨论。由于仅基于标题与摘要信息，具体技术细节和实验数据需结合原文确认。

本文针对受信执行环境（TEE）中严格内存模型导致的性能瓶颈问题，提出了一种新的内存模型——Elasticlave。传统TEE（如Intel SGX）采用空间隔离模型，强制enclave之间不能共享内存，导致数据拷贝开销巨大，性能降低1-2个数量级。Elasticlave允许enclave选择性地、临时地与其它enclave乃至操作系统共享内存，从而消除昂贵的数据拷贝操作，同时仍能保持与空间隔离模型相当的应用所需安全性。作者在基于RTL设计的周期级RISC-V核上实现了Elasticlave原型，实验表明，在相同处理器配置下，相比空间隔离模型可获得1-2个数量级的性能提升。Elasticlave的可信计算基（TCB）很小，其性能特性和硬件面积开销随所支持的共享内存区域数量扩展良好。该研究为TEE内存模型设计提供了新思路，适合系统安全与硬件架构领域的研究人员阅读。

本文提出 EXIA（External-Input Attestation），一种针对飞地（enclave）可信过渡的机制。飞地技术（如Intel SGX）旨在保护代码和数据免受底层操作系统或管理程序的攻击，但飞地在执行过程中可能涉及状态改变（如从安全域切换到非安全域，或在不同飞地间转移），这种过渡往往需要依赖外部输入。EXIA 通过对外部输入进行认证（attestation）来确保过渡过程的可信性，防止恶意外部输入破坏飞地的安全边界。论文给出了形式化模型和原型实现，评估了性能开销。该研究面向使用飞地技术的安全开发者，有助于设计更健壮的信任链。