BIBLIOTECA ASTRACode Cyber

CAPÍTULO 49 · PARTE V

Programas como transformación de estado y datos

Modela un programa como transiciones sobre estado y datos, con invariantes, pre/postcondiciones, efectos y decisiones sobre determinismo.

Nivel N2 · Estado published

Un programa de seguridad puede devolver el valor correcto y aun así dejar el sistema en un estado incorrecto. Puede aceptar una solicitud sin registrar la decisión, repetir un débito después de un timeout o publicar un dato antes de comprobar una precondición. Para razonar profesionalmente no basta con preguntar «¿qué salida produce?». Hay que reconstruir qué entra, qué estado lee, qué estado modifica, qué efectos externos intenta y qué propiedades deben conservarse.

En este capítulo, un programa se modela como una relación de transición entre estados. El foco es semántico: qué significa una operación y qué garantías se pueden observar. La representación de tipos, la memoria, el control de flujo y el parsing quedan reservados a los capítulos 50–52; aquí sólo aparecen como fronteras que pueden invalidar un contrato.

La unidad mínima: estado, entrada, salida y efecto

Un estado S reúne los hechos relevantes en un instante: saldo disponible, versión de una configuración, identidad del principal, estado de un pedido y eventos ya registrados. Una entrada I es información suministrada por un actor o por otro sistema. Una transición T produce un nuevo estado S', una salida O y, cuando corresponde, efectos E sobre sistemas externos:

