diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b95fe56..85dbf77 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,5 @@ -name: Docker build test -on: [push, pull_request] +name: Full CI tests and Docker deployment +on: [pull_request] jobs: build-docker: @@ -93,9 +93,9 @@ jobs: run: | cd /ecosystem/benchmarks/spectreguard make && mv specBench.bin specBench-32.bin - make clean && make 64BIT=1 && mv specBench.bin specBench-64.bin ../../simulation/build/sim-32-i specBench-32.bin ../../simulation/build/sim-32-o specBench-32.bin + make clean && make 64BIT=1 && mv specBench.bin specBench-64.bin ../../simulation/build/sim-64-i specBench-64.bin ../../simulation/build/sim-64-o specBench-64.bin @@ -117,19 +117,27 @@ jobs: with: image: ecosystem:latest run: | - cd /ecosystem . /ecosystem/waveform-analysis/.venv/bin/activate cd /ecosystem/noninterference-testing/ - make -C programs vcd USECLANG=0 RISCV_PREFIX=riscv64-unknown-elf SIM_EXE=/ecosystem/simulation/build/sim-32-o - ./run-security-eval.py + make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim-32-o + waveform-security - name: Run EVAL-HD uses: addnab/docker-run-action@v3 with: image: ecosystem:latest run: | + . /ecosystem/waveform-analysis/.venv/bin/activate cd /ecosystem/synthesis - ./run-yosys.sh + ./eval-hd.py ../core/Core.v --cell-library ../eval-hd/freepdk-45nm/stdcells.lib + + - name: Run one riscv-formal test + uses: addnab/docker-run-action@v3 + with: + image: ecosystem:latest + run: | + cd /ecosystem/formal-verification/riscv-formal + make formal-insn_bgeu push-image: name: Push Docker image diff --git a/.github/workflows/reduced.yml b/.github/workflows/reduced.yml new file mode 100644 index 0000000..191e4b4 --- /dev/null +++ b/.github/workflows/reduced.yml @@ -0,0 +1,83 @@ +name: Reduced CI tests +on: [push, pull_request] + +jobs: + build-docker: + name: Build Docker image + runs-on: ubuntu-latest + strategy: + fail-fast: false + steps: + - name: Free Disk Space + uses: jlumbroso/free-disk-space@main + with: + tool-cache: false + + - name: Check out repository + uses: actions/checkout@v2 + with: + submodules: 'recursive' + + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v2 + + - name: Build Docker image + uses: docker/build-push-action@v4 + with: + context: . + file: "Dockerfile" + tags: ecosystem:latest + push: false + build-args: | + INSTALL_PROTEUS=true + outputs: type=docker,dest=/tmp/ecosystem-docker.tar + + - name: Upload Docker artifact + uses: actions/upload-artifact@v4 + with: + name: ecosystem-docker + path: /tmp/ecosystem-docker.tar + + ci-tests: + runs-on: ubuntu-latest + needs: build-docker + steps: + - name: Free Disk Space + uses: jlumbroso/free-disk-space@main + with: + tool-cache: false + docker-images: false + + - name: Check out repository + uses: actions/checkout@v2 + + - name: Download Docker artifact + uses: actions/download-artifact@v4 + with: + name: ecosystem-docker + path: /tmp + + - name: Load Docker image + run: docker load --input /tmp/ecosystem-docker.tar + + - name: Run functional tests + uses: addnab/docker-run-action@v3 + with: + image: ecosystem:latest + run: | + cd /ecosystem + cp simulation/build/sim-32-i simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 -C functional-tests + cp simulation/build/sim-32-o simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 -C functional-tests + cp simulation/build/sim-64-i simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 64BIT=1 -C functional-tests + cp simulation/build/sim-64-o simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 64BIT=1 -C functional-tests + + - name: Run non-interference test + uses: addnab/docker-run-action@v3 + with: + image: ecosystem:latest + run: | + cd /ecosystem + . /ecosystem/waveform-analysis/.venv/bin/activate + cd /ecosystem/noninterference-testing/ + make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim-32-o + waveform-security diff --git a/.gitmodules b/.gitmodules index 29535b3..846ab62 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,3 @@ -[submodule "formal-verification/riscv-formal/riscv-formal"] - path = formal-verification/riscv-formal/riscv-formal - url = https://github.com/YosysHQ/riscv-formal.git [submodule "functional-tests/riscv-tests"] path = functional-tests/riscv-tests url = https://github.com/riscv-software-src/riscv-tests.git diff --git a/Dockerfile b/Dockerfile index bd11740..2daa163 100644 --- a/Dockerfile +++ b/Dockerfile @@ -3,12 +3,14 @@ FROM ubuntu:24.04 # Set to noninteractive mode ARG DEBIAN_FRONTEND=noninteractive -ARG INSTALL_TOOLCHAIN -ARG INSTALL_EVAL_HD -ARG INSTALL_PROTEUS +ARG INSTALL_TOOLCHAIN=false +ARG INSTALL_EVAL_HD=false +ARG INSTALL_PROTEUS=false +ARG INSTALL_RISCV_FORMAL=true RUN echo "Install RISC-V toolchain: ${INSTALL_TOOLCHAIN}" RUN echo "Install EVAL-HD: ${INSTALL_EVAL_HD}" RUN echo "Setup Proteus core: ${INSTALL_PROTEUS}" +RUN echo "Install riscv-formal: ${INSTALL_RISCV_FORMAL}" ################################################################################ # Basic dependencies @@ -35,6 +37,7 @@ WORKDIR /ecosystem RUN if [ "${INSTALL_TOOLCHAIN}" = "true" ] ; then ./install-scripts/toolchain.sh ; else echo Skipping RISC-V toolchain... ; fi RUN if [ "${INSTALL_EVAL_HD}" = "true" ] ; then ./install-scripts/eval-hd.sh ; else echo Skipping EVAL-HD setup... ; fi RUN if [ "${INSTALL_PROTEUS}" = "true" ] ; then ./install-scripts/proteus.sh ; else echo Skipping Proteus core setup... ; fi +RUN if [ "${INSTALL_RISCV_FORMAL}" = "true" ] ; then ./install-scripts/riscv-formal.sh ; else echo Skipping riscv-formal setup... ; fi # add RISC-V toolchain to path if it was installed (https://stackoverflow.com/a/51264575) ENV TOOLCHAIN_PATH=${INSTALL_TOOLCHAIN:+/opt/riscv/bin:} diff --git a/README.md b/README.md index aa00824..1da14a9 100644 --- a/README.md +++ b/README.md @@ -27,28 +27,18 @@ Alternatively, you can build this image locally with the included [Dockerfile](. The container can be built with the following command: ```shell-session -$ docker build -t ecosystem . +$ docker compose up ``` -Additional build arguments can be added with the `--build-arg FLAG_NAME=true` argument, for example `INSTALL_TOOLCHAIN` to install the RISC-V GNU toolchain, `INSTALL_EVAL_HD` to install the hardware cost evaluation tool and `INSTALL_PROTEUS` to clone and install the Proteus core inside the container (instead of mounting it as a volume). -Note that installing these extra tools will add a substantial amount of time to the build process (should quantify it later). - -```shell-session -$ docker build -t ecosystem . --build-arg INSTALL_PROTEUS=true --build-arg INSTALL_EVAL_HD=true --build-arg INSTALL_TOOLCHAIN=true -``` +Additional build arguments can be added in `docker-compose.yml`, for example `INSTALL_TOOLCHAIN` to install the RISC-V GNU toolchain, `INSTALL_EVAL_HD` to install the hardware cost evaluation tool and `INSTALL_PROTEUS` to clone and install the Proteus core inside the container (instead of mounting it as a volume). +Note that installing these extra tools will add a substantial amount of time to the build process. ### Working with the container You can launch a container after building: ```shell-session -$ docker run -it ecosystem -``` - -Optionally, you can attach the Proteus core directory as a volume, for example after cloning it to `core`: - -```shell-session -$ docker run -v ./core:/ecosystem/core -it ecosystem +$ docker compose run --remove-orphans ecosystem ``` ### Non-container setup diff --git a/benchmarks/spectreguard/specBench.c b/benchmarks/spectreguard/specBench.c index d60828e..12e17cb 100644 --- a/benchmarks/spectreguard/specBench.c +++ b/benchmarks/spectreguard/specBench.c @@ -265,7 +265,7 @@ int main(int argc, char **argv) time_work = 0; time_encrypt = 0; - for (k = 0; k < 100; k++) + for (k = 0; k < 10; k++) { printf("%d\n", k); time1 = rdcycle(); diff --git a/docker-compose.yml b/docker-compose.yml new file mode 100644 index 0000000..47d531e --- /dev/null +++ b/docker-compose.yml @@ -0,0 +1,20 @@ +services: + ecosystem: + build: + context: . + args: + INSTALL_EVAL_HD: "true" + INSTALL_TOOLCHAIN: "true" + container_name: ecosystem + restart: "no" + stdin_open: true + tty: true + working_dir: /ecosystem + volumes: + - ./core:/ecosystem/core + - ./synthesis:/ecosystem/synthesis + - ./noninterference-testing:/ecosystem/noninterference-testing + - ./waveform-analysis:/ecosystem/waveform-analysis + - ./install-scripts:/ecosystem/install-scripts + - ./formal-verification:/ecosystem/formal-verification + command: "/bin/bash" diff --git a/formal-verification/riscv-formal/Makefile b/formal-verification/riscv-formal/Makefile index ed378b7..e83fe02 100644 --- a/formal-verification/riscv-formal/Makefile +++ b/formal-verification/riscv-formal/Makefile @@ -1,27 +1,19 @@ -BASE_DIR = $(shell pwd) -RISCV_DIR = $(BASE_DIR)/.. -RISCV_FORMAL_DIR = $(BASE_DIR)/riscv-formal -CORE_DIR = $(RISCV_FORMAL_DIR)/cores/riscv +BASE_DIR = $(shell pwd)/../.. +TARGET_DIR = $(BASE_DIR)/riscv-formal/cores/proteus/ CORE ?= riscv.CoreFormal all: formal -$(RISCV_DIR)/Core.v: FORCE - cd $(RISCV_DIR); sbt "runMain $(CORE)" +proteus.v: + cd $(BASE_DIR)/core && sbt "runMain $(CORE)" && cp Core.v $(BASE_DIR)/formal-verification/riscv-formal/proteus.v -setup: $(RISCV_DIR)/Core.v - mkdir -p $(CORE_DIR) - cp $< $(CORE_DIR)/riscv.v - cp checks.cfg wrapper.sv disasm.py $(CORE_DIR) - cd $(CORE_DIR); python3 $(RISCV_FORMAL_DIR)/checks/genchecks.py +setup: proteus.v + mkdir -p $(TARGET_DIR) + cp checks.cfg wrapper.sv proteus.v $(TARGET_DIR) + cd $(TARGET_DIR) && python3 ../../checks/genchecks.py formal: setup - $(MAKE) -C $(CORE_DIR)/checks - @echo "Failed tests:" - find $(CORE_DIR)/checks -name trace.vcd + make -C $(TARGET_DIR)/checks -j$(nproc) formal-%: setup - $(MAKE) -C $(CORE_DIR)/checks $(subst formal-,,$@)_ch0 - -.PHONY: FORCE - + $(MAKE) -C $(TARGET_DIR)/checks $(subst formal-,,$@)_ch0 diff --git a/formal-verification/riscv-formal/checks.cfg b/formal-verification/riscv-formal/checks.cfg index 74c6db1..91e445d 100644 --- a/formal-verification/riscv-formal/checks.cfg +++ b/formal-verification/riscv-formal/checks.cfg @@ -1,4 +1,3 @@ - [options] isa rv32i @@ -19,4 +18,3 @@ causal 10 30 [script-sources] read_verilog -sv @basedir@/cores/@core@/wrapper.sv read_verilog @basedir@/cores/@core@/@core@.v - diff --git a/formal-verification/riscv-formal/riscv-formal b/formal-verification/riscv-formal/riscv-formal deleted file mode 160000 index 64931a6..0000000 --- a/formal-verification/riscv-formal/riscv-formal +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 64931a6094f02fc0946282b4cb79ec18d4e7f2d4 diff --git a/install-scripts/eval-hd.sh b/install-scripts/eval-hd.sh index 2d2b92c..37465e5 100755 --- a/install-scripts/eval-hd.sh +++ b/install-scripts/eval-hd.sh @@ -2,9 +2,6 @@ set -ex -apt-get install -yqq build-essential clang lld bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev git clone --recurse-submodules --depth 1 --shallow-submodules https://github.com/KULeuven-COSIC/eval-hd.git -cd eval-hd/yosys -make config-gcc -make -j$(nproc) -make install +. /ecosystem/waveform-analysis/.venv/bin/activate +pip install pyosys diff --git a/install-scripts/riscv-formal.sh b/install-scripts/riscv-formal.sh new file mode 100755 index 0000000..a5e9b75 --- /dev/null +++ b/install-scripts/riscv-formal.sh @@ -0,0 +1,32 @@ +#!/bin/bash + +set -ex + +git clone https://github.com/YosysHQ/riscv-formal.git + +git clone --recurse-submodules --depth 1 https://github.com/YosysHQ/yosys.git +cd yosys +apt-get install -yqq build-essential clang lld bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev +make -j$(nproc) +make install + +cd .. + +git clone https://github.com/YosysHQ/sby +cd sby +make install + +python3 -m pip install click --break-system-packages + +cd .. + +apt update && apt install -y cmake + +git clone https://github.com/boolector/boolector +cd boolector +./contrib/setup-btor2tools.sh +./contrib/setup-lingeling.sh +./configure.sh +make -C build -j$(nproc) +cp build/bin/{boolector,btor*} /usr/local/bin/ +cp deps/btor2tools/build/bin/btorsim /usr/local/bin/ diff --git a/noninterference-testing/README.md b/noninterference-testing/README.md index b9cd434..3e9801c 100644 --- a/noninterference-testing/README.md +++ b/noninterference-testing/README.md @@ -6,9 +6,37 @@ Specifically, it checks that observable microarchitectural components (e.g. exec We use noninterference testing to test security defenses implemented in Proteus. Concretely, we (1) generate sets of insecure programs that fail noninterference testing (2) secure these programs with hardware defenses and (3) make sure that secure versions pass noninterference testing. -> [!WARNING] -> The rest of this documentation is outdated and will be updated soon™. -> Try `--help` on the script you are interested in running. +For noninterference testing, we use the `waveform-security` binary, while for correctness testing we use `waveform-correctness`: + +```shell +$ make -C programs all +$ make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim + +$ waveform-correctness --p1 programs/vcd/pht-test1_FULLFENCE_LEAKBR_EXP1.vcd --p2 programs/vcd/pht-test1_NOFENCE_LEAKBR_EXP0.vcd --diff # correctness checking script +---------------------------------------- +Mismatch at change #13 +Common value: ('TOP.Core.pipeline.retirementStage.arbitration_isDone', 1) +Common value: ('TOP.Core.pipeline.retirementStage.in_PC', 2147483700) +Common value: ('TOP.Core.pipeline.retirementStage.in_RD_DATA', 0) +First value: ('TOP.Core.pipeline.retirementStage.in_RD', 16) +Second value: ('TOP.Core.pipeline.retirementStage.in_RD', 12) +Common value: ('TOP.Core.pipeline.retirementStage.in_RS1_DATA', 0) +Common value: ('TOP.Core.pipeline.retirementStage.in_RS2_DATA', 0) +First value: ('TOP.Core.pipeline.retirementStage.in_LSU_TARGET_ADDRESS', 2147483716) +Second value: ('TOP.Core.pipeline.retirementStage.in_LSU_TARGET_ADDRESS', 2147483712) + +$ waveform-security --leakage-sinks LEAKLOAD LEAKBR LEAKJMP # noninterference security evaluation +DEBUG: + Check all input for ./programs/vcd/ssb-test1_NOFENCE_LEAKBR with base=EXP1 + INFO: !--- Programs ./programs/vcd/ssb-test1_NOFENCE_LEAKBR is insecure :) ---! +DEBUG: + Check all input for ./programs/vcd/ssb-test1_FULLFENCE_LEAKBR with base=EXP1 + INFO: !--- Programs ./programs/vcd/ssb-test1_FULLFENCE_LEAKBR is secure :) ---! +DEBUG: + Check all input for ./programs/vcd/ssb-test1_NOFENCE_LEAKJMP with base=EXP1 + INFO: !--- Programs ./programs/vcd/ssb-test1_NOFENCE_LEAKJMP is insecure :) ---! +DEBUG: + Check all input for ./programs/vcd/ssb-test1_FULLFENCE_LEAKJMP with base=EXP1 + INFO: !--- Programs ./programs/vcd/ssb-test1_FULLFENCE_LEAKJMP is secure :) ---! + + RESULT: Secure programs: 12/12 Insecure programs: 6/12 +``` ## Overview @@ -25,50 +53,6 @@ Finally, each program is compiled with two secret values that should trigger dis ### Security evaluation +Compiled programs are in [./programs/build/](./programs/build/). The security evaluation runs pairs of programs with different secrets and monitors a set of selected signals. -The set of selected signals (conservative or liberal) are defined in [signals.py](./vcd_scripts/signals.py). - -Given two sets of signals, the [Comparator](./vcd_scripts/comparator.py) class reports any mismatch between the signal sets. If the set of selected signals match, then the program is secure; otherwise, there is a side-channel violation. - -TODO: the same principle can be applied for correctness evaluation (see [run-correctness-eval.py](./run-correctness-eval.py)) but, for now, this script is buggy. - -## Run security evaluation - -### Compile programs - -The first step is to compile the programs. Make sure the toolchain path is correct; the default is [../llvm-project](../llvm-project). - -``` -make -C programs all -``` - -Compiled programs are in [./programs/build/](./programs/build/). - -Optionally, you can create objdump files to look at the assembly code: - -``` -make -C programs objdump -``` - -### Run simulations - -The second step is to run the simulator to get the vcd files of these programs. Make sure the path of Proteus is correct; the default is [../proteus](../proteus). Additionally, make sure Proteus is compiled with the DynamicCore (`make -C sim CORE=riscv.CoreDynamicExtMem32`). - -``` -make -C programs vcd USECLANG=0 RISCV_PREFIX=riscv64-unknown-elf SIM_EXE=/ecosystem/simulation/build/sim -``` - -Resulting vcd files are in [./programs/vcd/](./programs/vcd/). - -### Run security evaluation - -The final step is to run the security evaluation: -``` -python ./run-security-evaluation.sh -``` - -The script can take arguments. For instance to chose the conservative security comparator, use `python ./run-security-evaluation.sh --compare-signals conservative`. -See help with `python ./run-security-evaluation.sh --help`. - -If you need to debug a particular program, run `python ./run-security-eval.py --debug ` to get a verbose output of the comparator. For instance `python ./run-security-eval.py --debug pht-test1_FULLFENCE_LEAKLOAD`. diff --git a/noninterference-testing/programs/Makefile b/noninterference-testing/programs/Makefile index 0a36b1e..9cf6a78 100644 --- a/noninterference-testing/programs/Makefile +++ b/noninterference-testing/programs/Makefile @@ -24,9 +24,8 @@ all: elf bin dirs: @mkdir -p $(BUILD_DIR) - @mkdir -p $(SIM_DIR) elf: dirs $(ELF_TARGETS) bin: dirs $(BIN_TARGETS) vcd: dirs $(VCD_TARGETS) -objdump: dirs $(OBJDUMP_TARGETS) \ No newline at end of file +objdump: dirs $(OBJDUMP_TARGETS) diff --git a/noninterference-testing/programs/Makefile.include b/noninterference-testing/programs/Makefile.include index f1a4ce7..61058cf 100644 --- a/noninterference-testing/programs/Makefile.include +++ b/noninterference-testing/programs/Makefile.include @@ -1,11 +1,9 @@ EVAL_DIR = $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) BASE_DIR = $(abspath $(EVAL_DIR)/../..) -SIM_DIR = $(BASE_DIR)/proteus/sim -SIM_EXE ?= $(SIM_DIR)/build/sim +SIM_EXE ?= $(BASE_DIR)/simulation/build/sim-32-o GTKW_DIR = $(EVAL_DIR)gtkw CORE ?= riscv.CoreExtMem32 -BUILD_CORE ?= 1 -USECLANG ?= 1 +USECLANG ?= 0 EXPERIMENT ?= LEGACY BOOT ?= 0 BUILD_DIR ?= ./ diff --git a/noninterference-testing/run-correctness-eval.py b/noninterference-testing/run-correctness-eval.py deleted file mode 100755 index 774e1bb..0000000 --- a/noninterference-testing/run-correctness-eval.py +++ /dev/null @@ -1,68 +0,0 @@ -#!/usr/bin/env python3 - -import argparse -import sys - - -from waveform_analysis.logger import log -from waveform_analysis.signal_extractor import CPUWaveform -from waveform_analysis.interface_parser import proteus_o_parser - - -def check_divergences(p1: str, p2: str, timing: bool, diff: bool, full_diff: bool) -> bool: - base_waveform: CPUWaveform = CPUWaveform(p1, proteus_o_parser) - return base_waveform.compare_signals(CPUWaveform(p2, proteus_o_parser), proteus_o_parser.get_instruction_stream_list(), timing_sensitive=timing, display_diff=diff, early_out=(not full_diff)) - - -def parse_arguments(): - parser = argparse.ArgumentParser( - description="Run security evaluation on benchmarks.") - parser.add_argument("--program_path", type=str, default="./programs", - help="Path to the program directory (default: ./programs)") - parser.add_argument( - "--p1", - type=str, - help="Name of the benchmark to run (e.g., pht-test1_FULLFENCE_LEAKLOAD_EXP0)." - ) - parser.add_argument( - "--p2", - type=str, - help="Name of the benchmark to run (e.g., pht-test1_NOFENCE_LEAKLOAD_EXP0)." - ) - parser.add_argument( - "--diff", - action="store_true", - help="Display difference in signals" - ) - parser.add_argument( - "--timing", - action="store_true", - help="Report differences in timing" - ) - parser.add_argument( - "--full_diff", - action="store_true", - help="Report all differences, not just the first one" - ) - args = parser.parse_args() - return args - - -def main(): - args = parse_arguments() - p1 = args.p1 - p2 = args.p2 - diff = args.diff - timing = args.timing - full = args.full_diff - - if not p1 or not p2: - print("Error: Both --p1 and --p2 arguments are required.") - sys.exit(1) - - print(f"Running correctness evaluation for {p1} and {p2}") - print(check_divergences(p1, p2, timing, diff, full)) - - -if __name__ == "__main__": - main() diff --git a/synthesis/eval-hd-area.ys b/synthesis/eval-hd-area.ys deleted file mode 100644 index abd2365..0000000 --- a/synthesis/eval-hd-area.ys +++ /dev/null @@ -1,26 +0,0 @@ -# read design -read_verilog ../core/Core.v - -# elaborate design hierarchy -hierarchy -check -top Core - -# the high-level stuff -proc; opt; fsm; opt; memory; opt - -# mapping to internal cell library -techmap; opt - -# mapping flip-flops to cell library -dfflibmap -liberty ../eval-hd/freepdk-45nm/stdcells.lib - -# mapping logic to cell library -abc -liberty ../eval-hd/freepdk-45nm/stdcells.lib - -# cleanup -clean - -# write synthesized design -write_verilog ../synthesis/result.v - -# get ASIC gate count and area numbers -stat -liberty ../eval-hd/freepdk-45nm/stdcells.lib diff --git a/synthesis/eval-hd-timing.ys b/synthesis/eval-hd-timing.ys deleted file mode 100644 index 808ff1d..0000000 --- a/synthesis/eval-hd-timing.ys +++ /dev/null @@ -1,29 +0,0 @@ -# read design -read_verilog ../core/Core.v - -# elaborate design hierarchy -hierarchy -check -top Core - -# flatten the design -flatten - -# the high-level stuff -proc; opt; fsm; opt; memory; opt - -# mapping to internal cell library -techmap; opt - -# mapping flip-flops to cell library -dfflibmap -liberty ../eval-hd/freepdk-45nm/stdcells.lib - -# mapping logic to cell library with timing constraint -abc -liberty ../eval-hd/freepdk-45nm/stdcells.lib -fast -D 2625 - -# cleanup -clean - -# write synthesized design -write_verilog ../synthesis/result.v - -# get ASIC gate count and area numbers -stat -liberty ../eval-hd/freepdk-45nm/stdcells.lib diff --git a/synthesis/eval-hd.py b/synthesis/eval-hd.py new file mode 100755 index 0000000..2b14d8b --- /dev/null +++ b/synthesis/eval-hd.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 + +from pyosys import libyosys as ys +import argparse + +def run_analysis(report_timing: bool, design_file: str, top_module: str, timing_target: int, cell_library: str) -> None: + design = ys.Design() + + # read design + ys.run_pass(f"read_verilog {design_file}", design) + + # elaborate design hierarchy + ys.run_pass(f"hierarchy -check -top {top_module}", design) + + if report_timing: + # flatten the design + ys.run_pass("flatten", design) + + # the high-level stuff + ys.run_pass("proc; opt; fsm; opt; memory; opt", design) + + # mapping to internal cell library + ys.run_pass("techmap; opt", design) + + # mapping flip-flops to cell library + ys.run_pass(f"dfflibmap -liberty {cell_library}", design) + + if report_timing: + # mapping logic to cell library with timing constraint + ys.run_pass(f"abc -liberty {cell_library} -fast -D {timing_target}", design) + else: + # mapping logic to cell library + ys.run_pass(f"abc -liberty {cell_library}", design) + + # cleanup + ys.run_pass("clean", design) + + # write synthesized design + ys.run_pass("write_verilog result.v", design) + + # get ASIC gate count and area numbers + ys.run_pass(f"stat -liberty {cell_library}", design) + +def main() -> None: + parser = argparse.ArgumentParser(description="Synthesize a design for ASIC using Yosys.") + parser.add_argument("design_file", type=str, help="Path to the Verilog design file.") + parser.add_argument("--top_module", type=str, default="Core", help="Name of the top module (default: Core).") + parser.add_argument("--cell-library", default="freepdk-45nm/stdcells.lib", help="Path to the cell library (default: FreePDK).") + parser.add_argument("--report-timing", action="store_true", help="Enable timing analysis during synthesis.") + parser.add_argument("--timing-target", type=int, default=2500, help="Target timing constraint (in picoseconds, default: 2500).") + args = parser.parse_args() + + run_analysis(args.report_timing, args.design_file, args.top_module, args.timing_target, args.cell_library) + +if __name__ == "__main__": + main() diff --git a/synthesis/run-yosys.sh b/synthesis/run-yosys.sh deleted file mode 100755 index b5d281d..0000000 --- a/synthesis/run-yosys.sh +++ /dev/null @@ -1 +0,0 @@ -../eval-hd/yosys/yosys eval-hd-area.ys diff --git a/synthesis/top.py b/synthesis/top.py new file mode 100755 index 0000000..65f5869 --- /dev/null +++ b/synthesis/top.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 + +import subprocess +import re + +def run_with_timing(target: int) -> bool: + timing_failed = False + + result = subprocess.run(["./eval-hd.py", "../core/Core.v", "--report-timing", "--timing-target", str(target), "--cell-library", "../eval-hd/freepdk-45nm/stdcells.lib"], capture_output=True, text=True) + rs = re.search(r"Chip area for module \'\\Core\': (\d+.\d+)", result.stdout) + if rs: + area = float(rs.group(1)) + print(f"Area = {area:.2f} µm² = {(area / 1000000):.4f} mm²") + + trs = re.search(r"Cannot meet the target required times \((\d+.\d+)\). Continue anyway.", result.stdout) + if trs: + timing = float(trs.group(1)) + print("Timing failed") + timing_failed = True + else: + print(f"Timing met: {target} ps = {target / 1000} ns = {1 / (target / 1000000):.2f} MHz") + + return timing_failed + +successful_target = 10000 + +for step in [1000, 100, 10, 1]: + for target in range(successful_target - 9 * step, successful_target, step): + failed = run_with_timing(target) + if not failed: + successful_target = target + break diff --git a/waveform-analysis/.gitignore b/waveform-analysis/.gitignore new file mode 100644 index 0000000..1d17dae --- /dev/null +++ b/waveform-analysis/.gitignore @@ -0,0 +1 @@ +.venv diff --git a/waveform-analysis/README.md b/waveform-analysis/README.md index 84c747c..ebaaf36 100644 --- a/waveform-analysis/README.md +++ b/waveform-analysis/README.md @@ -1,3 +1,17 @@ +# Waveform analysis + +## Binary tools + +After installation, the library exports the following binaries that can be used (after activating the virtual environment): + +- `strip-vcd`: reduce VCD files to the list of signals that we are interested in (to speed up later processing or to be able to store it) +- `waveform-correctness`: check the equivalence of architectural signals between two waveforms +- `waveform-security`: checks whether certain benchmarks, when compiled with and without different countermeasures exhibit the expected leakage + +For more details, consult the `--help` option on these binaries. + +## Internal detail notes + Waveform analysis is a fundamental basis of a lot of the analysis we perform in the ecosystem. - cpu interfaces describe which signals should be interpreted diff --git a/waveform-analysis/pyproject.toml b/waveform-analysis/pyproject.toml index c25e222..49c4e69 100644 --- a/waveform-analysis/pyproject.toml +++ b/waveform-analysis/pyproject.toml @@ -12,3 +12,5 @@ build-backend = "uv_build" [project.scripts] strip-vcd = "waveform_analysis.strip:main" +waveform-correctness = "waveform_analysis.check_correctness:main" +waveform-security = "waveform_analysis.check_security:main" diff --git a/waveform-analysis/src/waveform_analysis/check_correctness.py b/waveform-analysis/src/waveform_analysis/check_correctness.py new file mode 100755 index 0000000..a7c9d64 --- /dev/null +++ b/waveform-analysis/src/waveform_analysis/check_correctness.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 + +import argparse + + +from .signal_extractor import CPUWaveform +from .interface_parser import proteus_o_parser + + +def parse_arguments(): + parser = argparse.ArgumentParser( + description="Run correctness evaluation on two waveforms.") + parser.add_argument( + "--p1", + type=str, + required=True, + help="Path of the first waveform file." + ) + parser.add_argument( + "--p2", + type=str, + required=True, + help="Path of the second waveform file." + ) + parser.add_argument( + "--diff", + action="store_true", + help="Display diverging signals (default behavior is to only report True/False)" + ) + parser.add_argument( + "--timing", + action="store_true", + help="Report differences in timing" + ) + parser.add_argument( + "--full_diff", + action="store_true", + help="Report all differences, not just the first one" + ) + args = parser.parse_args() + return args + + +def main(): + args = parse_arguments() + p1 = args.p1 + p2 = args.p2 + diff = args.diff + timing = args.timing + full = args.full_diff + + base_waveform = CPUWaveform(p1, proteus_o_parser) + identical = base_waveform.compare_signals( + CPUWaveform(p2, proteus_o_parser), + proteus_o_parser.get_instruction_stream_list(), + timing_sensitive=timing, + display_diff=diff, + early_out=(not full)) + if identical: + print("Signals match!") + elif not diff: + print("Signals do not match!") diff --git a/noninterference-testing/run-security-eval.py b/waveform-analysis/src/waveform_analysis/check_security.py similarity index 60% rename from noninterference-testing/run-security-eval.py rename to waveform-analysis/src/waveform_analysis/check_security.py index 43ea1d6..10cd549 100755 --- a/noninterference-testing/run-security-eval.py +++ b/waveform-analysis/src/waveform_analysis/check_security.py @@ -20,30 +20,28 @@ def signals_based_on_policy(waveform: CPUWaveform, policy: str) -> list[str]: raise NotImplementedError() -def check_all_inputs(policy: str, filename: str, exp_numbers: list[str], display_diff: bool = False) -> int: +def secure_for_all_inputs(policy: str, filename: str, exp_postfixes: list[str], display_diff: bool = False) -> bool: global policy_signals - base = exp_numbers[0] + base = exp_postfixes[0] log.debug(f"+ Check all input for {filename} with base={base}") base_waveform = CPUWaveform(f"{filename}_{base}.vcd", proteus_o_parser) if policy_signals is None: policy_signals = signals_based_on_policy(base_waveform, policy) - for input_case in exp_numbers[1:]: + for input_case in exp_postfixes[1:]: if not base_waveform.compare_signals(CPUWaveform(f"{filename}_{input_case}.vcd", proteus_o_parser), policy_signals, display_diff=display_diff): - log.debug(f"!--- Programs {filename} is insecure ---!") - return 1 - log.debug(f"!--- Program {filename} is secure ---!") - return 0 + return False + return True def check_all_combinations( - # comparator: Comparator, + path: str, policy: str, benches: list[str], secure_defenses: list[str], insecure_defenses: list[str], leakage_sinks: list[str], - exp_numbers: list[str] + exp_postfixes: list[str] ) -> None: secure_programs_total = 0 secure_programs_found_secure = 0 @@ -51,14 +49,14 @@ def check_all_combinations( insecure_programs_found_insecure = 0 for bench in benches: - base_file = f"{benchmark_path}/vcd/{bench}" + base_file = f"{path}/vcd/{bench}" print(f"====== Running experiment for {base_file}") for leak_sink in leakage_sinks: for fence in insecure_defenses: file = f"{base_file}_{fence}_{leak_sink}" insecure_programs_total += 1 - if check_all_inputs(policy, file, exp_numbers) == 0: + if secure_for_all_inputs(policy, file, exp_postfixes): log.warning( f"!--- Programs {file} should be insecure :( ---!") else: @@ -68,7 +66,7 @@ def check_all_combinations( for fence in secure_defenses: file = f"{base_file}_{fence}_{leak_sink}" secure_programs_total += 1 - if check_all_inputs(policy, file, exp_numbers) == 1: + if not secure_for_all_inputs(policy, file, exp_postfixes): log.error(f"!--- Programs {file} should be secure :( ---!") else: log.info(f"!--- Programs {file} is secure :) ---!") @@ -79,31 +77,68 @@ def check_all_combinations( f"Secure programs: {secure_programs_found_secure}/{secure_programs_total} Insecure programs: {insecure_programs_found_insecure}/{insecure_programs_total}") -def debug(policy: str, target: str) -> None: - check_all_inputs( - policy, f"{benchmark_path}/vcd/{target}", ["EXP0", "EXP1"], display_diff=True) +def debug(path: str, policy: str, target: str) -> None: + secure_for_all_inputs( + policy, f"{path}/vcd/{target}", ["EXP0", "EXP1"], display_diff=True) -def parse_arguments(benchmarks: list[str]) -> argparse.Namespace: +def parse_arguments() -> argparse.Namespace: + benchmarks = ['pht-test1', 'pht-test2', 'psf-test1', 'ssb-test1'] + secure_defenses = ["FULLFENCE"] + insecure_defenses = ["NOFENCE"] + leakage_sinks = ["LEAKLOAD", "LEAKSTORE", "LEAKBR", "LEAKJMP", "LEAKDIV"] + exp_postfixes = ["EXP1", "EXP0"] + parser = argparse.ArgumentParser( description="Run security evaluation on benchmarks.") parser.add_argument("--program_path", type=str, default="./programs", help="Path to the program directory (default: ./programs)") parser.add_argument( - "--program_name", + "--benchmarks", type=str, - choices=benchmarks + ["all"], - default="all", - help="Name of the benchmark to run (default: all). Options: " + - ", ".join(benchmarks + ["all"]) + nargs='*', + choices=benchmarks, + default=benchmarks, + help="Name of the benchmark to run (leave out to include all)." ) - # Choose security comparator parser.add_argument( "--compare-signals", choices=["conservative", "liberal"], default="liberal", help="Choose which signals to compare: conservative (all signals except selected non-observable signals) or liberal (only selected observable signals) (default: liberal)" ) + parser.add_argument( + "--secure-defenses", + type=str, + nargs='*', + choices=secure_defenses, + default=secure_defenses, + help="Secure defense configurations (leave out to include all)." + ) + parser.add_argument( + "--insecure-defenses", + type=str, + nargs='*', + choices=insecure_defenses, + default=insecure_defenses, + help="Insecure defense configurations (leave out to include all)." + ) + parser.add_argument( + "--leakage-sinks", + type=str, + nargs='*', + choices=leakage_sinks, + default=leakage_sinks, + help="Leakage sink configurations (leave out to include all)." + ) + parser.add_argument( + "--experiment-postfixes", + type=str, + nargs='*', + choices=exp_postfixes, + default=exp_postfixes, + help="Experiment postfix identifiers (leave out to include all)." + ) parser.add_argument( "--debug", type=str, @@ -115,31 +150,20 @@ def parse_arguments(benchmarks: list[str]) -> argparse.Namespace: def main() -> None: - all_bench = ['pht-test1', 'pht-test2', 'psf-test1', 'ssb-test1'] - args = parse_arguments(all_bench) - - global benchmark_path - benchmark_path = args.program_path - benchmark = args.program_name + args = parse_arguments() if args.debug: - debug(args.compare_signals, args.debug) + debug( + path=args.program_path, + policy=args.compare_signals, + target=args.debug) return - # Experiment configuration - secure_defenses = ["FULLFENCE"] - insecure_defenses = ["NOFENCE"] - leakage_sinks = ["LEAKLOAD", "LEAKSTORE", "LEAKBR", "LEAKJMP", "LEAKDIV"] - exp_numbers = ["EXP1", "EXP0"] - - if benchmark == "all": - benchs = all_bench - else: - benchs = [benchmark] - - check_all_combinations(args.compare_signals, benchs, secure_defenses, - insecure_defenses, leakage_sinks, exp_numbers) - - -if __name__ == "__main__": - main() + check_all_combinations( + path=args.program_path, + policy=args.compare_signals, + benches=args.benchmarks, + secure_defenses=args.secure_defenses, + insecure_defenses=args.insecure_defenses, + leakage_sinks=args.leakage_sinks, + exp_postfixes=args.experiment_postfixes) diff --git a/waveform-analysis/src/waveform_analysis/py.typed b/waveform-analysis/src/waveform_analysis/py.typed new file mode 100644 index 0000000..e69de29