Software Fault Isolation for Robust Compilation

面向类型的容错非干扰编译

Type-Directed Compilation for Fault-Tolerant Non-Interference

环境噪声（如热、电离粒子等）会导致硬件中的瞬时故障，从而导致存储值损坏。任务关键型设备需要通过容错来减轻此类故障-容错是一种旨在保留系统功能行为的技术组合，尽管存在瞬时故障的破坏性影响。容错通常具有很高的部署成本--可能需要特殊的硬件来实现它--并且提供弱的统计保证。它还基于故障很少的假设。在本文中，我们考虑的情况下，安全性，而不是功能的正确性，是要保护的主要资产。我们的贡献是双重的。首先，我们开发了一个理论，用于表示在存在瞬时故障的数据的机密性。我们表明，自然概率定义的安全故障的存在下，可以捕获的可能性定义。此外，可能性的定义是由一个已知的基于互模拟的属性，称为强安全性。其次，我们说明了一个简单的RISC架构，只有代码存储器和程序计数器的容错这些结果的效用。我们提出了一个类型导向的编译方案，产生RISC代码从一个更高层次的语言，其中强安全举行-即良好类型的程序编译为RISC代码，这是安全的，尽管瞬态故障。与容错解决方案相比，我们的技术假设相对较少的特殊硬件，给出正式的保证，并在存在主动攻击者的情况下工作，主动攻击者积极地针对系统的部分并精确地引发故障。

基于受控故障注入的软件故障隔离实证安全分析

Empirical Security Analysis of Software-based Fault Isolation through Controlled Fault Injection

本研究提出一种通过受控故障注入模拟SFI安全边界的测试技术，在V8堆沙箱中发现19个可绕过沙箱的安全漏洞。

进入、退出、页错误、泄漏：测试微架构泄漏的隔离边界

Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks

针对CPU微架构侧信道易被忽略导致隔离不完整的问题，开发扩展基于模型的关系测试（MRT）方法的压力测试工具，检测到新泄漏并验证方法有效性，推动处理器安全验证从被动转向主动。

软件故障隔离系统的自动化形式化验证

Automated Formal Verification of a Software Fault Isolation System

本文针对软件故障隔离验证器可能存在健全性缺陷的问题，对轻量级故障隔离（LFI）系统进行了自动化形式化验证，证明其接受的程序不会在指定沙箱区域外读写内存。

Lightning: Striking the Secure Isolation on GPU Clouds with Transient Hardware Faults

GPU clouds have become a popular computing platform because of the cost of owning and maintaining high-performance computing clusters. Many cloud architectures have also been proposed to ensure a secure execution environment for guest applications by enforcing strong security policies to isolate the untrusted hypervisor from the guest virtual machines (VMs). In this paper, we study the impact of GPU chip's hardware faults on the security of cloud "trusted" execution environment using Deep Neural Network (DNN) as the underlying application. We show that transient hardware faults of GPUs can be …

使用微策略的完全抽象编译器：相互不信任组件的安全编译

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components

安全编译可以防止对编译代码的所有低级攻击，并允许对源语言的安全性进行合理的推理。在这项工作中，我们提出了一个新的攻击者模型的安全编译，扩展了众所周知的概念，充分的抽象，以确保保护相互不信任的组件。我们设计了一个编译器链（编译器，链接器和加载器）和一个新的安全监视器，共同抵御这种强大的攻击模型。该监视器是使用最近提出的，通用的基于标签的保护框架，称为微策略，它配备了硬件支持高效缓存和形式化验证方法。我们的监视器保护抽象的一个简单的面向对象的语言-类隔离，方法调用的纪律，和类型安全-对任意低级别的攻击者。