harkaq: Verdict clasificado (base|esperada|deuda) + el runtime base es por forma de build
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 <path>` (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 <noreply@anthropic.com>
This commit is contained in:
Claude Opus 4.8
@@ -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 <verdict-crudo> <politica> [--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 <path>` — 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.
|
||||
|
||||
Executable
+88
@@ -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 <verdict-crudo.json> <politica> [--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 <path>` — 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 <path>` 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())
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user