Security vulnerabilities and mitigations

.github/workflows/ci.yaml

@@ -0,0 +1,53 @@
+name: CI
+on:
+  push:
+  pull_request:
+  # trigger a cron job every monday at 8am
+  schedule:
+    - cron: '00 08 * * MON'
+
+jobs:
+  matrix-gen:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{steps.list_tests.outputs.matrix}}
+    steps:
+      - uses: actions/checkout@v2
+      - id: list_tests
+        run: |
+          cd core/sim/rtl_sim/src/gap-attacks
+          MATRIX=$(ls *.s43 | sed 's:.s43*$::' | jq -cnR '[inputs | select(length>0)]')
+          echo $MATRIX
+          echo "::set-output name=matrix::$MATRIX"
+
+  bench:
+    name: ${{ matrix.target }}
+    runs-on: ubuntu-latest
+    needs: matrix-gen
+    strategy:
+      fail-fast: false
+      matrix:
+        target: ${{ fromJson(needs.matrix-gen.outputs.matrix) }}
+        runner: ['./run_gap']
+        include:
+          - target: ./run_all
+            runner: ''
+            never-fail: 1
+          - target: test-env
+            runner: './run_gap'
+            never-fail: 1
+
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v2
+      - name: Install dependencies
+        run: sudo apt-get install build-essential cmake iverilog tk binutils-msp430 gcc-msp430 msp430-libc msp430mcu expect-dev verilator -y
+      - name: Build sancus-core
+        run: mkdir build && cd build && cmake -DNEMESIS_RESISTANT=1 .. && cd ..
+      - name: Run test bench
+        env:
+          # mitigations applied upstream -> expect failure, unless explicitly declared as a non-attack test case
+          EXPECT_FAIL: ${{ (github.repository_owner == 'sancus-tee' || github.ref_name == 'mitigations') && matrix.never-fail != 1 }}
+        run: |
+          cd core/sim/rtl_sim/run/
+          ${{ matrix.runner }} ${{ matrix.target }}

CMakeLists.txt

@@ -14,9 +14,7 @@ set(FULL_INSTALL_SIM_PATH ${CMAKE_INSTALL_PREFIX}/${INSTALL_SIM_PATH})
 set(INSTALL_TOOLS_PATH "${INSTALL_DATA_PATH}/tools")
 set(FULL_INSTALL_TOOLS_PATH ${CMAKE_INSTALL_PREFIX}/${INSTALL_TOOLS_PATH})
 
-if (NOT NB_MODULES)
-    set(NB_MODULES 4)
-endif ()
+set(NB_MODULES 1)
 
 if (NOT SECURITY)
     set(SECURITY 64)

LICENSE

@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2021, openmsp430 and sancus-tee contributors
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of openmsp430 nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -1,46 +1,127 @@
-# Installation
+# Security analysis of Sancus_V
 
