Security analysis of VRASED

This repository contains part of the source code accompanying our paper "Mind the Gap: Studying the Insecurity of Provably Secure Embedded Trusted Execution Architectures" to appear at the IEEE Symposium on Security and Privacy 2022. More information on the paper and links to other investigated systems can be found in the top-level gap-attacks repository.

M. Bognar, J. Van Bulck, and F. Piessens, "Mind the Gap: Studying the Insecurity of Provably Secure Embedded Trusted Execution Architectures," in 2022 IEEE Symposium on Security and Privacy (S&P).

✔️ Continuous integration. A full reproducible build and reference output for all of the VRASED attack experiments, executed via a cycle-accurate iverilog simulation of the openMSP430 core, can be viewed in the GitHub Actions log. We also integrated VRASED's machine-checked proofs into the CI framework, showing that our attacks remain entirely undetected by the current proof strategy.

🚫 Mitigations. Where applicable, we provide simple patches for the identified implementation flaws in a separate mitigations branch, referenced in the table below. Note, however, that these patches merely fix the identified vulnerabilities in the VRASED reference implementation in an ad-hoc manner. Specifically, our patches do not address the root cause for these oversights (i.e., in terms of preventing implementation-model mismatches, missing attacker capabilities, deductive errors) and cannot in any other way guarantee the absence of further vulnerabilities. We provide more discussion on mitigations and guidelines in the paper.

Overview

Implementation/model mismatches

Paper reference	Proof-of-concept attack	Patch?	Description
VI-B1	B-1-dma-translation.sh	1ae6d1a	Leak full key[0:63] via incorrect DMA address translation.
VI-B2	B-2-key-size.sh	fa806f7	Leak key[31:63] via inconsistent key sizes.
Appendix-C-1	A-1-register-leak.sh	bdc42f3	Leak uncleared caller-save registers after SW-Att execution.

Missing attacker capabilities

Paper reference	Proof-of-concept attack	Patch?	Description
VI-C1	apex-gap repository	❌	Secure metadata corruption with a peripheral.
VI-C2	C-2-stack-pointer.sh	8fdc298	Leak key[0:21] with stack pointer poisoning.
VI-C3	C-3-auth-timing.sh	531db52	Leak authentication token with start-to-end timing.
VI-C4	C-4-nemesis.sh	70e2bf4	Leak authentication token with Nemesis side channel.
VI-C5	C-5-dma-sc.sh	621f2a8	Leak authentication token with DMA side channel.

Deductive errors

Paper reference	Proof-of-concept attack	Patch?	Description
VI-D	N/A (see paper)	❌	Missing assumptions about the core.

Source code organization

This repository is a fork of the upstream sprout-uci/vrased repository that contains the source code of a verifiable remote attestation hardware-software co-design, described in the following paper.

I. D. O. Nunes, K. Eldefrawy, N. Rattanavipanon, M. Steiner, and G. Tsudik, "VRASED: A verified hardware/software co-design for remote attestation," in 28th USENIX Security Symposium, 2019, pp. 1429–1446.

The original upstream VRASED system is accessible via commit 4a29c24 and earlier. All subsequent commits implement our test framework and proof-of-concept attacks.

⚠️ VRASED derivatives. Multiple derived architectures have been published that are directly derived from the open-source VRASED research prototype and use its security arguments as the basis of their own. At the time of writing, open-source VRASED-based security architectures include RATA (CCS'21), APEX (USENIX'20), and PURE (ICCAD'19). While we only validated the attacks in this repository on the original VRASED base architecture, they may similarly affect these derived architectures.

Attack code and experimental setup

Our attacks are integrated into the untrusted VRASED wrapper code. Specifically, we extended the untrusted VRASED invocation code in wrapper.c. The required attack code is selected using C precompiler directives, depending on the value of __ATTACK (i.e., a number between 1 and 7, set in the top-level attack runner script in the scripts directory).

VRASED includes an alternative, and similarly verified, version of HW-Mod to optionally support verifier authentication (cf. paper). Unfortunately, however, while the added functionality to support verifier authentication is rather minimal, the two versions of HW-Mod do not share a unified implementation nor proof code base. Our continuous integration setup, hence, runs all (applicable) attacks against both the default hw-mod and the alternative hw-mod-auth. Results for both versions of HW-Mod can be viewed in the GitHub Actions log.

⚠️ HW-Mod-Auth. Importantly, our experiments revealed several divergences and additional shortcomings of the verified HW-Mod-Auth module:

• HW-Mod-Auth does not monitor the irq signal and, hence, does not comply with the explicit VRASED atomicity design requirement. This important requirement also seems to be entirely missing from the HW-Mod-Auth LTL requirements, and therefore this implementation oversight was not caught by the proof. (Also note that, in the absence of resets on interrupts, the C-4-nemesis side-channel attack, of course, does not apply to HW-Mod-Auth).
• The HW-Mod-Auth implementation (but not proof, cf. below) interestingly appears to have been parameterized with the correct key size, making the optional HW-Mod-Auth resistant against attack B-2-key-size.
• The proof accompanying HW-Mod-Auth does currently not succeed: it was incorrectly parameterized with wrong KMEM_SIZE and CTR_SIZE parameters that are out-of-sync with the implementation. This could have been detected, as the current proof fails for the accompanying implementation, even generating insightful counterexamples (cf. continuous integration logs).

Installation

The original installation instructions of VRASED can be found here.

What follows are minimal instructions to get the experimental environment up and running on Ubuntu (tested on 20.04).

• Prerequisites:

  $ sudo apt-get install bison pkg-config gawk clang flex gcc-msp430 iverilog expect-dev libffi-dev tcl bc

• Checkout VRASED:

  $ git clone https://github.com/martonbognar/vrased-gap.git
  $ cd vrased-gap

• Optional: following steps are only needed when you want to run VRASED with our mitigations:

  $ git checkout mitigations
  $ mkdir build
  $ cd build
  $ cmake ..
  $ cd ..

Running the proof-of-concept attacks

To run the VRASED attacks, simply proceed as follows:

$ cd scripts
$ ./B-1-dma-translation.sh # or select other attack scripts in this directory