Chio/Docs
LOGIN · JOIN

PlatformTesting & Adversarial Analysis

Formal Assurance

Constant-time tests

dudect harnesses measure data-dependent timing in three verdict paths: signature comparison, scope subset checks, and JWT VC rejection.

Measured, not proved

dudect is a statistical timing-leak detector, and its evidence kind is a measurement on one machine and toolchain rather than a proof over all executions. Nothing on this page appears in the property matrix of formal/proof-manifest.toml, so a clean run supports no property claim there. Power and electromagnetic side channels are out of scope. See the Assumptions and TCB page for the full side-channel scope.

What dudect does

dudect (Distinguishability Under Decision Theoretic Effort) is a statistical detector for data-dependent timing. The harness runs the function under test against two input classes and records the runtime distribution per class. It then runs Welch's t-test on the distributions: if the means are statistically distinguishable, the function is taking different times on different inputs.

The per-run verdict is FAIL when the maximum absolute t reaches 4.5 and PASS below it. Two consecutive FAIL verdicts for the same harness are the alarm condition. What the alarm does is open a GitHub issue, not fail a build: every job in the lane carries continue-on-error: true and the workflow header states the posture directly, that the whole lane is advisory and the issue is the signal.

Timing can expose secrets when the response time depends on the secret bytes. A short-circuiting == on a MAC tag returns early on the first mismatched byte; an attacker who can issue many comparisons can binary-search the tag byte by byte. A constant-time compare runs every byte regardless and gives the attacker no timing difference in this comparison.


Functions tested

Three harnesses across two crates, each gated behind the dudect Cargo feature so a default cargo test is unaffected.

HarnessCode pathClass definition
mac_eqchio_core_types::crypto::Signature byte-equality compare (PartialEq on [u8; 64])Left: pair differs at byte 0. Right: pair differs at byte 63.
scope_subsetNormalizedScope::is_subset_ofLeft: matching parent grant at index 0. Right: matching parent grant at index PARENT_FANOUT - 1.
jwt_verifychio_credentials::verify_chio_passport_jwt_vc_json rejection path (crate chio-credentials)Left: all-zero compact byte string, rejected at the first base64url segment split. Right: random ASCII of the same length, same fail-closed verdict but a different parse path.

MAC equality

The portable receipt and passport verifiers compare Signature blobs by bytes; the underlying PartialEq impl on Signature uses == on the underlying Ed25519 byte array. That byte-equality compare is the closest in-tree analogue of an HMAC-tag compare, the canonical constant-time cryptographic code path.

From crates/kernel/chio-kernel-core/tests/dudect/mac_eq.rs:

crates/kernel/chio-kernel-core/tests/dudect/mac_eq.rs86-109rust
fn mac_eq_bench(runner: &mut CtRunner, rng: &mut BenchRng) {
    let mut inputs: Vec<(Class, Signature, Signature)> = Vec::with_capacity(SAMPLES_PER_RUN);
    for _ in 0..SAMPLES_PER_RUN {
        if rng.random::<bool>() {
            let (a, b) = signature_pair_differing_at(rng, 0);
            inputs.push((Class::Left, a, b));
        } else {
            let (a, b) = signature_pair_differing_at(rng, 63);
            inputs.push((Class::Right, a, b));
        }
    }

    for (class, a, b) in inputs {
        runner.run_one(class, || {
            // The verdict is always `false` because the inputs differ by
            // construction; we only care about the time the compare takes.
            // Return the comparison result so `run_one`'s `black_box` keeps
            // the compare in the optimized binary; assigning to `_` would
            // let `--release` LLVM eliminate the comparison and leave the
            // harness measuring runner overhead instead of byte equality.
            a == b
        });
    }
}

Both classes have identical input shapes (random 64-byte blobs); the only difference is which byte position carries the inequality. A naive == short-circuits early on Left (one byte compare) and runs the full 64 bytes on Right. A constant-time compare takes the same time on both.


Scope subset

NormalizedScope::is_subset_of walks the child's tool grants and asks whether each is covered by any grant in the parent. The inner short-circuit (Iterator::any) returns as soon as a covering parent grant is found. Whether the input data influences how quickly the subset check resolves is the question this harness asks.

From crates/kernel/chio-kernel-core/tests/dudect/scope_subset.rs:

crates/kernel/chio-kernel-core/tests/dudect/scope_subset.rs129-148rust
fn scope_subset_bench(runner: &mut CtRunner, rng: &mut BenchRng) {
    let child = child_scope_matching();

    let mut inputs: Vec<(Class, NormalizedScope)> = Vec::with_capacity(SAMPLES_PER_RUN);
    for _ in 0..SAMPLES_PER_RUN {
        if rng.random::<bool>() {
            inputs.push((Class::Left, parent_scope_with_match_at(0)));
        } else {
            inputs.push((Class::Right, parent_scope_with_match_at(PARENT_FANOUT - 1)));
        }
    }

    for (class, parent) in inputs {
        runner.run_one(class, || {
            // Verdict is always `true` by construction; we are measuring
            // the time the check takes to return that verdict.
            let _ = child.is_subset_of(&parent);
        });
    }
}

