Datasetpublic

Akirayasha/relbench_O2

RelBench-O2: Constant-Time Assembly at -O2 Overview This dataset collects the rel_bench constant-time programs, re-cut into one self-contained program per record, compiled with LLVM/Clang-17 at -O2 for three targets, and checked for constant-timeness with binsec -sse -checkct. Constant-time source code is not enough: the optimizer can reintroduce a secret-dependent branch or memory access that the -O0 build does not have, and it does so differently per target. The… See the full description on the dataset page: https://huggingface.co/datasets/Akirayasha/relbench_O2.

sourceHugging Facemitupdated 1mo agoView on Hugging Face

0likes34downloads

Dataset Card

RelBench-O2: Constant-Time Assembly at -O2

Overview

This dataset collects the rel_bench constant-time programs, re-cut into one self-contained program per record, compiled with LLVM/Clang-17 at -O2 for three targets, and checked for constant-timeness with binsec -sse -checkct.

Constant-time source code is not enough: the optimizer can reintroduce a secret-dependent branch or memory access that the -O0 build does not have, and it does so differently per target. The intended tasks are transpilation (translate the assembly to another ISA) and classification/repair (decide whether a build leaks, and fix it if it does).

Dataset Structure

Column	Description
`task_name`	Sample identifier, e.g. `ct_select_1`
`flag_x86_64`	BinSec constant-time verdict for the x86-64 `-O2` build: `secure`, `insecure`, or `unknown`
`flag_aarch64_linux`	Same, for the AArch64 `-O2` build
`flag_riscv`	Same, for the RISC-V `-O2` build
`x86_64`	x86-64 assembly at -O2 (Intel syntax, built with `-masm=intel`)
`aarch64_linux`	AArch64 assembly at -O2
`riscv`	RISC-V RV64 (`rv64gc`/`lp64d`) assembly at -O2
`test_c`	C source of the BinSec harness (`test.c`) -- tags inputs secret/public through the `high_input_N` / `low_input_N` markers and calls the function under analysis
`binsec_output_x86_64`	Full `binsec -checkct` log for the x86-64 `-O2` build -- the evidence `flag_x86_64` was parsed from, including the leaking instruction addresses
`binsec_output_aarch64_linux`	Same, for the AArch64 `-O2` build
`binsec_output_riscv`	Same, for the RISC-V `-O2` build

Statistics

—Total records: 36

column	secure	insecure
`flag_x86_64`	31	5
`flag_aarch64_linux`	34	2
`flag_riscv`	29	7

The constant-time oracle

Each build is analysed by BinSec's checkct plugin:

bash

binsec -sse -checkct -sse-script "libsym.ini,checkct.cfg" -sse-depth 50000 test_bin

libsym.ini replaces the high_input_N markers with secret and the low_input_N markers with nondet (public), so BinSec knows which bytes are secret. It then reports:

—secure -- no control flow or memory access depends on a secret
—insecure -- at least one secret-dependent branch or address was found
—unknown -- BinSec could not decide (path cut, depth limit, unresolved symbol)

The verdict is per build. The same program can be secure on one target and insecure on another, because the three backends make different branch/cmov/csel choices at -O2. That is why the verdict is not collapsed into one label: each target carries its own flag_* column, with the full analysis log in the matching binsec_output_* column -- that log names the control-flow and memory-access checks that failed and at which addresses, so an insecure verdict can be traced back to a specific instruction.

Usage

python

from datasets import load_dataset

ds = load_dataset("Akirayasha/relbench_O2", split="test")

record = ds[0]
src_asm = record["x86_64"]  # source-side assembly
tgt_asm = record["riscv"]   # reference target-side assembly
leaky   = record["flag_riscv"] == "insecure"   # per-target verdict
harness = record["test_c"]  # rebuild + recheck a candidate against BinSec
why     = record["binsec_output_riscv"]  # the BinSec log behind flag_riscv

Citation

Part of the CISC-to-RISC transpilation research project at MBZUAI.