harkaq: Q2 RESUELTA — el runtime base son 5 paths, y aparece una 3ª categoría
Método (lo importante): NO se adivina, se mide. MODE=base corre SIN ninguna dep
declarada ⇒ sin clausura que pueda explicarlas, toda denegación es runtime base
por definición. Aísla la respuesta sin juicio de valor.
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 salen en todos los builds y sin tratarlas entierran la deuda real.
La partición cierra en TRES categorías, todas medidas (§4.2):
- Contrato del sandbox: /src /out /tmp /dev/null(rw) /dev/urandom /proc
/opt/zig — los monta BWRAP, no son Alpine ⇒ no son deuda. Ésta era la línea
divisoria que faltaba.
- 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, y eso
hace viable todo el planteo.
- Denegación ESPERADA (no estaba en el diseño): /usr/bin/gcc. zig cc lo sondea
3× y el build sale rc=0 igual ⇒ 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. Es D3 literal ("una
denegación esperada no se calla, se CLASIFICA") y confirma que no tener
`quiet` era correcto: silenciarla habría borrado el hallazgo.
El contraste con el mismo runtime base:
MODE=base rc=0 Impuro [ /usr/bin/gcc ] ← esperada
MODE=zlib rc=1 Impuro [ /usr/lib/libz.so.1.3.2 ] ← DEUDA PURA, sin ruido
Consecuencia de diseño para el Verdict: las denegaciones tienen que venir
CLASIFICADAS (base|esperada|deuda), no en lista plana. `Hermetico` debe
significar "cero deuda", no "cero denegaciones" — si no, ningún build real lo
alcanzaría jamás.
Gotchas medidos: /dev/null es destino de ESCRITURA (rw, no ro) y el piso duro es
/bin/sh→busybox→ld-musl (sin eso ni el canario corre ⇒ sólo SinEvidencia).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
Claude Opus 4.8
+55
-18
@@ -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> /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**:
|
||||
|
||||
@@ -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`.
|
||||
|
||||
@@ -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 <stdio.h>
|
||||
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 <zlib.h>
|
||||
#include <stdio.h>
|
||||
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 \
|
||||
|
||||
Reference in New Issue
Block a user