Both classes resolve to true; the question is whether the time taken to reach that verdict is data-dependent in a way an off-path attacker could use to learn which parent grant matched.

Scope evaluation runs on the verdict-producing hot path for capability-bearing tool calls. A timing leak here would let a tenant learn the structure of another tenant's parent capability through response-time analysis.


JWT VC signature verification

chio_credentials::verify_chio_passport_jwt_vc_json is the compact-JWT verifier behind Chio passport verifiable credentials. It is fail-closed: no arbitrary byte stream passes the issuer signature check. The harness asks whether the rejection path is constant-time with respect to the input contents.

From crates/trust/chio-credentials/tests/dudect/jwt_verify.rs, the two classes are the same length so only the contents differ:

  • Class::Left · an all-zero compact byte string. The compact-JWT decoder rejects it at the first base64url segment split, so the rejection path is short.
  • Class::Right · a random printable-ASCII string of the same length. Same fail-closed verdict, but the parse path may run a different number of base64url-decode or serde_json steps before failing.

The issuer keypair is materialized once from a fixed seed so signature-mismatch noise stays out of the timing distribution. A distinguishable Left/Right distribution would mean the verifier leaks something about why a candidate JWT was rejected.


Running

All three harnesses are gated behind the dudect Cargo feature and require --release.

bash
# MAC equality
cargo test -p chio-kernel-core \
  --features dudect --release mac_eq

# Scope subset
cargo test -p chio-kernel-core \
  --features dudect --release scope_subset

# JWT VC verify (chio-credentials)
cargo test -p chio-credentials \
  --features dudect --release jwt_verify

Those three commands are the ones each harness quotes in its own module docstring. CI runs a slightly different shape, naming the test binary and forwarding --nocapture, because ctbench_main! writes its max t lines to stdout and the threshold script has to read them:

bash
cargo test -p chio-kernel-core --features dudect --release \
  --test dudect_mac_eq -- --nocapture | tee dudect-out/mac_eq.out

The lane is .github/workflows/dudect.yml. It runs the three harnesses as a parallel matrix on a nightly schedule and on manual workflow_dispatch; its own concurrency comment records that pull-request triggers are not configured for it. The harness names are jwt_verify, mac_eq and scope_subset, bound to the test binaries dudect_jwt_verify, dudect_mac_eq and dudect_scope_subset. The threshold is overridable per dispatch through inputs.threshold, which the workflow keeps in lock step with the script default of 4.5.


Reading the t-statistic

ctbench_main! from the dudect-bencher crate prints one line per sample-count checkpoint. The threshold script documents the shape it parses:

scripts/check-dudect-threshold.sh22-29bash
# dudect-bencher 0.7 stdout shape (relevant lines):
#
#     running 1 bench
#     bench jwt_verify_bench seeded with 0xdeadbeef_cafef00d
#     bench jwt_verify_bench ... : n == +0.040M, max t = +2.13, max tau = ...
#
# The parser extracts every "max t = <signed-float>" occurrence, takes
# the absolute value, tracks the maximum, and compares against THRESHOLD.

Reading a line:

  • n is the sample count so far, printed with an M suffix.
  • max t is the worst-case Welch's t across the percentile cutoffs, signed. The parser takes its absolute value.
  • The verdict compares the maximum |t| across every such line in the file against the threshold, so a single elevated checkpoint decides the run's verdict even if later checkpoints settle.

Each harness builds SAMPLES_PER_RUN: usize = 100_000 input pairs per invocation, and the sample count in the output accumulates across the runner's repeated invocations. How far it climbs on a given machine is a property of that run, not a configured bound: the workflow's comment records that the bench iteration cap lives in ctbench_main! and that the job's timeout-minutes: 30 is only an outer bound on a release run.


The verdict script

scripts/check-dudect-threshold.sh is the whole decision procedure. It extracts every max t = <signed-float> occurrence with awk, takes absolute values, keeps the maximum, and compares it against the threshold. The 4.5 default is a literal in the script rather than a config value, and the script's header records that a gate check greps for it so a change to the threshold is a deliberate edit.

scripts/check-dudect-threshold.sh174-203bash
verdict() {
    local input="$1"
    local threshold="$2"

    if [[ ! -r "${input}" ]]; then
        err "input file not readable: ${input}"
        exit 2
    fi

    local max_t
    max_t="$(extract_max_abs_t "${input}")"

    if [[ -z "${max_t}" ]]; then
        err "no 'max t = <float>' lines found in ${input}; nothing to verdict"
        exit 2
    fi

    # Numeric compare via awk (avoids bc dep). Returns 1 (FAIL) when
    # max_t >= threshold per the dudect paper's "highly significant" rule.
    local result
    result="$(awk -v a="${max_t}" -v b="${threshold}" 'BEGIN { print (a + 0.0 >= b + 0.0) ? "FAIL" : "PASS" }')"

    printf 'dudect verdict: max|t|=%s threshold=%s result=%s\n' \
        "${max_t}" "${threshold}" "${result}"

    if [[ "${result}" == "FAIL" ]]; then
        exit 1
    fi
    exit 0
}