T(S, I) → (S', O, E)

La notación no promete que toda transición termine ni que sea pura. Sirve para separar observación de inferencia. Un log puede mostrar O = accepted; no demuestra que S' se haya persistido ni que E haya llegado al receptor. La frontera de confianza importa: una entrada recibida por red no tiene la misma autoridad que una decisión ya validada por el componente que protege el recurso.

En Asteria, reserve(order, quantity) lee inventario y una versión de la reserva, comprueba la identidad del servicio y escribe una reserva. La salida reserved sólo es completa si el estado persistido refleja la reserva y el efecto downstream, si existe, tiene un contrato explícito. Si el proceso cae después de escribir y antes de publicar el evento, existen al menos dos estados observables; no deben comprimirse en una etiqueta «éxito».

Figura 49-01 · ¿Qué transforma una operación y qué queda como efecto separado?

Vista adaptada. Toca el diagrama para ampliarlo.

Una transición toma estado e input no confiable, comprueba el contrato y produce nuevo estado, salida y efectos separados.

Del estado abstracto a la observación operacional

El estado que usamos para razonar no coincide necesariamente con una fila, una variable o un registro. Es un estado abstracto: el conjunto mínimo de hechos que permite decidir si el contrato se conserva. Una implementación puede representar reservation = pending con una fila, un log y una caché; el modelo sigue siendo uno solo si todos esos artefactos se interpretan de manera coherente. La representación es el soporte concreto: columnas, bytes, índices, mensajes, handles y metadatos. Confundir ambos niveles produce dos errores opuestos: declarar que una fila es la verdad completa, o ignorar que una representación parcial puede permitir estados incompatibles.

El refinamiento relaciona ambos niveles mediante una función de abstracción. Si R es la representación concreta y α(R) su estado abstracto, una operación correcta debe preservar que la representación pertenece al dominio válido y que α(R') satisface la postcondición. La función no tiene que ser computable como una operación de producción; es una herramienta de revisión. En Asteria, una reserva puede tener una fila confirmed y un evento aún no publicado. α(R) debe expresar ambas cosas, no fingir que «confirmada» implica «notificada».

La observabilidad añade una tercera capa. Un sistema expone salidas, métricas, logs y eventos, pero éstos son proyecciones del estado, no el estado completo. Una métrica reservations_total permite detectar volumen; no permite reconstruir por sí sola qué tenant fue autorizado. Un log con request_id, versión, decisión y timestamps puede conservar procedencia sin copiar un secreto. El diagnóstico debe indicar qué se observó directamente, qué se infiere por correlación y qué permanece desconocido. En particular, una ausencia de evento puede significar pérdida, retraso, filtrado o que la transición nunca empezó.

Para cada transición conviene escribir una tabla pequeña: entrada recibida, estado abstracto leído, representación consultada, decisión, estado abstracto esperado, artefactos concretos que deben cambiar y evidencia de cada cambio. Esta tabla no sustituye pruebas; impide que una salida HTTP o un log de aplicación se conviertan en prueba de persistencia. También permite detectar datos que cruzan una frontera sin autoridad, por ejemplo un tenant_id copiado desde una petición hacia una escritura sin una relación comprobada con el principal.

Invariantes: lo que debe seguir siendo cierto

Un invariante es una propiedad que debe conservarse en todos los estados aceptables de un ámbito definido. El ámbito evita promesas universales. Para Asteria, stock_available ≥ 0 puede ser invariante de inventario; reservation.version debe aumentar una sola vez por transición aceptada; y una reserva no debe asociarse a un tenant distinto del principal autorizado. No se afirma que todo el sistema preserve esas propiedades sin declarar quién escribe y qué transacciones cubren.

El invariante no es una validación aislada. Si se comprueba saldo en una lectura y otra operación puede escribir antes de la persistencia, la propiedad puede romperse aunque ambas funciones parezcan correctas. La pregunta causal es qué conjunto de lectura y escritura constituye una transición indivisible, y qué ocurre ante reintento o fallo parcial. La atomicidad es una propiedad del contrato de la operación y de su frontera de almacenamiento, no un sinónimo de «función corta».

Un invariante negativo es igual de útil: «ningún evento incluye el secreto de pago», «una petición no cambia de tenant durante la transición» o «un efecto externo no se confirma dos veces con el mismo identificador». Estas propiedades dirigen pruebas y observabilidad. La ausencia de una alerta no prueba que el invariante se haya mantenido.

Invariantes locales y globales: refinar sin prometer demasiado

Un invariante local se conserva dentro de un componente o transacción: una fila de inventario no baja de cero, un contador monotónico no retrocede o una clave de idempotencia sólo se asocia a un resultado. Un invariante global atraviesa varios componentes: una reserva confirmada no puede cobrarse dos veces, una identidad de producción no debe mutar en identidad de staging o un evento publicado debe corresponder a una versión persistida. El segundo no se deduce automáticamente del primero.

El refinamiento debe hacer visible la composición. Si el servicio A escribe reserved y el broker B publica un evento, hay un intervalo en el que A puede haber terminado y B no. Una garantía global necesita una relación adicional —por ejemplo, un registro de outbox transaccional o una reconciliación— y una política para estados parciales. Decir «la transacción es atómica» sin nombrar el ámbito sólo oculta la frontera.

Los invariantes también tienen alcance temporal. «Nunca se reutiliza una clave de idempotencia» puede significar durante la vida del pedido, durante una ventana de 24 horas o mientras exista el registro. «El token no se usa después de revocación» depende de cachés y receptores. Es preferible declarar la ventana y el observador: ∀ t dentro del almacenamiento primario, o «en cada receptor que haya confirmado la actualización». Así se evita convertir una propiedad operacional en una afirmación universal.

Un análisis adversarial busca qué acción rompe cada invariante: reintento, concurrencia, replay, caída entre dos efectos, restauración desde backup o configuración de un tenant equivocado. Para cada caso se determina si la transición debe rechazar, compensar, reanudar o quedar en unknown. La seguridad no consiste sólo en mantener estados felices; consiste en limitar la autoridad de estados incompletos.

Precondiciones y postcondiciones hacen auditable una decisión

La precondición delimita cuándo una transición está autorizada a empezar; la postcondición describe qué debe ser cierto si termina aceptada. Para reserve:

Una precondición fallida debe producir rechazo explícito, no una postcondición parcial. Una postcondición desconocida después de un timeout debe quedar como unknown o review, no convertirse en éxito por conveniencia. Este modelo sigue la lógica de aserciones de Hoare: {P} C {Q} expresa una relación entre estado inicial, comando y estado final; no es una prueba de disponibilidad, rendimiento o ausencia de errores fuera de P y Q.

El contrato también declara salidas negativas: deny por autorización, conflict por versión, invalid por entrada fuera de dominio y unknown cuando no se puede observar el efecto. Distinguirlas evita que un cliente reintente una denegación como si fuera una pérdida transitoria, o que trate un conflicto como prueba de que la reserva nunca existió.

Figura 49-02 · ¿Cómo se distinguen aceptación, rechazo y estado desconocido?

Vista adaptada. Toca el diagrama para ampliarlo.

Las precondiciones separan el rechazo de la ejecución; sólo una postcondición observada acredita aceptación y una observación inconclusa conserva el estado desconocido.

Atomicidad, linealización y consistencia

Atomicidad significa que, dentro de un ámbito declarado, una transición no se observa como una mezcla arbitraria de antes y después. No implica que todos los sistemas remotos cambien juntos. Linealización es el modelo más fuerte para una operación concurrente: cada llamada parece ocurrir en un punto entre su inicio y su fin, respetando el orden de llamadas que ya terminó antes. Una base de datos puede ofrecer atomicidad y serialización para sus filas, mientras un servicio externo observa el efecto después; el contrato debe decirlo.

La consistencia tiene varios sentidos. En el modelo de invariantes, es conservar reglas válidas. En un sistema distribuido, puede referirse a qué lecturas ven qué escrituras y cuándo. No deben usarse como sinónimos. Una lectura eventualmente consistente puede ser aceptable para una vista de métricas y peligrosa para una decisión de autorización. La pregunta correcta es qué lectura necesita qué operación, no si el sistema es «consistente» en abstracto.

Cuando la transición toca un único almacenamiento, el diseño puede usar una condición de versión: leer v, escribir sólo si continúa v, y devolver conflict si otro actor ganó. Cuando toca dos almacenes, no conviene simular atomicidad con dos llamadas independientes. Se explicita un protocolo: estado pendiente, confirmación posterior, compensación o revisión manual. El capítulo 51 tratará mecanismos de ejecución y memoria; aquí importa el contrato observable y la frontera de la garantía.

Una caída es parte del modelo. Si ocurre antes del punto de linealización, la operación puede no haber tenido efecto; si ocurre después, puede haberlo tenido aunque el cliente no reciba respuesta. Sin una clave de correlación y una consulta segura del estado, el cliente no puede adjudicarlo. Reintentar ciegamente transforma incertidumbre en posible duplicación. Un endpoint de consulta idempotente o una operación con clave estable permite resolver el estado sin volver a aplicar el efecto.

Determinismo, nondeterminismo y efectos observables

Una transición es determinista en un modelo si el mismo estado, entrada y contexto fijado produce un único resultado. El contexto incluye reloj, configuración, identidad de la dependencia y orden de efectos; omitirlo hace pasar por determinista una operación que depende de datos no modelados. La aleatoriedad es una fuente concreta de variación; el nondeterminismo también puede surgir de elección entre interleavings concurrentes, respuestas de red o disponibilidad de recursos.

Dos ejecuciones con la misma petición pueden ser legítimamente distintas si una obtiene conflict porque otra transición confirmó primero. Eso no autoriza resultados arbitrarios: el conjunto de salidas y sus condiciones debe estar especificado. Un contrato profesional dice, por ejemplo, «ante una versión distinta, no modifica el estado y devuelve conflict», no «a veces gana».

La seguridad se degrada cuando un efecto nondeterminista se presenta como confirmado. Un timeout de charge puede significar «no llegó», «llegó y se procesó» o «llegó dos veces». La idempotency key reduce duplicados sólo si el receptor conserva y aplica una relación única entre clave, operación y resultado. No convierte una red incierta en determinista ni resuelve una autorización ausente.

La concurrencia añade una dimensión de orden. Si dos transiciones leen la misma versión, el control de compare-and-swap o una garantía equivalente puede aceptar una y rechazar la otra. Si el contrato no fija el orden, un auditor debe marcar el estado como no adjudicado. No hay que invadir el capítulo 51 para decidir esta propiedad: basta razonar sobre estados antes y después, y declarar que el mecanismo de memoria o scheduler será tratado allí.

Nondeterminismo y trazas reproducibles

Una traza es una secuencia ordenada de eventos de ejecución y observación: lectura, decisión, escritura, envío, respuesta y fallo. Dos trazas pueden partir del mismo estado y divergir por orden de mensajes, reloj, elección de réplica o respuesta de dependencia. El análisis no pretende inventar un orden total donde sólo existe un orden parcial; registra relaciones causales y los eventos concurrentes.

Para reproducir una decisión se conservan versión de la policy, identificador del principal no sensible, versión de datos, request_id, clave de idempotencia, timestamps con zona, resultado y razón. No se almacenan tokens, claves ni payloads secretos sólo para facilitar el debugging. Un hash puede ayudar a correlacionar si se documentan colisiones, retención y límites de inferencia. Los logs son evidencia de lo que el sistema registró, no una prueba independiente de que su reloj o instrumentación fueran correctos.

Un diagnóstico serio construye primero la traza observada y después las hipótesis. Hipótesis H1: dos workers aceptaron la misma versión. H2: sólo uno aceptó y el segundo reintentó tras timeout. H3: ambos aceptaron localmente pero un downstream duplicó el efecto. Cada hipótesis debe tener una predicción comprobable —versiones, claves, respuestas y estado downstream— y un control negativo. Si faltan datos, se conserva unknown; no se elige la narración más conveniente.

Efectos y fronteras de confianza

Un efecto es una modificación observable fuera del cálculo local: escribir una base de datos, emitir un evento, cambiar una política, enviar un correo o revelar un dato. Separar S' de E permite detectar una falsa equivalencia frecuente: «la base confirmó» no significa «el consumidor aplicó el evento».

En una frontera de confianza, la entrada debe validarse por estructura, rango y significado antes de cambiar estado. CWE-20 describe el riesgo de aceptar datos no validados; el modelo de transición añade la pregunta «¿qué estado quedó comprometido y qué efecto se disparó?». Una validación de esquema no concede autorización. El principal, la acción, el recurso y el estado aplicable deben permanecer ligados durante toda la transición.

Caso negativo: tenant llega en el cuerpo y el servicio obtiene principal de una sesión válida. Si el código usa el tenant solicitado sin comprobar que el principal puede actuar sobre él, la transición puede ser determinista y aun así insegura. El defecto no es nondeterminismo: es una precondición de autoridad ausente.

Otro caso: un worker consume dos veces el mismo mensaje. Si el estado sólo registra «procesado» después del efecto externo, un fallo intermedio puede duplicar el efecto. La solución no es afirmar que la cola es exactamente una vez; el contrato debe escoger deduplicación, transacción coordinada, compensación o estado unknown, y documentar el límite.

Figura 49-03 · ¿Qué evita que dos transiciones confirmen el mismo estado?

Vista adaptada. Toca el diagrama para ampliarlo.

Dos intentos simétricos compiten en un punto de serialización: uno confirma la nueva versión y el otro observa conflicto.

Efectos: outbox, sagas e idempotencia con límites

El patrón outbox guarda el cambio de dominio y un registro de evento en el mismo ámbito transaccional; un publicador posterior lee ese registro y entrega el evento. Su ventaja es relacionar persistencia local y publicación pendiente. No garantiza que el consumidor aplique el evento, ni que nunca haya redelivery. Por eso el consumidor necesita deduplicar o procesar de forma idempotente, y la evidencia debe distinguir outbox_written, published y consumed.

Una saga descompone una operación larga en transiciones locales y define acciones compensatorias para estados intermedios. Compensar no equivale a deshacer físicamente: un correo enviado no puede retirarse de la bandeja, y un cargo que ya llegó al banco puede requerir un reembolso separado. La saga debe enumerar qué efectos son reversibles, cuáles son sólo mitigables y qué ocurre si la compensación falla. Un estado cancel_requested puede ser más exacto que cancelled.

La idempotencia significa que repetir una solicitud bajo una clave y contexto definidos no añade un efecto nuevo más allá del resultado ya registrado. La clave debe estar ligada al principal, recurso, operación y ventana apropiados; si sólo se usa un texto global, un actor puede adivinarla o reutilizar el resultado de otro tenant. Tampoco toda operación es idempotente por repetir el mismo payload: una transferencia necesita identidad de operación, control de versión y un receptor que conserve la deduplicación. Los límites —retención, failover, restauración y cambio de región— deben formar parte del contrato.

Caso negativo: el outbox confirma event_id=E7, pero el consumidor cae después de ejecutar el cargo y antes de marcar E7 procesado. El redelivery es esperado. Si el consumidor no conserva una clave única o una consulta al procesador, puede cobrar dos veces. La corrección no es borrar el segundo mensaje: requiere que el efecto downstream acepte una clave idempotente, o una reconciliación que compare el estado del cargo antes de repetirlo.

Caso profesional: reserva, cobro y notificación de extremo a extremo

Supongamos que una plataforma recibe POST /orders/{id}/reserve-and-charge. La petición incluye cantidad, tenant y una clave de idempotencia; la sesión aporta el principal. El contrato exige que sólo el tenant autorizado pueda reservar, que el inventario no resulte negativo, que el cobro no se duplique y que una notificación pueda retrasarse sin convertir una reserva parcial en éxito completo.

El estado abstracto contiene stock, reservation_status, charge_status, notification_status y las versiones de cada agregado. La representación son filas y un outbox. La precondición liga principal y tenant, exige cantidad positiva, versión vigente y una clave de operación no usada por otro recurso. La primera transición escribe reserva y evento ReservationCreated en una unidad atómica local. Su salida es accepted_pending_charge, no success, porque el cobro todavía es efecto de otra transición.

El worker de cobro consume el evento. Comprueba que la reserva pertenece al tenant y que su estado es cobrable; llama al proveedor con una clave derivada de order_id + operation_id. Si recibe confirmación, escribe charge_status=paid y publica ChargeCompleted. Si recibe timeout, consulta el estado con la misma clave o marca charge_status=unknown; nunca asume declined ni vuelve a cobrar con una clave nueva sin adjudicar la primera. Si el proveedor confirma rechazo, el worker puede ejecutar una compensación de reserva según policy, dejando trazabilidad de released o release_pending.

El notificador consume ChargeCompleted. Su entrega es un efecto externo no reversible. El estado correcto distingue notification_pending, sent y unknown; un timeout del correo no autoriza un segundo envío sin una política de deduplicación. La API puede devolver al cliente el estado agregado consultando estas fases, y debe distinguir accepted_pending_charge, paid_notification_pending, completed, rejected y review. El cliente no debe interpretar cualquier código 2xx como dinero cobrado.

Los invariantes locales son stock no negativo, una única reserva por operation_id y una sola transición de charge_status desde pending a paid o declined. Los globales son «no se cobra una operación no autorizada» y «cada cargo confirmado corresponde a una reserva autorizada». La segunda exige correlación entre los dos dominios; una mera firma de evento no demuestra que la policy actual siga permitiendo la operación.

Durante un incidente, la traza puede mostrar dos requests con la misma clave, una escritura de outbox y dos entregas al worker. La adjudicación busca el registro de idempotencia del proveedor, la versión de reserva, el estado del cargo y el evento de compensación. Si el proveedor carece de consulta fiable, el resultado es review, no un segundo cargo. El informe separa impacto observado (un cargo confirmado), impacto potencial (duplicación si se reintenta con clave distinta) y control pendiente (confirmar estado remoto).

Método de verificación y diagnóstico

La verificación empieza por el contrato y sus invariantes, no por los logs que casualmente existen. Construye casos válidos, límites y fallos: cantidad cero, tenant cruzado, versión obsoleta, retry idéntico, retry con clave distinta, caída antes y después de cada escritura, duplicación del evento y dependencia que responde tarde. Para cada caso, anota el estado inicial, la traza esperada, la salida y la ausencia de efectos prohibidos.

Después prueba refinamiento: ¿cada representación concreta corresponde a un estado abstracto válido? ¿Puede una caché devolver un estado que el contrato de autorización no permite usar? ¿La restauración mantiene la unicidad de claves? Las pruebas de propiedad son útiles para invariantes, mientras las pruebas de integración verifican fronteras reales. Un mock que siempre confirma al proveedor no prueba el comportamiento ante timeout o redelivery.

El diagnóstico operativo clasifica evidencia en observada, derivada y faltante. Observada: versión persistida o respuesta firmada por el receptor. Derivada: correlación de dos registros con el mismo request ID. Faltante: aplicación downstream cuando sólo se vio publicación. Esta disciplina evita que una afirmación de «exactly once» nazca de una cola sin duplicados en una prueba pequeña. El resultado final debe incluir precondiciones, alcance temporal, actores, ventanas de caché, efectos residuales y condición concreta para pasar de unknown a confirmed.

Método de adjudicación y transferencia

Para analizar una operación nueva, escribe primero el estado mínimo y los actores que pueden modificarlo. Después formula un invariante positivo y uno negativo; define precondiciones verificables; separa postcondiciones locales de efectos externos; y enumera fallos entre cada efecto. Finalmente clasifica cada resultado como confirmado, rechazado, pendiente o desconocido.

El método funciona para un cambio de contraseña, un despliegue o un registro de auditoría, pero no infiere garantías que no estén en el contrato. Una figura de estado puede revelar una transición que la prosa oculta: dónde se bifurca el rechazo, qué flecha cruza una frontera y qué camino deja unknown. No debe confundirse una flecha de dependencia con una flecha de ejecución.

La síntesis es limitada: un programa es una transformación de estado y datos bajo condiciones, no una función matemática aislada ni una caja negra autorizada a decidir por el sistema. El análisis profesional pregunta qué estado se conserva, qué entrada puede influir, qué salida se observa, qué efecto se confirma y qué incertidumbre permanece. Tipos, memoria, control de flujo y parsing concretan otras partes de esa transformación; sus mecanismos se desarrollan en los capítulos siguientes.

Fuentes primarias