gioser

sergio/takana

> Una distribución Linux construida con un laboratorio funcional y hermético en el > sótano, y una terminal mutable, clásica y anárquica en el piso de arriba — diseñada > desde el suelo para que una IA programadora entienda, modifique y co…

TOML 188Rust 55Shell 30Markdown 281211 Definitions

⎇ 8730aad34e868068796f9c85ca4e4c89cfb43fa6 scripts/qorpa/evidence-probe.sh Shell · 74 lines · 4.4 KB History raw

takana etapa 3b: las 49 invocaciones pasan a ./target/release/takana 8730aad34 · Sergio ·

1#!/bin/sh
2# Prueba el canal de evidencia de una instancia qorpa: que distinga HERMÉTICO de IMPURO, y que se
3# NIEGUE a opinar cuando no hay nada que medir. ADR 0015 D9 punto 3.
4#
5# ── POR QUÉ ESTE GUARDIÁN ───────────────────────────────────────────────────────────────────────
6# De un binario ajeno no hay fuente que leer: lo único observable es lo que el kernel le NIEGA y
7# anota. Si ese canal se rompe —caps que se pierden al recompilar, un kernel sin audit, una
8# política que ya no deniega nada—, el síntoma es **un veredicto limpio**. O sea que el modo de
9# fallo de este instrumento es *parecer que todo está bien*, y por eso hace falta medirlo con algo
10# que TIENE que salir sucio.
11#
12# ── LAS TRES ASERCIONES ─────────────────────────────────────────────────────────────────────────
13#   1. una instancia que no toca nada prohibido → HERMÉTICO
14#   2. la MISMA instancia tocando /usr y /opt   → IMPURO, y con esas rutas
15#   3. una instancia sin `seal_image`           → se NIEGA a correr (no hay nada denegable, así que
16#                                                 un `denials=[]` sería el instrumento mintiendo)
17# La 2 es la que sostiene a la 1: sin ella, «HERMÉTICO» lo cumple igual un canal muerto.
18set -eu
19
20QORPA_ROOT="${HAMMER_QORPA_ROOT:-/var/lib/hammer/qorpa}"
21HAMMER="${HAMMER_BIN:-./target/release/takana}"
22ID="${1:-arch-probe}"
23export HAMMER_QORPA_ROOT="$QORPA_ROOT"
24
25INST="$QORPA_ROOT/instances/$ID"
26[ -f "$INST/instance.toml" ] || { echo "no existe la instancia $ID en $QORPA_ROOT" >&2; exit 2; }
27
28AUDIT="${HARKAQ_BIN:-$HOME/.cache/harkaq}/harkaq-audit"
29if [ ! -x "$AUDIT" ]; then
30  echo "falta $AUDIT — gcc -O1 -Wall -o $AUDIT scripts/harkaq/harkaq-audit.c" >&2; exit 2
31fi
32# El `setcap` se pierde en CADA recompilación del lector, y ésa es la forma más probable de que el
33# canal muera sin que nadie se entere: por eso se comprueba acá y no se descubre en el veredicto.
34case "$(getcap "$AUDIT" 2>/dev/null)" in
35  *cap_audit_read*) : ;;
36  *) echo "el lector no tiene capabilities (se pierden al recompilar):" >&2
37     echo "  sudo setcap cap_audit_read,cap_audit_control+ep $AUDIT" >&2; exit 2 ;;
38esac
39
40LOG=$(mktemp -d); trap 'rm -rf "$LOG"' EXIT
41# A fichero y no a `$( )`: la sustitución espera al PIPE, no al proceso, y un descendiente vivo la
42# cuelga para siempre (misma cicatriz que `pressure-vessel-probe.sh`).
43corre() { timeout -k 5 180 "$HAMMER" qorpa run "$ID" --evidence -- /bin/sh -c "$1" > "$2" 2>&1 </dev/null || true; }
44
45sed -i 's/^seal_image = false/seal_image = true/' "$INST/instance.toml"
46
47echo "== 1. sin tocar nada prohibido"
48corre 'true' "$LOG/limpio"
49grep -q "HERMÉTICO" "$LOG/limpio" || { tail -5 "$LOG/limpio"; echo "FALLA: no dio hermético" >&2; exit 1; }
50echo "   HERMÉTICO ✓"
51
52echo "== 2. tocando la imagen sellada"
53corre 'touch /usr/INTRUSO 2>/dev/null; mkdir /opt/INTRUSO 2>/dev/null; true' "$LOG/sucio"
54grep -q "IMPURO" "$LOG/sucio" || { tail -8 "$LOG/sucio"; echo "FALLA: el canal no vio nada — un canal muerto se ve así" >&2; exit 1; }
55for ruta in "/usr" "/opt"; do
56  grep -q " $ruta\$" "$LOG/sucio" || { tail -8 "$LOG/sucio"; echo "FALLA: falta la denegación de $ruta" >&2; exit 1; }
57done
58grep -E "fs\.(make_reg|make_dir)" "$LOG/sucio" | sed 's/^/   /'
59echo "   IMPURO con las dos rutas ✓"
60
61echo "== 3. sin seal_image: tiene que NEGARSE, no dar limpio"
62sed -i 's/^seal_image = true/seal_image = false/' "$INST/instance.toml"
63corre 'true' "$LOG/sinsello"
64sed -i 's/^seal_image = false/seal_image = true/' "$INST/instance.toml"
65# Se busca la LÍNEA de veredicto (`evidencia: …`), no la palabra «denials»: el propio mensaje de
66# rechazo la contiene al explicar por qué se niega, y la primera versión de este guardián falló
67# contra su propia explicación.
68if grep -q "^evidencia:" "$LOG/sinsello"; then
69  tail -5 "$LOG/sinsello"; echo "FALLA: opinó sobre una política que no puede denegar nada" >&2; exit 1
70fi
71grep -q "seal_image" "$LOG/sinsello" || { tail -5 "$LOG/sinsello"; echo "FALLA: no explicó por qué se niega" >&2; exit 1; }
72echo "   se niega y dice por qué ✓"
73
74echo "OK: el canal de evidencia distingue hermético de impuro, y no opina cuando no puede medir"