• SHUFFLE
  • Directory Structure
  • Resources Requirement
  • Installation
    • Setup the repository
    • Environment Setup
      • Option A (recommended): Docker
      • Option B: Manual Installation
    • Build the Dependencies
  • Toy Example
  • Reproducing Experiments
    • SISP
    • DelayFwd-All
    • DelayFwd-Transmitter
  • Claims
    • Claim 1
    • Claim 1: Script
    • Claim 1: Expectation
    • Claim 2
    • Claim 2: Script
    • Claim 2: Expectation
    • Claim 3
    • Claim 3: Script
    • Claim 3: Expectation

SHUFFLE

This is an anonymous artifact for S&P 2026 submission.

Directory Structure

• huf/: HUF abstraction plugin
• patches/: Patches for rIC3 / BOOM
• scripts/: Workflow scripts
• src/: Verification tasks, each verifying some property on some CPU

To be cloned:

• rIC3/: rIC3 model checker
• chipyard/
  • generators/boom/: BOOM core

To be output:

• results/: Runtime directories for verification tasks
• figures/: Output figures

Resources Requirement

The storage requirement for this artifact is 64GB.

If operating on public infrastructure (e.g., SPHERE), verify that the primary volume has sufficient storage before proceeding. If it does not, follow instructions in Option A to relocate Docker and containerd data to a larger drive.

You will need a minimum of 16GB of RAM, though 32/64GB are highly recommended.

Installation

Setup the repository

Clone the repositories to create a workspace ~/shuffle under your home directory:

# Method 1: zip file (from Zenodo)
curl -LO https://zenodo.org/records/19270884/files/shuffle-artifact-0.1.0.zip
unzip shuffle-artifact-0.1.0.zip
mv shuffle-artifact-0.1.0 ~/shuffle
cd ~/shuffle
# Method 2: git clone
cd ~
git clone https://github.com/MATCHA-MIT/shuffle
cd shuffle

# Clone rIC3 from public release
git clone -b v1.4.0 https://github.com/gipsyh/rIC3.git

# Clone chipyard from public release
git clone -b 1.13.0 https://github.com/ucb-bar/chipyard.git

Environment Setup

We recommend using Docker if you are on x86_64 platform. Alternatively, you can manually install the dependencies. After this section, we will assume that you are executing commands in you preferred environment.

Option A (recommended): Docker

First, install Docker following the official document.

Then, build and start a Docker container.

cd ~/shuffle
docker-compose up -d
# If `docker-compose` is not available, try `docker compose` instead.

You can attach an interactive shell to the running container using the command below. Multiple shells can be attached to the same container simultaneously.

docker-compose exec dev zsh

The whole workspace is be mounted at ~/shuffle in the container.

(Optional) Redirect Docker storage to a larger drive

If the primary storage volume has insufficient space, and an additional larger drive is available, Docker and containerd data directories can be relocated to that drive using the steps below. This may be useful for testing the artifact on public infrastructures.

These steps assume the target drive is mounted at /mnt/data, and that all commands are executed in a Unix shell.

1. Stop Docker and containerd:
   • sudo systemctl stop docker
   • sudo systemctl stop containerd
2. Create and setup a storage directory for Docker:
   • mkdir -p /mnt/data/docker
   • Set the permission: sudo chown -R root:root /mnt/data/docker
   • Configure Docker: Create or edit /etc/docker/daemon.json and fill in the key-value pair:

     {
       "data-root": "/mnt/data/docker"
     }

3. Create and setup a storage directory for containerd:
   • mkdir -p /mnt/data/containerd
   • Set the permission: sudo chown -R root:root /mnt/data/containerd
   • Configure containerd: Update /etc/containerd/config.toml to include the following lines:

     root = "/mnt/data/containerd"
     state = "/run/containerd"

4. Restart Docker and containerd:
   • sudo systemctl start containerd
   • sudo systemctl start docker

Option B: Manual Installation

Here is the detailed setup instruction that install components separately.

• Yosys. We suggest following the official Building Yosys instructions to build yosys from source. The version we used is 0.54.

• Rust Nightly.

• Conda. As suggested by chipyard, we use Miniforge.