-The general installation instructions of Sancus can be found [here][sancus install].
-What follows are instructions to get everything up and running on Ubuntu (tested on 20.04).
+[![CI](https://github.com/martonbognar/sancus-core-gap/actions/workflows/ci.yaml/badge.svg)](https://github.com/martonbognar/sancus-core-gap/actions/workflows/ci.yaml)
+
+This repository contains part of the source code accompanying our [paper](https://mici.hu/papers/bognar2022gap.pdf) "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](https://github.com/martonbognar/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).
+
+**:heavy_check_mark: Continuous integration.**
+A full reproducible build and reference output for all of the Sancus_V attack
+experiments, executed via a cycle-accurate `iverilog` simulation of the
+openMSP430 core, can be viewed in the [GitHub Actions log](https://github.com/martonbognar/sancus-core-gap/actions).
+
+**:no_entry_sign: Mitigations.**
+Where applicable, we provide simple patches for the identified implementation
+flaws in a separate [mitigations](https://github.com/martonbognar/sancus-core-gap/tree/mitigations)
+branch, referenced in the table below.
+Note, however, that these patches merely fix the identified vulnerabilities in
+the Sancus_V 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 mismatch, missing attacker
+capabilities) 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 |
+|-----------------|---------------|:-------------:|-------------|
+| V-B1            | [B-1-dependent-length.s43](core/sim/rtl_sim/src/gap-attacks/B-1-dependent-length.s43) | [`e8cf011`](https://github.com/martonbognar/sancus-core-gap/commit/e8cf0114c9b3d2b823cd5a5f38e06da5049225ce) | Variable instruction length following `reti`. |
+| V-B2            | [B-2-maxlen.s43](core/sim/rtl_sim/src/gap-attacks/B-2-maxlen.s43) | [`3170d5d`](https://github.com/martonbognar/sancus-core-gap/commit/3170d5d6a4431db93bac4f11a7f91559f7c07620) | Instructions with execution time T > 6. |
+| V-B3            | [B-3-shadow-register.s43](core/sim/rtl_sim/src/gap-attacks/B-3-shadow-register.s43) | [`6475709`](https://github.com/martonbognar/sancus-core-gap/commit/64757098191824238df9a502f7fd8cfbcadb61b2) | Resuming an enclave with `reti` multiple times. |
+| V-B4            | [B-4-reentering-from-isr.s43](core/sim/rtl_sim/src/gap-attacks/B-4-reentering-from-isr.s43) | [`3636536`](https://github.com/martonbognar/sancus-core-gap/commit/3636536772baac7523d59fa3708df6b52518d267) | Restarting enclaves from the ISR. |
+| V-B5            | [B-5-multiple-enclaves.s43](core/sim/rtl_sim/src/gap-attacks/B-5-multiple-enclaves.s43) | [`b17b013`](https://github.com/martonbognar/sancus-core-gap/commit/b17b013e65411df1d557cc34a2c4f7c46ebf7a58) | Multiple enclaves. |
+| V-B6            | [B-6-untrusted-memory.s43](core/sim/rtl_sim/src/gap-attacks/B-6-untrusted-memory.s43) | [`d54f031`](https://github.com/martonbognar/sancus-core-gap/commit/d54f031b8705109509f598602899dec9c9dbd871) | Enclave accessing unprotected memory. |
+| V-B7            | [B-7-gie.s43](core/sim/rtl_sim/src/gap-attacks/B-7-gie.s43); [B-7-ivt.s43](core/sim/rtl_sim/src/gap-attacks/B-7-ivt.s43); [B-7-peripheral.s43](core/sim/rtl_sim/src/gap-attacks/B-7-peripheral.s43) | [`264f135`](https://github.com/martonbognar/sancus-core-gap/commit/264f135e9fb7d903a90933861cfb81d6d2fba51d) [`093f51c`](https://github.com/martonbognar/sancus-core-gap/commit/093f51c73abdd84fbb95165bd6100ab8315993a3) | Manipulating interrupt behavior from the enclave. |
+
+### Missing attacker capabilities
+
+| Paper reference | Proof-of-concept attack | Patch? | Description |
+|-----------------|---------------|:-------------:|-------------|
+| V-C1            | [sancus-examples/dma](https://github.com/sancus-tee/sancus-examples/blob/master/dma/main.c) | :x: | DMA side-channel leakage (see also note below). |
+| V-C2            | [C-2-watchdog.s43](core/sim/rtl_sim/src/gap-attacks/C-2-watchdog.s43) | [`c3dcf6e`](https://github.com/martonbognar/sancus-core-gap/commit/c3dcf6ef08d62e63ff66a8a69125abd66b7c892b) | Scheduling interrupts with the watchdog timer. |
+
+**:bulb: DMA side channel.** As explained in our paper, the Sancus_V implementation is
+based on an older version of the openMSP430 core without DMA capabilities.
+Hence, the DMA attack does _not_ directly affect the current version of Sancus_V, and we
+demonstrate the DMA side channel on the more recent (non-formalized) [upstream
+version of Sancus](https://github.com/sancus-tee/sancus-core/).
+Continuous integration for the DMA side-channel attack is, therefore,
+integrated in the separate
+[sancus-examples](https://github.com/sancus-tee/sancus-examples) repository,
+referenced in the table above.
+Also note that, as discussed in the paper, no straightforward mitigation
+(apart from disabling DMA completely) exists at this point for the DMA side channel.
+
+## Source code organization
+
+This repository is a fork of the upstream
+[sancus-core/tree/nemesis](https://github.com/sancus-tee/sancus-core/tree/nemesis)
+repository that contains the source code of a provably secure interruptible
+enclave processor, described in the following paper.
+
+> M. Busi, J. Noorman, J. Van Bulck, L. Galletta, P. Degano, J. T. Mühlberg and F. Piessens, "Provably secure isolation for interruptible
+enclaved execution on small microprocessors," in 33rd IEEE Computer Security Foundations Symposium (CSF), Jun. 2020, pp. 262–276.
+
+The original upstream Sancus_V system is accessible via commit
+[7c7d7fa](https://github.com/martonbognar/sancus-core-gap/commit/7c7d7fa9360439360d1eff0d26135c3d93a4b846)
+and earlier. All subsequent commits implement our test framework and
+proof-of-concept attacks.
+
+All of our attacks are integrated into the existing openMSP430 testing framework.
+Specifically, the [`core/sim/rtl_sim/src/gap-attacks/`](core/sim/rtl_sim/src/gap-attacks) directory contains one
+assembly file per attack (containing therein both the victim enclave and
+untrusted runtime attacker code), plus a corresponding Verilog stimulus file
+that validates the contextual equivalence breach.
+
+![sancus-v-overview](sancus-v-overview.png)
+
+## Installation
+
+The general installation instructions of Sancus can be found [here](https://github.com/sancus-tee/sancus-main).
+However, for our experiments we only need the Nemesis-resistant version of the Sancus core.
+All attacks are directly written in assembly, so we don't need any custom Sancus compiler or support software.
+
+What follows are instructions to get the experimental environment up and running on Ubuntu (tested on 20.04).
 
 - Prerequisites:
   ```bash
-  apt install cmake iverilog tk python3-pip libtinfo5
-  pip3 install pyelftools
-  ```
-- Patched Clang (needed for the Sancus compiler):
-  ```bash
-  wget https://distrinet.cs.kuleuven.be/software/sancus/downloads/clang-sancus_4.0.1-2_amd64.deb
-  apt install ./clang-sancus_4.0.1-2_amd64.deb
+  $ sudo apt install build-essential cmake iverilog tk binutils-msp430 gcc-msp430 msp430-libc msp430mcu expect-dev verilator
   ```
-- Sancus compiler:
+- Build Sancus core with Nemesis defense:
   ```bash
-  wget https://distrinet.cs.kuleuven.be/software/sancus/downloads/sancus-compiler_2.0_amd64.deb
-  apt install ./sancus-compiler_2.0_amd64.deb
-  ```
-- Sancus core with Nemesis defense:
-  ```bash
-  git clone --branch nemesis https://github.com/sancus-tee/sancus-core.git
-  mkdir build
-  cd build
-  cmake ..
-  make install
+  $ git clone https://github.com/martonbognar/sancus-core-gap.git
+  $ cd sancus-core-gap
+  $ mkdir build
+  $ cd build
+  $ cmake -DNEMESIS_RESISTANT=1 ..
+  $ cd ..
   ```
 
-# Running
+## Running the proof-of-concept attacks
 
-We have provided an [example](nemesis-example) to start experimenting with the Nemesis defense.
-It provides a Makefile so running it is easy:
-```bash
-cd nemesis-example
-make sim
-```
+**:bulb: Contextual equivalence.**
+As explained in the paper, the security definition of Sancus_V uses the notion
+of _contextual equivalence_. This means that our proof-of-concept attacks will
+have to distinguish two enclaves that can otherwise not be distinguished
+without interrupts. For this, our test framework compiles every victim enclave
+two times, once with an environment variable `__SECRET=0` and once with
+`__SECRET=1`. We consider the proof-of-concept attack successful if the
+attacker context (i.e., the untrusted code outside the enclave) unambiguously
+succeeds in telling whether it interacted with an enclave compiled with
+`__SECRET=1` or `__SECRET=0`.
 
-This produces a waveform in `sancus_sim.fst` which can be viewed with [GTKWave][gtkwave].
+To run all of the Sancus_V attacks, simply proceed as follows:
 
-The example uses the `timer_irq` function to precisely generate an interrupt while a Sancus module is executing.
-With the current value of 100, the interrupt is triggered during the third cycle of a 4-cycle instruction.
-Adapt the value to generate interrupts at different points during the execution of the module.
-
-[sancus install]: https://distrinet.cs.kuleuven.be/software/sancus/install.php
-[gtkwave]: http://gtkwave.sourceforge.net/
+```bash
+$ cd core/sim/rtl_sim/run/
+$ __SECRET=0 ./run_all_attacks
+$ __SECRET=1 ./run_all_attacks
+```

core/bench/verilog/sancus-def.v

@@ -0,0 +1,33 @@
+// for simulator testing purposes only
+
+wire        exec_done           = dut.frontend_0.exec_done;
+wire [15:0] pc_nxt              = dut.frontend_0.pc_nxt;
+wire [15:0] current_inst_pc     = dut.frontend_0.current_inst_pc;
+wire        gie                 = dut.frontend_0.gie;
+wire [8:0]  inst_so             = dut.frontend_0.inst_so;
+wire        inst_branch         = dut.frontend_0.inst_branch;
+wire        inst_irq_rst        = dut.frontend_0.inst_irq_rst;
+
+wire        handling_irq        = dut.execution_unit_0.handling_irq;
+wire        crypto_start        = dut.execution_unit_0.crypto.start;
+wire        crypto_busy         = dut.execution_unit_0.crypto.busy;
+
+wire        r2_z                = dut.execution_unit_0.register_file_0.r2_z;
+
+wire [15:0] sm_current_id       = dut.execution_unit_0.spm_control_0.spm_current_id;
+wire [15:0] sm_prev_id          = dut.execution_unit_0.spm_control_0.spm_prev_id;
+wire [15:0] sm_prev_cycle_id    = dut.execution_unit_0.spm_control_0.prev_cycle_spm_id;
+
+wire [15:0] sm_0_public_start   = dut.execution_unit_0.spm_control_0.omsp_spms[0].public_start;
+wire [15:0] sm_0_public_end     = dut.execution_unit_0.spm_control_0.omsp_spms[0].public_end;
+// wire [15:0] sm_1_public_start   = dut.execution_unit_0.spm_control_0.omsp_spms[1].public_start;
+wire [15:0] sm_0_secret_end     = dut.execution_unit_0.spm_control_0.omsp_spms[0].secret_end;
+wire        sm_0_enabled        = dut.execution_unit_0.spm_control_0.omsp_spms[0].enabled;
+// wire        sm_1_enabled        = dut.execution_unit_0.spm_control_0.omsp_spms[1].enabled;
+// wire        sm_2_enabled        = dut.execution_unit_0.spm_control_0.omsp_spms[2].enabled;
+wire [15:0] sm_0_id             = dut.execution_unit_0.spm_control_0.omsp_spms[0].id;
+// wire [15:0] sm_1_id             = dut.execution_unit_0.spm_control_0.omsp_spms[1].id;
+// wire [15:0] sm_2_id             = dut.execution_unit_0.spm_control_0.omsp_spms[2].id;
+wire        sm_0_executing      = dut.execution_unit_0.spm_control_0.omsp_spms[0].executing;
+// wire        sm_1_executing      = dut.execution_unit_0.spm_control_0.omsp_spms[1].executing;
+// wire        sm_2_executing      = dut.execution_unit_0.spm_control_0.omsp_spms[2].executing;

core/bench/verilog/tb_openMSP430.v

@@ -189,6 +189,9 @@ reg                stimulus_done;
 // CPU & Memory registers
 `include "registers.v"
 
+/* Sancus-specific register/wire definitions */
+`include "sancus-def.v"
+
 // Debug interface tasks
 `include "dbg_uart_tasks.v"
 

core/rtl/verilog/omsp_execution_unit.v

@@ -95,7 +95,8 @@ module  omsp_execution_unit (
     handling_irq,
     irq_num,
     sm_irq_save_regs,
-    sm_irq_restore_regs
+    sm_irq_restore_regs,
+    sm_irq_busy
 );
 
 // OUTPUTs
@@ -149,6 +150,7 @@ input               handling_irq;
 input         [3:0] irq_num;
 input               sm_irq_save_regs;
 input               sm_irq_restore_regs;
+input               sm_irq_busy;
 
 
 //=============================================================================
@@ -259,7 +261,8 @@ omsp_register_file register_file_0 (
     .reg_incr     (reg_incr),     // Increment source register
     .scan_enable  (scan_enable),  // Scan enable (active during scan shifting)
     .sm_irq_save_regs(sm_irq_save_regs),
-    .sm_irq_restore_regs(sm_irq_restore_regs)
+    .sm_irq_restore_regs(sm_irq_restore_regs),
+    .sm_executing(sm_executing)
 );
 
 
@@ -534,6 +537,7 @@ omsp_spm_control #(
   .write_key              (sm_write_key),
   .key_in                 (crypto_data_out),
   .key_idx                (sm_key_idx),
+  .sm_irq_busy            (sm_irq_busy),
   .violation              (sm_violation),
   .spm_data_select_valid  (sm_data_select_valid),
   .spm_key_select_valid   (sm_key_select_valid),