Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.

翻译：低信任架构从软件视角看，始终对已加密数据进行操作，并将硬件信任量显著降低至一个不含软件的微型飞地组件。本文对一种特定低信任架构——隔离加密（SE）架构——进行了完整的正式验证，证明该设计能抵御所有可能程序下的直接数据泄露和数字侧信道攻击。我们首先定义了SE低信任架构的指令集架构（ISA）安全需求。向上看，该ISA作为硬件对软件的抽象，用于证明任何由这些指令组成的程序无法泄露信息（包括通过数字侧信道）。向下看，该ISA是硬件的规范，用于定义由ISA级安全需求产生的任何RTL实现的证明义务，覆盖功能安全与数字侧信道泄露两方面。接着，我们展示了如何借助商业形式化验证工具成功履行这些证明义务。我们通过SE架构的七种正确及含缺陷实现，验证了所提RTL安全验证技术的有效性。