• Python dependencies. Please refer to scripts/setup/environment.yml for the list.

Build the Dependencies

In a shell of your chosen environment, run these commands to apply patches and build the dependencies:

cd ~/shuffle/huf
make -j

cd ~/shuffle/rIC3
git submodule update --init --recursive
patch -p1 < ~/shuffle/patches/rIC3.patch
cargo b --release

cd ~/shuffle/chipyard
./build-setup.sh -s 6 -s 7 -s 8 -s 9
# Note: It is expected that conda setup may print lots of "INFO:root:" and stall for a while.

Toy Example

We provide a toy example to test if the artifact setup is successful. The toy proves SISP on a very simple processor.

Under ~/shuffle/src/ToySISP, you can find

• core.sv: The simple processor
• top.sv: The self-composition circuit encoding SISP property
• uf.yml: HUF abstraction configuration

To start the proof:

cd ~/shuffle

DUV=ToySISP
RUN=testrun
UF=uf.yml

# Apply HUF abstraction
make DUV=$DUV RUN=$RUN UF=$UF build
make DUV=$DUV RUN=$RUN UF=$UF build-rp -j

# Start the proof
python3 -m scripts.proof run $DUV $RUN

To print the final results of the proof:

python3 -m scripts.proof status $DUV $RUN

The expected output is shown as follows. You will find the verification result of (1) the top-level proof (a.k.a. "main proof"), (2) refinement proofs, and (3) longest proof.

 [Main Proof] Proved  (frame=2, time=0.00s)
 [Multiplier] Proved  (frame=2, time=1.24s)
Found 1 refinement proof(s). 1 are non-default HUF
Overall status: Proved
Longest proofs:
                           [Max Refinement] [Multiplier] Proved  (frame=2, time=1.24s)
                                [Max Proof] [Multiplier] Proved  (frame=2, time=1.24s)

You can investigate the verification task in ~/shuffle/results/ToySISP/testrun/:

• The abstracted self-composition circuit (top-level proof) is at top.dump.
• Refinement proofs are under uf_po/.
• Invariants are at inv-ToySISP-testrun.txt.

Reproducing Experiments

This artifact reproduces the verification time and invariant analysis of three case studies (setups) in the paper.

1. Proving SISP on BOOM (all sizes)
2. Proving Sandboxing on BOOM (all sizes) with defense DelayFwd-All
3. Proving Sandboxing on BOOM (TinyBOOM) with defense DelayFwd-Transmitter

Note: You cannot run the three setups in parallel. They share a single chipyard directory with conflicting patches, so be sure to finish a setup and unpatch chipyard before moving on to the next one.

SISP

Estimated Time: ~1 hour

First, apply a patch that prepares BOOM for proving SISP.

cd ~/shuffle/chipyard
patch -p1 < ~/shuffle/patches/chipyard-SISP.patch

Then, start the proofs on all BOOM sizes by running the following command. Use --nproc to specify the level of parallelism (try reducing it if you encounter out-of-memory errors). This may take a while depending on your PC's performance.

cd ~/shuffle
python3 -m scripts.run all SISP --nproc=16

While the proofs are running, you can use another shell to probe the progress, or draw figures based on the currently available results.

cd ~/shuffle
# Probe the progress
python3 -m scripts.run all SISP --status
# Draw figures
python3 -m scripts.run all SISP --figonly

Realtime log is at ~/shuffle/log-SISP.txt, where you will find the summary of each finished proof.

Once the proofs finish, you can find reproduced figures under ~/shuffle/figures:

• Figure 5(a): SISP-VerificationTime.pdf
• Figure 7(a): SISP-InvLen-SmallBoom.pdf

To reproduce Figure 6, run the following command after SISP on SmallBOOM is finished. The output file is PaperFig-RP-SISP-SmallBoom.pdf.

python3 -m scripts.run paperfig-sisp-rp SmallBoom reproduce

Finally, when you are done with SISP setup, unpatch the BOOM.

cd ~/shuffle/chipyard
patch -p1 -R < ~/shuffle/patches/chipyard-SISP.patch

DelayFwd-All

Estimated Time: <8 hours

