From 77317a72911ad2fe7895b2e2da5a8d9ac812fbad Mon Sep 17 00:00:00 2001 From: sergio Date: Wed, 15 Jul 2026 15:35:42 -0400 Subject: [PATCH] harkaq: Verdict clasificado (base|esperada|deuda) + el runtime base es por forma de build MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit harkaq-verdict.py: clasifica las denegaciones crudas. Va DELIBERADAMENTE fuera del lector — éste corre con CAP_AUDIT_READ y clasificar es POLÍTICA, no privilegio (mismo argumento que Q1c). De yapa: se itera sin recompilar el binario capabilitado y sin perder el setcap. Las expectativas viajan en la propia política como `# expect ` (una sola fuente de verdad; harkaq-exec las ignora como comentario). SinEvidencia manda sobre todo: si el lector no es confiable no se clasifica nada — reinterpretarlo sería el falso Hermetico que el canario existe para impedir. MODE=base rc=0 Hermetico esperadas: /usr/bin/gcc deuda: ninguna ✓ MODE=zlib rc=1 Impuro DEUDA: /usr/lib/libz.so.1.3.2 §4.3 — ¿aguantan los 5 paths en otra forma de build? Medido con un configure de autotools REAL (libgpg-error, MODE=configure): ronda 1: /bin/bash, /bin/coreutils ronda 2: libacl, libattr, libcrypto, libreadline, libutmps ronda 3: libncursesw, libskarnet ronda 4: /usr/bin/c89, /usr/bin/c99, /usr/bin/ldd, /usr/bin/make NO: el runtime base es POR FORMA DE BUILD (~16 entradas para autotools, no 5). Pero converge en 3 rondas (34 denegaciones → 5) y se queda chico ⇒ la métrica de <5% de la Fase 2 sigue siendo plausible. Hallazgo: **el runtime base no es una lista de binarios, es su CIERRE de .so** (bash arrastra libreadline+libncursesw; coreutils arrastra libacl+libattr). Es computable con ldd, no adivinable ⇒ harkaq-policy debe derivarlo igual que deriva la clausura de las deps. Misma idea, otro origen. Y el residuo es todo señal, nada ruido: c89/c99/ldd son sondas de compilador de Alpine (→ esperadas, como gcc) y /usr/bin/make es una decisión de diseño real — hoy los builds de hammer usan el make de Alpine sin declararlo. Es EXACTAMENTE lo que los swaps del selfhost-verify reemplazan uno a uno: la lista de deuda de harkaq y la lista de swaps del bootstrap son la MISMA lista, descubierta por dos caminos independientes. Que coincidan es la mejor validación externa del método. Co-Authored-By: Claude Opus 4.8 --- docs/16-harkaq-jaula.md | 45 ++++++++++++++++ scripts/harkaq/README.md | 35 ++++++++++++ scripts/harkaq/harkaq-verdict.py | 88 +++++++++++++++++++++++++++++++ scripts/harkaq/q2-runtime-base.sh | 31 +++++++---- 4 files changed, 188 insertions(+), 11 deletions(-) create mode 100755 scripts/harkaq/harkaq-verdict.py diff --git a/docs/16-harkaq-jaula.md b/docs/16-harkaq-jaula.md index ad519d57..f927c717 100644 --- a/docs/16-harkaq-jaula.md +++ b/docs/16-harkaq-jaula.md @@ -429,6 +429,51 @@ Alpine. **Es exactamente el bug de §0, aislado en un build real y en una corrid 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. +Implementado en `harkaq-verdict.py`, **deliberadamente fuera del lector**: éste corre con +`CAP_AUDIT_READ` y clasificar es *política, no privilegio* (mismo argumento que Q1c). Las +expectativas viajan en la propia política como `# expect ` — una sola fuente de verdad, y +`harkaq-exec` las ignora como comentario. Medido: + +``` +MODE=base rc=0 Hermetico esperadas: /usr/bin/gcc deuda: ninguna ✓ +MODE=zlib rc=1 Impuro DEUDA: /usr/lib/libz.so.1.3.2 +``` + +### 4.3 ¿Aguantan los 5 paths? No — pero converge, y eso es lo que importa + +Los 5 paths de §4.2 son la respuesta para *un* shape de build (C mínimo con `zig cc`). La +pregunta honesta era si sobreviven a un `configure` de autotools, que sondea el sistema entero. +Medido contra una fuente **real** (`libgpg-error`, `MODE=configure`), iterando con el método de +§4.2 (cada línea sólo tras una denegación real): + +| Ronda | Deuda restante (paths únicos) | +|---|---| +| 1 | `/bin/bash`, `/bin/coreutils` | +| 2 | `libacl`, `libattr`, `libcrypto`, `libreadline`, `libutmps` | +| 3 | `libncursesw`, `libskarnet` | +| 4 | `/usr/bin/c89`, `/usr/bin/c99`, `/usr/bin/ldd`, `/usr/bin/make` | + +**Respuesta: no, el runtime base es por forma de build.** Un `configure` necesita ~16 entradas, +no 5. Pero las tres cosas que importan salieron bien: + +1. **Converge, y rápido** — 3 rondas, de 34 denegaciones a 5. No es una cola infinita. +2. **Se queda chico** — ~16 entradas, no cientos. La métrica de <5% de la Fase 2 sigue siendo + plausible. +3. **El runtime base no es una lista de binarios: es su CIERRE de `.so`.** Conceder `/bin/bash` + arrastra `libreadline`+`libncursesw`; conceder `/bin/coreutils` arrastra `libacl`+`libattr`. + Eso es *computable* (`ldd`), no adivinable ⇒ `harkaq-policy` debe derivar también el cierre + dinámico del runtime base, igual que deriva la clausura de las deps. Misma idea, otro origen. + +**Y el residuo es todo significativo, ninguno ruido:** + +- `c89`, `c99`, `ldd` — la misma familia que `gcc` (§4.2): sondas de compilador de Alpine. Van a + **denegación esperada**; concederlas sería dejar que `configure` compile con Alpine. +- `/usr/bin/make` — **la decisión de diseño de verdad**, y no la toma harkaq. Hoy los builds de + hammer usan el `make` de Alpine sin declararlo. O es runtime base (se acepta y se escribe), o + es deuda (y se declara como dep). Nótese que esto es *exactamente* lo que los swaps del + `selfhost-verify` reemplazan uno a uno: **la lista de deuda de harkaq y la lista de swaps del + bootstrap son la misma lista, descubierta por dos caminos.** Que coincidan es la mejor + validación externa que tiene el método. --- diff --git a/scripts/harkaq/README.md b/scripts/harkaq/README.md index 8641464e..02bf652d 100644 --- a/scripts/harkaq/README.md +++ b/scripts/harkaq/README.md @@ -198,3 +198,38 @@ Tres categorías, todas medidas (detalle en `docs/16-harkaq-jaula.md` §4.2): 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`. + +### ¿Aguantan los 5 paths en otra forma de build? No — pero converge (§4.3) + +`MODE=configure` corre un `configure` de autotools **real** (`work/sources/libgpg-error-*`, +override con `Q2_SRC`). Iterando con el mismo método: + +| Ronda | Deuda restante (paths únicos) | +|---|---| +| 1 | `/bin/bash`, `/bin/coreutils` | +| 2 | `libacl`, `libattr`, `libcrypto`, `libreadline`, `libutmps` | +| 3 | `libncursesw`, `libskarnet` | +| 4 | `/usr/bin/c89`, `/usr/bin/c99`, `/usr/bin/ldd`, `/usr/bin/make` | + +El runtime base es **por forma de build** (~16 entradas para autotools, no 5), pero **converge en +3 rondas y se queda chico** ⇒ la métrica de <5% de la Fase 2 sigue siendo plausible. + +Lo importante: **el runtime base no es una lista de binarios, es su cierre de `.so`** (bash +arrastra libreadline+libncursesw; coreutils arrastra libacl+libattr). Es computable con `ldd`, no +adivinable — `harkaq-policy` debería derivarlo igual que deriva la clausura de las deps. + +Y el residuo es todo señal: `c89`/`c99`/`ldd` son sondas de compilador de Alpine (→ esperadas, +como `gcc`), y `/usr/bin/make` es una decisión de diseño real — hoy los builds usan el `make` de +Alpine sin declararlo. **Es la misma lista que reemplazan los swaps del `selfhost-verify`**, +descubierta por otro camino. + +### El clasificador va FUERA del lector + +`harkaq-verdict.py [--human]`. El lector tiene `CAP_AUDIT_READ`; +clasificar es política, no privilegio. Mantenerlo tonto es el argumento de Q1c, y de yapa se +itera la clasificación sin recompilar el binario capabilitado (sin perder el `setcap`). + +Las expectativas viajan en la política como `# expect ` — una sola fuente de verdad, y +`harkaq-exec` las ignora como comentario. `SinEvidencia` manda sobre todo: si el lector no es +confiable no se clasifica nada, porque reinterpretarlo sería el falso `Hermetico` que el canario +existe para impedir. diff --git a/scripts/harkaq/harkaq-verdict.py b/scripts/harkaq/harkaq-verdict.py new file mode 100755 index 00000000..b84d2e1f --- /dev/null +++ b/scripts/harkaq/harkaq-verdict.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""harkaq-verdict — clasifica las denegaciones crudas y emite el Verdict final (SDD 16 §4.2). + + harkaq-verdict.py [--human] + +Por qué es un proceso aparte y NO parte de harkaq-audit: el lector corre con CAP_AUDIT_READ, y +clasificar es POLÍTICA, no privilegio. El componente privilegiado se mantiene lo más tonto +posible — mismo argumento que Q1c (el privilegio en un helper chico, no en hammerd). Efecto +lateral útil: se itera la clasificación sin recompilar el binario capabilitado (y sin perder el +setcap en cada cambio). + +Las tres categorías salen de la medición de §4.2: + + base concedida por la política ⇒ nunca aparece como denegación. No se clasifica acá. + esperada denegada A PROPÓSITO y previsible. `zig cc` sondea /usr/bin/gcc y el build sale rc=0 + igual: concederlo lo dejaría usar el gcc de Alpine por detrás. Se declara en la + política con `# expect ` — la MISMA fuente de verdad que las reglas, y + harkaq-exec la ignora como comentario. D3: no se calla, se clasifica. + deuda todo lo demás. ESTO es la de-Alpinización: lo que el build usó sin declarar. + +Y la consecuencia que obliga: `Hermetico` = **cero deuda**, no cero denegaciones. Con la +definición estricta ningún build real lo alcanzaría jamás y el estado más importante del sistema +quedaría vacío de uso. +""" +import json +import sys + + +def cargar_esperadas(politica): + """Lee los `# expect ` de la política. Un fichero, una fuente de verdad.""" + esperadas = set() + with open(politica) as f: + for linea in f: + linea = linea.strip() + if linea.startswith("# expect "): + esperadas.add(linea[len("# expect "):].strip()) + return esperadas + + +def main(): + if len(sys.argv) < 3: + print(__doc__.split("\n")[2].strip(), file=sys.stderr) + return 2 + crudo = json.load(open(sys.argv[1])) + esperadas = cargar_esperadas(sys.argv[2]) + humano = "--human" in sys.argv + + # SinEvidencia manda sobre todo: si el lector no es confiable, no clasificamos nada. Un + # veredicto sin canario no es "limpio", es "no sabemos" (D9), y reinterpretarlo acá sería + # justo el falso Hermetico que el canario existe para impedir. + if crudo["estado"] == "SinEvidencia": + salida = dict(crudo, esperadas=[], deuda=[]) + print(json.dumps(salida) if not humano else + f"SinEvidencia — {crudo.get('motivo', 'sin motivo')}") + return 3 + + vistas_esperadas, deuda = [], [] + for d in crudo["denials"]: + (vistas_esperadas if d["path"] in esperadas else deuda).append(d) + + estado = "Hermetico" if not deuda else "Impuro" + salida = { + "estado": estado, + "canario_visto": crudo["canario_visto"], + "domain": crudo["domain"], + "contador_kernel": crudo["contador_kernel"], + "esperadas": vistas_esperadas, + "deuda": deuda, + } + + if not humano: + print(json.dumps(salida)) + else: + print(f" estado: {estado} (canario visto, contador kernel={crudo['contador_kernel']})") + if vistas_esperadas: + uniq = sorted({d["path"] for d in vistas_esperadas}) + print(f" esperadas ({len(vistas_esperadas)}): " + ", ".join(uniq)) + if deuda: + print(f" DEUDA ({len(deuda)}) — usado sin declarar:") + for p in sorted({d["path"] for d in deuda}): + print(f" {p}") + else: + print(" deuda: ninguna ✓") + return 0 if estado == "Hermetico" else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/harkaq/q2-runtime-base.sh b/scripts/harkaq/q2-runtime-base.sh index cbfff15c..963e6203 100755 --- a/scripts/harkaq/q2-runtime-base.sh +++ b/scripts/harkaq/q2-runtime-base.sh @@ -30,7 +30,16 @@ MODE="${MODE:-zlib}" WORK=$(mktemp -d); trap 'rm -rf "$WORK"' EXIT mkdir -p "$WORK/src" "$WORK/out" -if [ "$MODE" = base ]; then +if [ "$MODE" = configure ]; then + # Una fuente autotools REAL. `configure` sondea el sistema entero (cientos de tests con + # sed/grep/awk/rm...), así que es la prueba de si el runtime base de 5 paths medido contra + # un `zig cc` mínimo aguanta, o si es POR FORMA DE BUILD. Es la pregunta que decide si la + # métrica de <5% de la Fase 2 es alcanzable. + DEPS="" + SRCDIR="${Q2_SRC:-work/sources/libgpg-error-7a85413f2bc354f4}" + [ -d "$SRCDIR" ] || { echo "falta $SRCDIR"; exit 1; } + cp -a "$SRCDIR"/. "$WORK/src/" +elif [ "$MODE" = base ]; then DEPS="" LDFLAGS="" cat > "$WORK/src/hello.c" <<'EOF' @@ -63,6 +72,9 @@ POLICY="$WORK/policy" # llena SÓLO con lo que el kernel denunció — nunca por corazonada. Cada línea de acá es una # respuesta medida a Q2, no una conjetura. [ -n "${BASE_EXTRA:-}" ] && printf '%s\n' "$BASE_EXTRA" + # Denegaciones ESPERADAS (§4.2): se deniegan a propósito y se declaran acá para que el + # clasificador no las cuente como deuda. harkaq-exec las ignora (empiezan con #). + [ -n "${EXPECT:-}" ] && printf '# expect %s\n' $EXPECT } >> "$POLICY" echo "── MODE=$MODE deps=[${DEPS:-ninguna}]" >&2 @@ -88,7 +100,12 @@ 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 $LDFLAGS -o /out/hello && echo BUILD-OK" +if [ "$MODE" = configure ]; then + BUILD='cd /src && ./configure --prefix=/usr >/tmp/conf.log 2>&1; echo "configure rc=$?"' +else + BUILD='cd /src && zig cc -mcpu=baseline hello.c '"$LDFLAGS"' -o /out/hello && echo BUILD-OK' +fi +CMD="read _ < $CANARY || true; $BUILD" set +e bwrap --overlay-src "$ROOTFS" $(for d in $DEPS; do printf -- "--overlay-src %s " "$d"; done) --tmp-overlay / \ @@ -110,12 +127,4 @@ kill -TERM "$AUDIT_PID" 2>/dev/null || true wait "$AUDIT_PID" 2>/dev/null || true echo "── build rc=$RC" >&2 -echo "── denegaciones (= candidatos a runtime base):" >&2 -python3 -c ' -import json,sys -v=json.load(open(sys.argv[1])) -print(" estado:", v["estado"], "| canario:", v["canario_visto"], "| contador kernel:", v["contador_kernel"]) -for d in v["denials"]: - print(" ", d["blockers"], d["path"]) -if not v["denials"]: print(" (ninguna)") -' "$VERDICT" +scripts/harkaq/harkaq-verdict.py "$VERDICT" "$POLICY" --human