Cumplimiento en compilación
El cumplimiento en compilación significa que las reglas sobre adónde
pueden ir los datos regulados las verifica el compilador, no un procedimiento.
Una clase regulatoria —HIPAA, GDPR, PCI_DSS y doce más— forma parte del
tipo de un valor, y un programa que la lleva a través de una frontera sin un
shield que la cubra se rechaza antes de ejecutarse.
Casi todos los sistemas tratan el cumplimiento como un proceso: un documento de política, una revisión, una auditoría que ocurre después de que el código existe. axon-lang lo trata como una propiedad del sistema de tipos, comprobada antes de que nada se ejecute.
La clase es un tipo
type PatientRecord compliance [HIPAA, GDPR] { ssn: String }
PatientRecord no tiene simplemente un comentario que diga que es sensible.
Sus clases regulatorias —escritas κ— viajan con él por todo el programa: por
los parámetros de un flow, por el body: y el output: de un
axonendpoint, por un manejador Channel<PatientRecord>, hasta un
axonstore.
Cuatro declaraciones pueden transportar una clase: type, shield,
axonendpoint y manifest.
La cobertura es una diferencia de conjuntos
La regla cabe en una frase:
Toda frontera que transporte una clase regulada debe declarar un shield cuya lista
compliance:cubra esa clase.
"Cubrir" significa una diferencia de conjuntos real, no una comprobación de presencia. Un shield que cubre algunas de las clases falla, y el diagnóstico nombra exactamente las que le faltan:
axon-T957 axonendpoint 'Api' declares `shield: PartialShield`, but that shield
does not cover kappa = {GDPR} carried across the boundary — the ESK coverage
rule. Add [GDPR] to shield 'PartialShield's `compliance:` list, or name a shield
that already covers them.
La regla guarda toda frontera portadora de κ:
| dónde | código |
|---|---|
| endpoints HTTP | axon-T957 |
| canales tipados, en la declaración | axon-T1215 |
publish del cálculo π, en ejecución, para IR que esquivó el verificador | falla cerrado |
El vocabulario es cerrado
type Record compliance [HIPPA] { ssn: String } // mal escrito a propósito
axon-T1214 type 'Record' declares `HIPPA`, which is not a regulatory class.
Did you mean `HIPAA`?
El registro canónico tiene quince miembros, y la pertenencia distingue mayúsculas de minúsculas:
HIPAA · PCI_DSS · GDPR · SOX · FINRA · ISO27001 · SOC2 ·
FISMA · GxP · CCPA · NIST_800_53 · NOM151 · LFPDPPP · LGPD ·
LEY1581
El cierre no es pulcritud — es lo que hace sólida la regla de cobertura. Si el vocabulario fuera abierto, una errata simétrica en el tipo y en el shield satisfaría la diferencia de conjuntos sin proteger absolutamente nada. Ese es el fallo que el catálogo cerrado vuelve irrepresentable.
Verificado otra vez en el despliegue
La comprobación en compilación responde a "¿pasó este código fuente?". Una compuerta de despliegue tiene una pregunta más difícil: "¿satisface este artefacto las obligaciones, lo haya construido quien lo haya construido?".
axon pcc prove emite un objeto de prueba; axon pcc verify vuelve a derivar
las obligaciones desde el artefacto, de forma independiente. Así, un programa
cuya IR nunca pasó por el verificador tampoco puede extruir una carga regulada —
el bus tipado deriva su predicado de la misma IR desde la que registra los
canales, y falla cerrado.
Qué demuestra esto, con precisión
Ser honesto sobre el límite forma parte del diseño, así que:
Lo que se comprueba automáticamente: el cierre del vocabulario
(axon-T1214) y la cobertura de shield en toda frontera portadora de κ
(axon-T957, axon-T1215), reverificado en el despliegue y en el publish. El
motor de auditoría puntúa que la cobertura se sostiene, nunca la presencia de
una etiqueta.
Lo que no: las obligaciones semánticas de cada norma. Lo que HIPAA exige
en la práctica es cosa del diseño de tus shields y tus flows. AXON pone el
mecanismo —NOM151 se corresponde con las cadenas de auditoría selladas de
axonstore; LFPDPPP, LGPD y LEY1581 con la redacción de shield y la cobertura
de κ— y tú pones la política. El motor de auditoría hace constar esa salvedad en
la evidencia que emite.
La postura frente a FIPS 140-3 es conforme algorítmicamente, no validada formalmente. CAVP y CMVP son procesos de laboratorio, y ningún compilador puede cerrarlos.
Preguntas frecuentes
¿AXON hace que mi sistema cumpla HIPAA o GDPR?
No, y nada en el lenguaje lo afirma. Lo que AXON comprueba automáticamente es
más estrecho y exacto: que cada clase regulatoria exista de verdad
(axon-T1214) y que toda frontera portadora de una clase declare un shield que
la cubra (axon-T957, axon-T1215). Las obligaciones operativas de cada norma
son cosa del diseño de tus shields y tus flows — ver
Qué demuestra esto, con precisión.
¿Qué pasa cuando una frontera no está cubierta?
axon check sale con 1, igual que ante un error de sintaxis, y el diagnóstico
nombra las clases que le faltan al shield. No se construye nada aguas abajo.
¿En qué se diferencia de los guardrails en tiempo de ejecución?
Un guardrail en ejecución inspecciona el tráfico mientras el sistema corre, así que un camino sin guardia se descubre —si se descubre— en producción. La regla de cobertura se verifica antes de que el programa exista como artefacto desplegable, así que un camino sin guardia no se puede desplegar. Las dos cosas se complementan: el shield es precisamente lo que actúa en ejecución cuando se detecta una brecha. El trabajo del compilador es garantizar que esté ahí.
¿La verificación ocurre solo al compilar?
No. Se repite en el despliegue, contra el artefacto (axon pcc verify), y el
bus tipado falla cerrado en el publish para una IR que nunca pasó por el
verificador.
¿Qué clases regulatorias existen?
Quince, en un registro cerrado que distingue mayúsculas — listadas en El vocabulario es cerrado.