diff --git a/docs/16-harkaq-jaula.md b/docs/16-harkaq-jaula.md index cdf3286c..ad519d57 100644 --- a/docs/16-harkaq-jaula.md +++ b/docs/16-harkaq-jaula.md @@ -378,6 +378,58 @@ Dos consecuencias de diseño: un fichero regular hacen que el kernel rechace la regla entera con `EINVAL`. Como la clausura es mayormente ficheros sueltos, sin recortar por tipo no arranca ni la primera regla. +### 4.2 Q2 resuelta: el runtime base son 5 paths, y hay una tercera categoría + +El método es lo importante: **no se adivina, se mide**. `scripts/harkaq/q2-runtime-base.sh` corre +un build real en el sandbox real con `política = clausura declarada` y deja que las denegaciones +nombren el resto. `MODE=base` (sin **ninguna** dep declarada) aísla la respuesta sin juicio de +valor: sin clausura que pueda explicarlas, *toda* denegación es runtime base por definición. + +`MODE=base`, `hello.c` mínimo con `zig cc` — 18 denegaciones, 4 paths distintos (contador del +kernel 19 = 18 + canario ✓): + +``` +8× /dev/urandom 6× /usr/lib/os-release 3× /dev/null 1× /usr/bin/env +``` + +**Y el build salió `rc=0`.** No son cosas que el build *necesite*: son cosas que *intenta*. Pero +aparecen en todos los builds, así que sin tratarlas cada veredicto sale `Impuro` con los mismos +paths y la deuda real queda enterrada. Iterando (cada línea añadida sólo tras una denegación +real, nunca por corazonada) la partición se cierra en **tres** categorías: + +| Categoría | Qué | Qué hacer | +|---|---|---| +| **Contrato del sandbox** | `/src`, `/out`, `/tmp`, `/dev/null` (**rw**: es destino de escritura), `/dev/urandom`, `/proc`, `/opt/zig` | conceder — **los crea bwrap, no son Alpine** | +| **Runtime base Alpine** | `/bin/sh`, `/bin/busybox`, `/lib/ld-musl-x86_64.so.1`, `/usr/bin/env`, `/usr/lib/os-release` | conceder — irreducible, y son **5** | +| **Denegación esperada** | `/usr/bin/gcc` | **denegar y clasificar** (D3) | + +La primera línea divisoria es la que hacía falta: `/dev` y `/proc` **los monta bwrap**, no salen +del rootfs Alpine ⇒ son superficie de contrato como `/src`, no deuda. Sólo 5 paths de Alpine son +irreducibles. Eso hace viable todo el planteo: **el resto de Alpine es, genuinamente, deuda**. + +**La tercera categoría no estaba en el diseño y es la más interesante.** `zig cc` sondea +`/usr/bin/gcc` (`fs.execute,fs.read_file`, 3 veces) y el build igual sale `rc=0` sin él. Esa +denegación **no es ruido a permitir: es la jaula haciendo su trabajo**. Concederla dejaría a zig +invocar el gcc de Alpine por detrás — justo lo que la campaña *matar gcc* persigue a mano. harkaq +da evidencia mecánica de que zig lo intenta *y* de que negárselo no rompe el build. Es D3 literal +("una denegación esperada no se calla, se *clasifica*"), y confirma que la decisión de no tener +`quiet` era correcta: silenciarla habría borrado el hallazgo. + +**El contraste, con el mismo runtime base:** + +``` +MODE=base rc=0 Impuro, denegaciones = [ /usr/bin/gcc ] ← esperada +MODE=zlib rc=1 Impuro, denegaciones = [ /usr/lib/libz.so.1.3.2 ] ← DEUDA PURA +``` + +Una sola denegación, sin ruido: el build se linkaba contra **la zlib de Alpine** en vez de la dep +declarada (que aporta `libz.a`). Sin harkaq eso pasa en verde y el artefacto queda dependiendo de +Alpine. **Es exactamente el bug de §0, aislado en un build real y en una corrida de 20 segundos.** + +Consecuencia para el `Verdict`: los tres estados de D9 necesitan que las denegaciones vengan +**clasificadas** (`base` | `esperada` | `deuda`), no en una lista plana. `Hermetico` debe +significar "cero deuda", no "cero denegaciones" — si no, ningún build real lo alcanzaría jamás. + --- ## 5. Decisiones cerradas @@ -626,24 +678,9 @@ vibra. - **Q1d (Fase 1, menor):** el `exe=` del registro trae la ruta **del host**. Con el sandbox real (`--bind /src`) hay que confirmar qué ruta reporta para un builder que vive en `/src`, y si sirve para algo o basta con `domain=`. -- **Q2 (Fase 2) — EN CURSO, con método y primeros datos.** ¿Qué es el "runtime base" que toda - receta necesita y ninguna declara? *Sigue siendo la decisión de diseño de verdad* — determina si - la métrica de la Fase 2 mide deuda real o ruido. **El método está resuelto: no se adivina, se - mide.** `scripts/harkaq/q2-runtime-base.sh` corre un build real en el sandbox real con - `política = clausura declarada` y deja que las denegaciones nombren el resto. - - Medido (2026-07-15), compilando contra la dep `zlib` del store: - - **Piso duro:** `/bin/sh` → `/bin/busybox` → `/lib/ld-musl-x86_64.so.1`. Sin esto ni el canario - corre (el `execvp` de `/bin/sh` rebota) ⇒ `SinEvidencia` y cero diagnóstico. El runtime base - mínimo es, literalmente, *lo que hace falta para que el canario pueda correr*. - - **Candidato:** `/usr/bin/env` — legítimo, ninguna receta lo declara ni debería. - - **Y el hallazgo que justifica el proyecto:** `fs.read_file /usr/lib/libz.so.1.3.2`. El build - se linkaba contra **la zlib de Alpine** en vez de la dep declarada (que aporta `libz.a`). Sin - harkaq eso pasa en verde y el artefacto queda dependiendo de Alpine. Con harkaq el kernel lo - nombra, con path e inode. **Es exactamente el bug de §0, cazado en un build real.** - - Falta: correrlo sobre el catálogo y separar el runtime base (pocos, estables, en todas las - recetas) de la deuda real (variable, por receta). Esa separación *es* la respuesta a Q2. +- **Q2 — ✅ RESPONDIDA (2026-07-15), y el resultado es mejor de lo esperado.** Ver §4.2. El + runtime base de Alpine son **5 paths**, medidos; la deuda queda aislada sin ruido; y apareció + una tercera categoría que no estaba en el diseño: la *denegación esperada*. - **Q3 (Fase 2):** ¿`/proc` y `/dev` mínimos rompen builds reales? (`/proc/self` suele hacer falta; `/proc/sys` casi nunca.) bwrap ya monta `--proc /proc --dev /dev`. - **Q4:** ¿el `Verdict` entra en `Recipe::hash_inputs`? Por simetría con `Evidence` (H1), **no**: diff --git a/scripts/harkaq/README.md b/scripts/harkaq/README.md index 463f2635..8641464e 100644 --- a/scripts/harkaq/README.md +++ b/scripts/harkaq/README.md @@ -168,3 +168,33 @@ estado: Impuro | canario: True | contador kernel: 3 El segundo lo cazó **D9 mismo**: el lector se negó a certificar (`SinEvidencia`) en vez de decir `Hermetico`. El canario funcionando como se diseñó, sobre un bug de quien lo diseñó. + +### Q2 resuelta: el runtime base son 5 paths (2026-07-15) + +`MODE=base` corre **sin ninguna dep declarada**: sin clausura que pueda explicarlas, toda +denegación es runtime base por definición. Eso aísla la respuesta sin juicio de valor. + +```sh +export BASE_EXTRA='ro /bin/sh +ro /bin/busybox +ro /lib/ld-musl-x86_64.so.1 +ro /usr/bin/env +ro /usr/lib/os-release +rw /dev/null +ro /dev/urandom' +MODE=base scripts/harkaq/q2-runtime-base.sh # rc=0, sólo queda /usr/bin/gcc (esperada) +MODE=zlib scripts/harkaq/q2-runtime-base.sh # Impuro: [/usr/lib/libz.so.1.3.2] — deuda pura +``` + +Tres categorías, todas medidas (detalle en `docs/16-harkaq-jaula.md` §4.2): + +- **Contrato**: `/src /out /tmp /dev/null(rw) /dev/urandom /proc /opt/zig` — los monta bwrap, no + son Alpine. +- **Runtime base Alpine**: `/bin/sh /bin/busybox /lib/ld-musl /usr/bin/env /usr/lib/os-release`. + Cinco. El resto de Alpine es deuda genuina. +- **Denegación esperada**: `/usr/bin/gcc` — `zig cc` lo sondea y el build sale `rc=0` igual. + Concederla dejaría a zig usar el gcc de Alpine por detrás. **Se deniega y se clasifica** (D3). + +Ojo con dos: `/dev/null` es destino de **escritura** (`rw`, no `ro` — con `ro` quedan +`fs.write_file` colgando), y el piso duro es `/bin/sh`→`busybox`→`ld-musl`: sin eso ni el canario +corre y no hay diagnóstico, sólo `SinEvidencia`. diff --git a/scripts/harkaq/q2-runtime-base.sh b/scripts/harkaq/q2-runtime-base.sh index 14d98122..cbfff15c 100755 --- a/scripts/harkaq/q2-runtime-base.sh +++ b/scripts/harkaq/q2-runtime-base.sh @@ -17,23 +17,43 @@ cd "$(dirname "$0")/../.." BIN="${HARKAQ_BIN:-$HOME/.cache/harkaq}" ROOTFS=.dev-fs/alpine ZIG=.dev-fs/tools/zig -DEP=$(ls -d store/*-zlib | head -1) + +# MODE=base → build SIN ninguna dep declarada. Por definición, TODA denegación es runtime base: +# no hay clausura que pueda explicarla. Aísla la respuesta a Q2 sin juicio de valor. +# MODE=zlib → el mismo build contra la dep zlib del store. Lo que sobre por encima del runtime +# base ES la deuda de de-Alpinización, sin ambigüedad. +MODE="${MODE:-zlib}" [ -d "$ROOTFS" ] || { echo "falta $ROOTFS"; exit 1; } [ -d "$ZIG" ] || { echo "falta $ZIG"; exit 1; } WORK=$(mktemp -d); trap 'rm -rf "$WORK"' EXIT mkdir -p "$WORK/src" "$WORK/out" -cat > "$WORK/src/hello.c" <<'EOF' + +if [ "$MODE" = base ]; then + DEPS="" + LDFLAGS="" + cat > "$WORK/src/hello.c" <<'EOF' +#include +int main(void) { printf("hola\n"); return 0; } +EOF +else + DEPS=$(ls -d store/*-zlib | head -1) + LDFLAGS="-lz" + cat > "$WORK/src/hello.c" <<'EOF' #include #include int main(void) { printf("zlib %s\n", zlibVersion()); return 0; } EOF +fi # La clausura DECLARADA (D1) + las superficies que el sandbox define por contrato, no la receta: # /src (fuentes), /out (DESTDIR), /tmp (HOME). Nada de Alpine. POLICY="$WORK/policy" -scripts/harkaq/harkaq-policy.sh "$DEP" > "$POLICY" +# Sin deps (MODE=base) la clausura declarada es VACÍA: la política son sólo las +# superficies de contrato del sandbox. Todo lo demás que el build toque, se ve. +: > "$POLICY" +[ -n "$DEPS" ] && scripts/harkaq/harkaq-policy.sh $DEPS > "$POLICY" { echo "rw /src" echo "rw /out" @@ -45,6 +65,7 @@ scripts/harkaq/harkaq-policy.sh "$DEP" > "$POLICY" [ -n "${BASE_EXTRA:-}" ] && printf '%s\n' "$BASE_EXTRA" } >> "$POLICY" +echo "── MODE=$MODE deps=[${DEPS:-ninguna}]" >&2 echo "── política: $(grep -c '^ro ' "$POLICY") ro, $(grep -c '^list ' "$POLICY") list, $(grep -c '^rw ' "$POLICY") rw" >&2 NONCE="q2-$$" @@ -67,10 +88,10 @@ read -r _ < "$FIFO" || true # El probe del canario usa SÓLO builtins del shell: `read` + redirección. Con `cat` dependía de # /bin/cat (otro applet de busybox) y, si no estaba en la clausura, el probe moría sin probar # nada — el canario tiene que ser lo más barato e independiente del sistema. -CMD="read _ < $CANARY || true; cd /src && zig cc -mcpu=baseline hello.c -lz -o /out/hello && echo BUILD-OK" +CMD="read _ < $CANARY || true; cd /src && zig cc -mcpu=baseline hello.c $LDFLAGS -o /out/hello && echo BUILD-OK" set +e -bwrap --overlay-src "$ROOTFS" --overlay-src "$DEP" --tmp-overlay / \ +bwrap --overlay-src "$ROOTFS" $(for d in $DEPS; do printf -- "--overlay-src %s " "$d"; done) --tmp-overlay / \ --proc /proc --dev /dev --tmpfs /tmp \ --ro-bind "$ZIG" /opt/zig \ --bind "$WORK/src" /src --bind "$WORK/out" /out \