Three things follow from that body and are worth being exact about. The comparison is >=, so a maximum of exactly 4.5 is a FAIL. The printed line is dudect verdict: max|t|=<value> threshold=<T> result=<PASS|FAIL>, not a free-text leak banner. And the value is emitted at %.17g precision on purpose: the script explains that truncating to four decimals would round 4.49996 up to 4.5000 and manufacture a FAIL.

Exit codes are the interface the workflow consumes: 0 for a run under the threshold, 1 for a run at or above it, and 2 for a precondition failure such as a missing file, a bad --threshold, or a file with no max t lines at all. The workflow maps those to the literal strings PASS, FAIL and ERROR in a <harness>.verdict file. A parse failure is therefore neither a pass nor an alarm.

--dry-run parses a built-in synthetic input carrying mixed-sign t values and checks the parser recovers the correct maximum, exiting 2 on disagreement. It touches nothing outside a private temp file, so it is the cheap way to confirm the script itself still works.


What happens on a leak

A regressed byte-equality compare would push max t past the threshold and the harness's verdict file would read FAIL. That alone does nothing. The measurement job is continue-on-error: true and the threshold step captures the exit code explicitly so it never fails the job.

The decision sits in a second job, dudect-correlate (two-consecutive-run rule). It downloads the current run's dudect-nightly-* artifacts and the most recent prior completed run's, filtered to schedule and workflow_dispatch events with status completed so an in-progress run is never picked as the baseline. For each of the three harnesses it compares the two verdict strings.

  • Both FAIL: the job opens, or comments on an existing open issue titled dudect: sustained timing leak in <harness> (t >= 4.5 in 2 consecutive runs), labelled timing-leak, with links to both runs.
  • Anything else, including a missing baseline on the first run in the lane: it prints no sustained leaks (two-consecutive-run rule); nothing to file and exits 0.

So the honest description of the gate is that it raises a tracked issue on a correlated signal and stays quiet on an uncorrelated one. It does not block a merge, and the workflow header says why: on a shared runner a single above-threshold reading is plausibly a noisy neighbour, a JIT warmup, or a transient throttle event.

Once an issue exists, the triage question is whether the signal is the compare path or the machine. A timing leak commonly produces max t that grows with the sample count; noise does not. The raw <harness>.out files travel with each artifact for 30 days, so both runs'checkpoint sequences are available to compare. A confirmed leak in mac_eq means the byte-equality compare regressed, and the conventional fix is to route through subtle::ConstantTimeEq or equivalent. A confirmed leak in scope_subset means a change to NormalizedScope::is_subset_of introduced an iteration order or short-circuit that exposes parent-grant structure.


Reproduce

The parser and the arithmetic check themselves without a toolchain and without touching the filesystem:

bash
./scripts/check-dudect-threshold.sh --dry-run

A full harness run needs the dudect feature and a release build, and takes minutes. Quiesce the machine first; the verdict is a measurement, and a busy laptop produces readings the CI runner would not.

bash
cargo test -p chio-kernel-core --features dudect --release \
  --test dudect_mac_eq -- --nocapture | tee mac_eq.out
./scripts/check-dudect-threshold.sh --input mac_eq.out

Why the trust-boundary surface

chio-kernel-core does not expose its own mac_eq symbol; the kernel delegates byte-equality to the Signature type from chio-core-types, which is part of the same trust boundary. Measuring the underlying == directly catches data-dependent behavior in the implementation under test, without a wrapper that can change the measurement.

The same logic applies to NormalizedScope::is_subset_of: it is the authoritative capability-algebra subset check used by the proof-facing evaluation lane, so timing measurements there measure the relevant evaluation path.


Caveats

  • Detection, not proof. A clean dudect run is evidence the measured code path is constant-time on the harness machine and toolchain. It is not a proof. Microarchitectural variation (different CPU, different frequency scaling, different cache state) could surface a leak that the harness machine did not see.
  • Statistical noise. Welch's t on a shared runner is noisy, and the two-run correlation is the whole noise filter. It works by suppressing an alarm, not by making the measurement better, so a real leak that only shows on alternate nights raises nothing.
  • Compiler escape. mac_eq_bench returns a == b out of the run_one closure so black_box keeps the compare in the optimized binary. Its comment states the reason: assigning to _ would let --release LLVM eliminate the comparison and leave the harness measuring runner overhead.
  • Advisory, by design. Nothing on this page blocks a merge. A sustained leak produces a labelled GitHub issue, and acting on it is a human step.
  • Other side channels are out of scope. Power, electromagnetic, and microarchitectural (Spectre, etc.) channels are not addressed by chio. Operators relying on those mitigations need to apply OS, hypervisor, and hardware countermeasures themselves.

Next