Cryptographically Assured Information Flow: Assured Remote Execution

TL;DR

Cryptographically Assured Information Flow (CAIF) is a hardware mechanism to enable Assured Remote Execution, akin to existing Trusted Execution Environments, but securely implements an ideal functionality for logging and confidential escrow.

Abstract

Assured Remote Execution on a device is the ability of suitably authorized parties to construct secure channels with known processes -- i.e. processes executing known code -- running on it. Assured Remote Execution requires a hardware basis including cryptographic primitives. In this paper, we show that a simple hardware-level mechanism called Cryptographically Assured Information Flow (CAIF) enables Assured Remote Execution. CAIF is akin to some operations in existing Trusted Execution Environments, but securely implements an ideal functionality defined in terms of logging and confidential escrow. We show how to achieve Assured Remote Execution for a wide variety of processes on a CAIF device. Cryptographic protocol analysis demonstrates our security goals are achieved even against a strong adversary that may modify our programs and execute unauthorized programs on the device. Assured Remote Execution enables useful functionality such as trustworthy remote attestation, and provides some of the support needed for secure remote reprogramming.

Figures (6)

• Figure 1: caif Hardware Cryptography Components
• Figure 2: Implementation theorem proof strategy: Lemmas \ref{['lem:a-u']} and \ref{['lem:p-u']} bound the last term
• Figure 3: Metal room activity, symmetric anchoring
• Figure 4: Distributor request
• Figure 5: Message $m_3$ signed with delegated key; ${\textcolor{darkgreen}{\star}}$ authenticated channel

Theorems & Definitions (11)

• Definition 1
• Lemma 1
• Lemma 2
• Lemma 3
• Definition 2
• Definition 3
• Definition 4: caif properties
• Lemma 4: Attestation unforgeability
• Lemma 5: Protection unforgeability
• Theorem 1