First, apply a patch that implements DelayFwd-All on BOOM (if you were testing other setups, make sure you have unpatched the BOOM before you apply this patch).

cd ~/shuffle/chipyard
patch -p1 < ~/shuffle/patches/chipyard-DelayFwd-All.patch

The remaining commands and their outputs are analogous to those in SISP.

cd ~/shuffle
# Start the proof
python3 -m scripts.run all DelayFwd-All --nproc=16
# Probe the progress
python3 -m scripts.run all DelayFwd-All --status
# Draw figures
python3 -m scripts.run all DelayFwd-All --figonly

Finally, unpatch the BOOM.

cd ~/shuffle/chipyard
patch -p1 -R < ~/shuffle/patches/chipyard-DelayFwd-All.patch

DelayFwd-Transmitter

Estimated Time: <13 hours

First, apply a patch that implements DelayFwd-Transmitter on BOOM (if you were testing other setups, make sure you have unpatched the BOOM before you apply this patch).

cd ~/shuffle/chipyard
patch -p1 < ~/shuffle/patches/chipyard-DelayFwd-Transmitter.patch

The remaining commands are similar. This proof takes a long time.

cd ~/shuffle
# Start the proof
python3 -m scripts.run all DelayFwd-Transmitter --nproc=16
# Probe the progress
python3 -m scripts.run all DelayFwd-Transmitter --status

Note that this setup does not generate any figure. You can investigate the runtime directory ~/shuffle/results/STT-TinyBoom for proof details.

• top.dump: Abstracted self-composition circuit
• run.txt: Log of the top-level proof
• log/: Lemmas profiling dumped by rIC3
• uf_po/: Refinement proofs

Finally, unpatch the BOOM.

cd ~/shuffle/chipyard
patch -p1 -R < ~/shuffle/patches/chipyard-DelayFwd-Transmitter.patch

Claims

Claim 1

1. HUF effectively verifies SISP on all sizes of BOOM, achieving about 6x speedup compared to the prior work VeloCT.
2. By leveraging hierarchical proof, all required refinement proofs complete faster than the SISP proof.
3. The majority of invariant lemmas contain no more than two literals and concisely reflect non-interference on important signals.

Claim 1: Script

Please refer to SISP.

Claim 1: Expectation

The above three points are well-supported by reproducing results that match the relevant figures in the paper:

1. Figure 5(a) is reproduced at figures/SISP-VerificationTime.pdf. The proof on MegaBoom takes around 1000s, which is much faster than VeloCT's ~13000s (interpreted from Figure 2 in their paper).
2. Figure 6 is reproduced at PaperFig-RP-SISP-SmallBoom.pdf. Heavy modules such as FpPipeline are successfully proved by applying hierarchical proof. The refinement proof times are moderate compared to the top-level proof.
3. Figure 7(a) is reproduced at figures/SISP-InvLen-SmallBoom.pdf. Invariant lemmas can be examined at results/SISP-SmallBoom/reproduce/inv-SISP-SmallBoom-reproduce.txt.

Claim 2

1. HUF successfully verifies DelayFwd-All on all sizes of BOOM.
2. The majority of invariant lemmas contain two literals and concisely reflect non-interference on important signals.

Claim 2: Script

Please refer to DelayFwd-All.

Claim 2: Expectation

The above two points are well-supported by reproducing results that match the relevant figures/tables in the paper:

1. Figure 5(b) is reproduced at figures/DelayFwd-All-VerificationTime.pdf.
2. Figure 7(b) is reproduced at figures/DelayFwd-All-InvLen-SmallBoom.pdf. Invariant lemmas can be examined at results/DelayWB-SmallBoom/reproduce/inv-DelayWB-SmallBoom-reproduce.txt.

Claim 3

HUF can prove DelayFwd-Transmitter on TinyBoom, with the help of auxiliary assumptions and assertions.

Claim 3: Script

Please refer to DelayFwd-Transmitter.

Claim 3: Expectation

The proof finishes in about 12 hours on a 2.20GHz server CPU (or about 5 hours on i9-14900K). The runtime report is at log-DelayFwd-Transmitter.txt. The invariant lemmas are available at results/STT-TinyBoom/reproduce/inv-STT-TinyBoom-reproduce.txt.