Teorema de seguridad
DG trata las especificaciones, la evidencia, los comandos, los bytes almacenados, la salida del proveedor, la entrada del operador, los artefactos generados y los testigos de autoridad externa como hostiles en sus límites de propiedad.
hostile source material
-> source-specific acquisition witness
-> admitted evidence
-> condition-use-policy witness
-> pure semantic candidate
-> exact-head accepted successor or rejection
-> dispatch eligibility only after acceptance
El fallo de adquisición operacional no acuña ningún candidato semántico. Un candidato obsoleto no cambia ningún estado aceptado. Una intención aceptada no es un efecto externo realizado. La autoridad de implementación se importa a través de testigos exactos y nunca se infiere de espacio de nombres, ruta, caché o configuración local.
Activos protegidos
- Leyes, gráficos, condiciones, políticas e identidades de escenario canónicas.
- Testigos de adquisición, admisión, política de uso, progreso, preparación y finalización.
- Valores de evidencia, referencias, procedencia, alcance, tiempo, sensibilidad y metadatos de retención.
- Encabezados de ejecución aceptada, historial inmutable, recibos de idempotencia, intenciones de evidencia de gobernanza y registros de despacho.
- Autenticación, autorización, atribución, contrato de proveedor y hechos de admisión de despliegue externo.
- Runpacks, informes de verificación, registros de auditoría, credenciales y claves de firma.
- Registros de capacidad, autoridad, decisión, prueba y liberación.
Adversarios
Suponga llamadores maliciosos o comprometidos, autores de escenarios, fuentes de evidencia, proveedores, almacenamiento, sumideros de despacho, operadores, complementos, proxies, CI, SDKs y poblaciones de nodos calificados. Suponga reproducción, reordenamiento, duplicación, omisión, equívoco, lecturas obsoletas, retroceso, procedencia falsificada, confusión de esquema, diputado confundido, fallo parcial, recorrido de ruta, carreras de symlink, SSRF, inyección de subprocesos, agotamiento de recursos y divulgación de credenciales.
Un host/kernel comprometido está fuera de la capacidad del proceso para neutralizar, pero su autoridad, material retenido y radio de explosión permanecen explícitos.
Mapa de límites
| Frontera | Único propietario de admisión | Resultado permanente |
|---|---|---|
| Sintaxis de escenario | constructor de ley de escenario | ValidatedScenarioLaw |
| Sintaxis y refinamientos de RET | RET | requisito validado/satisfacible/monótono |
| Topología de dependencia | Xarxa | identidad de gráfico, progreso, preparación, delta de finalización |
| Evidencia del llamador | constructor de fuente de llamador | testigo de adquisición del llamador |
| Evidencia de tiempo/env/documento | constructores de fuente local | testigo de adquisición específico de fuente |
| Uso de evidencia | evaluador de política de condición | testigo de satisfacción de política y instantánea canónica |
| Aceptación de candidatos | autoridad de ejecución aceptada | revisión aceptada o rechazo cerrado |
| Bytes de almacenamiento | rehidratación de almacenamiento local | valores aceptados reconstruidos o rechazo |
| Exportación de auditoría aceptada | backend de ejecución aceptada seleccionada | punto de control exacto de cabeza aceptada más páginas de punto de control acotadas |
| Bytes de ejecución | constructores de runpack-v6 | identidades exactas de manifiesto/objeto/árbol o rechazo tipado |
| Evaluación de RET | requisito/plan validado y ejecutor acotado | resultado semántico o fallo operativo tipado |
fuente de corredor file:// | AdmittedFileRoot explícito | capacidad de directorio retenida o denegación tipada |
| Publicación de runpack local | repositorio enraizado en capacidades | resultado exacto de objeto/manifiesto nuevo creado |
| Material de verificación | constructor de material suministrado | conjunto de material local/agrupado acotado sin autoridad de resolutor |
| Reclamaciones de verificación | registro de reclamaciones cerrado y verificador independiente | informe total verificado por dependencia |
| Ejecución de intención | autoridad de despacho | resultado exacto de diario/recibo |
| Hechos de autenticación y despliegue | adaptadores de autoridad externa/embebida | testigo exacto de admisión de operación |
Amenazas de escenario y gráfico
| Amenaza | Control requerido |
|---|---|
| Gráfico o testigo falsificado | Construcción sellada; bytes hostiles se reconstruyen a través de constructores. |
| Sustitución de gráfico/ley | Cada progreso, frontera, delta, ejecución, registro y empaquetado de ejecución vincula la identidad exacta de gráfico/ley. |
| Topología colgante, auto, cíclica, duplicada, no monótona o agotada | Xarxa/RET rechaza antes de acuñar ley validada. |
| Regresión de progreso o gráfico incorrecto | El progreso vinculado al gráfico y el delta de finalización comparan identidad e inclusión monótona. |
| Apertura/completación duplicada | Ciclo de vida sellado más idempotencia/conflicto de ejecución aceptada. |
| Fan-out implícito, selección de rama o cancelación | La frontera es solo descriptiva; el operador abre explícitamente una etapa. |
| Apertura de etapa interpretada como asignación | La atribución permanece fuera de la propiedad de gráfico/etapa; la coordinación es externa. |
| Hoja estructural interpretada como éxito | Solo ley de finalización de escenario explícita. |
| Ejecución recursiva oculta | La evaluación nunca comienza/evalúa otro escenario. |
| Hecho de ejecución externa obsoleto | La evidencia vincula la ley/external-run/cabeza exacta y la política de actualidad. |
Amenazas a la representación y la identidad
| Amenaza | Control requerido |
|---|---|
| Identidad inválida construida por API o deserialización | Almacenamiento de dominio privado, transportista hostil privado, constructor falible y Serde mediado por constructor. |
| Normalización o aliasing de identificador | Gramática ASCII sensible a mayúsculas exacta; sin recortes, plegado de Unicode, plegado de mayúsculas o coerción para identificadores DG creados. |
| Sustitución de identidad nominal | Tipos de dominio Rust distintos; sin identificador de cadena genérico o conversión no verificada. |
| Deriva de token de vocabulario cerrado | Una tabla total de variantes/tokens generada posee análisis, visualización, Serde, OpenAPI y JSON Schema. |
| Campos sobrantes introducidos en un estado de suma cerrada sin campos | Los estados sin campos etiquetados internamente utilizan variantes exactas de objeto vacío más evidencia de rechazo de cable hostil; las variantes de unidad de Serde no son admitidas para sumas de objetos cerrados. |
| Procedencia de solicitud solo del llamador | El constructor de procedencia compartida devuelve un error tipado a menos que esté presente una identidad de solicitud emitida por el servidor. |
| Identidad de solicitud del llamador tratada como autoridad o idempotencia | La procedencia de transporte sigue siendo no autoritativa y nominalmente separada de la identidad de operación semántica. |
| Ambigüedad de ancho/codificación de resumen | Bytes SHA-256 fijos internamente y proyección de cable exacta de 64 caracteres en minúsculas. |
| Sustitución de resumen de sujeto cruzado | Identidad de sujeto nominal más separador de dominio fijo y revisión de formato; los resúmenes de contenido genéricos no pueden ingresar a consumidores de identidad de ley de escenario. |
| Formato antiguo aceptado a través de un alias o migración | dag-v2 y versiones anteriores, runpack v5 y versiones anteriores, y cada esquema de SQLite que no sea 12 se rechazan como entradas hostiles no soportadas. |
PF-04 cierra la ejecución, intento, apertura, presentación, intención, registro aceptado/cabeza y identidades de idempotencia de propiedad del protocolo a través de tipos mediados por constructores nominales. Las proyecciones almacenadas o de ejecución permanecen hostiles y se reconstruyen a través de esos constructores.
Amenazas de condición y evidencia
Confusión de categoría y autoridad
La implementación debe prevenir:
- canal de adquisición interpretado como autoridad de fuente o rango de confianza;
- localizador/referencia interpretado como un canal de adquisición;
- atestación interpretada como verdad universal o transporte;
- identidad de condición fusionada por texto de consulta de proveedor igual;
- proveedor/query tratado como semántica de condición inherente;
- estado, confianza, procedencia, ausencia o resultado de comparador proporcionados por el llamador;
- la evidencia faltante se interpreta como ausencia observada;
- error del proveedor almacenado como evidencia semántica;
- violación de contrato reclasificada como
Unknownsemántico.
Solo los hechos factorizados más una política de uso de condición exacta autorizan el uso.
Presentación del llamador
Las amenazas incluyen falsificación de identidad del llamador, material sobredimensionado, sustitución entre ejecuciones/condiciones, tiempo de procedencia u observación auto-asignado, inflación de reintentos de un quórum de origen, afirmaciones obsoletas y retención excesiva de datos sensibles. La admisión vincula el contexto de autoridad autenticada o embebida, la procedencia de solicitud revisada, la autoridad de perfil/principal estable, contenido exacto, límites, alcance objetivo, tiempo de recibo de propiedad de límite y política de divulgación/retención. Las identidades de solicitud nunca definen la independencia de origen. Las reclamaciones del llamador permanecen distinguibles de los hechos verificados.
Tiempo
Las lecturas del reloj ambiental pueden hacer que la reproducción sea no determinista o permitir la falsificación de frescura. La evaluación recibe un contexto de tiempo explícito. El tiempo utilizado como evidencia proviene de una autoridad nombrada y vincula intervalo, resolución, incertidumbre y dominio de reloj. La falla nunca fabrica una marca de tiempo.
Entorno
Las amenazas incluyen filtración de secretos, lecturas mutables, acceso a claves no configuradas, agotamiento de codificación/tamaño y falsa ausencia. El perfil inicial utiliza claves validadas en la lista blanca y una instantánea de inicio inmutable por defecto. Cada observación vincula la identidad de la instantánea, la clave, un resultado explícito presente-o-observado-ausente, sensibilidad y divulgación/conservación. Las codificaciones opcionales/nulas no pueden acuñar ausencia, y una reclamación de instantánea hostil incompleta no puede sustentar ninguna forma de contenido.
JSON/YAML enraizado
Las amenazas incluyen recorrido de padre, ruta absoluta, carrera de symlink, escape de raíz, acceso a dispositivo/FIFO/socket, reemplazo después de la verificación, archivos de gran tamaño, árboles profundos o anchos, amplificación de alias/etiqueta YAML, claves duplicadas, documentos en blanco, inclusiones de red, análisis parcial y falsa ausencia.
Los controles requieren raíces registradas, rutas relativas validadas, contención canónica, objetos abiertos regulares, un resumen de bytes abierto exacto, un análisis completo acotado, políticas de duplicados/espacios en blanco, sin escape de red/inclusión, y un análisis completo antes de la ausencia. Los constructores de testigos de tiempo nombrado, entorno y documento comparten el límite de privacidad del crate central con la construcción de evidencia sellada; un crate de Rust separado no puede llamar a esos constructores para auto-mintar un hecho de fuente local.
Instantánea y política
La identidad de evidencia duplicada, la dependencia del orden de llegada, la fabricación de cuórum cero, la evaluación incompleta del candidato, la reutilización cruzada de objetivos sin un testigo, la revocación obsoleta y la inflación de linaje Sybil fallan en cerrarse. Una instantánea canónica y una evaluación total de la política de uso poseen el resultado.
Amenazas de capacidad excluida
La antigua red, MCP remoto, subproceso y linaje de tiempo de ejecución de proveedor ejecutable están ausentes de la implementación inicial. Si alguna familia excluida se reintroduce, permanece no soportada e inalcanzable desde todas las configuraciones y rutas de herramientas soportadas hasta que su pista independiente PF-08 se cierre.
Adquisición de red
Las amenazas incluyen SSRF, reencuadre de DNS, redirecciones, acceso privado/local de enlace, exfiltración de credenciales, confusión de proxy, contrabando de respuestas, cuerpos no limitados, tormentas de reintentos, DNS/política obsoleta, deriva de contrato y equívoco de fuente remota. DG-DECISION-NETWORK-ACQUISITION-001 debe aprobar la ley del testigo de origen, autoridad de egreso/credenciales, límites y calificación antes de brindar soporte.
Subproceso y ejecución arbitraria
Las amenazas incluyen inyección de comandos/argumentos, reemplazo ejecutable, secretos/entorno heredados, confusión de directorio de trabajo, procesos huérfanos, falsificación de salida, escape de recursos y compromiso del host. El DG inicial no carga ningún código de proveedor nativo arbitrario y no admite adquisición de MCP stdio/subproceso. La ejecución futura prefiere un proceso aislado, WASM o protocolo remoto versionado con manifiesto firmado, capacidades, presupuestos de recursos/red, validación de salida hostil y calificación.
Evaluación remota
Los bytes de propuesta sellada con apariencia de sellado no prueban la evaluación. Un trabajador remoto puede reclamar cada etapa pasada. Los perfiles iniciales co-localizan evaluación y compromiso. La verificación de prueba remota o la ejecución atestiguada requieren un perfil independiente; la atestiguación prueba solo su reclamación de ejecución medida exacta, no la verdad del mundo o la corrección matemática.
Amenazas de ejecución aceptada
| Amenaza | Propiedad de protocolo requerida |
|---|---|
| El llamador elige una identidad de ejecución reutilizada | DG emite un RunId opaco no reutilizable a partir de una solicitud de creación idempotente. |
| Misma solicitud, contenido diferente | Conflicto de idempotencia tipado. |
| Repetición de la misma solicitud | Resultado original exacto; sin intento o intención duplicada. |
| Dos candidatos compiten desde una cabeza | Como máximo un sucesor directo; el perdedor es obsoleto y no cambia nada. |
| Respuesta perdida después de la aceptación | Resolver mediante identidad de operación estable. |
| Fallo antes/después de la transacción | El backend refina el modelo aprobado y preserva el comportamiento de atomicidad/recibo. |
| Cabeza forjada | Validación hostil; sin mutación de estado. |
| Desacuerdo de cabeza/historia almacenada | Fallo de integridad, cuarentena/recuperación; nunca reparación local por conjetura. |
| Confusión de autorización/atribución | El adaptador deriva testigos exactos; la solicitud semántica no puede auto-seleccionar principal/agente. |
| La búsqueda de recibos ocurre después de una comparación obsoleta | La búsqueda de recibos aceptados es primero; una cabeza posterior no puede ocultar un resultado aceptado. |
| Eliminación de recibo aceptado o tumba de RunId | Autoridades indexadas permanentes; la compactación requiere prueba de dependencia y no puede debilitar la repetición/no reutilización. |
| Compromiso de estado/historia/recibo/cabeza/intención dividida | Un solo par aceptado atómico o un tartamudeo autoritativo completo. |
| La mutación aceptada carece de evidencia de gobernanza | El par aceptado atómico lleva una identidad sellada de GovernanceEvidenceIntent y devuelve CommittedWithGovernanceIntent. |
| Resultado de auditoría o uso es descartado | Cada sumidero de autoridad devuelve un recibo estable o un fallo tipado; los sumideros no duraderos rechazan, y el fallo primario más el de gobernanza permanecen como un compuesto. |
| Resultado falso conocido-no aceptado después de un posible compromiso | Unavailable requiere prueba de no aceptación; la ambigüedad es Indeterminate. |
| El llamador o el reloj ambiental suministran el tiempo de compromiso | La autoridad de tiempo inyectada nombrada emite un testigo tipado antes del compromiso; la revisión por sí sola ordena la historia. |
| La repetición vuelve a muestrear el tiempo de aceptación | El recibo aceptado devuelve el testigo de tiempo original. |
| Bypass de cuarentena de integridad | La cuarentena bloquea cada aceptación posterior para la autoridad afectada. |
| Probing de recibos no autorizados/divulgación de resultados | La autorización precede la búsqueda de recibos y gobierna la divulgación exacta de resultados. |
| Probing de creación-recibo entre namespaces | La resolución de creación vincula el namespace autorizado antes de la búsqueda de recibos; un recibo extranjero es indistinguible de la ausencia delimitada. |
| Identidad de operación semántica utilizada bajo una familia de operación diferente | Las familias de operación nominal permanecen distintas; los resultados abstractos y los recibos aceptados satisfacen la invariante de familia-escopo verificada. |
| Construcción directa de material de admisión reclamado | El testigo de admisión de ejecución aceptada tiene estado privado, sin deserializador en bruto, constructores de límite explícitos y proyección de persistencia de solo lectura. |
| Cambios de codificación específicos del backend limitan la admisión | Los límites semánticos canónicos de propiedad central son idénticos para memoria y SQLite; el sobrecosto del sobre de persistencia tiene un techo inmutable separado. |
| Agotamiento del almacenamiento de recibos/tumbas | Los límites inmutables nombrados y los fallos de capacidad fallan conocidos-no aceptados antes del compromiso; los hechos semánticos no son expulsados silenciosamente. |
| Retroceso coherente de una base de datos local completa | Ancla externa explícita no reclamada; los auto-hashes locales no fabrican resistencia al retroceso. |
VIEW formal o restricción oculta un sucesor que viola | Las configuraciones autoritativas rechazan VIEW, SYMMETRY y restricciones de estado; las huellas dactilares de TLC completan el estado del modelo. |
| Coordenadas de herramienta no aprobadas alcanzan descarga o ejecución | Bootstrap valida el cierre completo aprobado antes del uso de red o Java, luego permite solo namespaces de liberación upstream exactos y artefactos fijados por digest. |
| La acción modelada no tiene rastro de refinamiento PF-04 | El esquema de trazas, el mapa de acciones y los vocabularios del corpus observado deben ser exactamente iguales; una transición incorrecta independiente debe hacer fallar el oráculo TLA. |
PF-03 cierra la decisión de propiedad/modelo abstracto con evidencia TLC acotada, contraejemplos de mutación esperados y trazas deterministas de PF-04. PF-04 implementa la relación y reproduce dieciséis trazas genéricas de protocolo contra memoria y SQLite más dos trazas de reinicio duraderas contra SQLite. La memoria tiene evidencia de reinicio negativa explícita. Este refinamiento local no establece propiedad distribuida, resistencia a retrocesos externos o recuperación de despacho.
Amenazas de despacho
El modelo de candidato PF-06A trata estos como casos adversariales explícitos:
| Amenaza | Límite de control/reclamación permanente |
|---|---|
| Despacho de una intención no aceptada | Solo una mutación de propiedad aceptada puede entrar en elegibilidad. |
| Sustitución de objetivo, ejecutor, autorización o perfil de recuperación | Se retiene un vínculo inmutable de un solo objetivo en cada registro de diario. |
| Cabeza de diario falsificada, intento o finalización ABA | Las identidades exactas de cabezas y de intentos nunca reutilizados hacen que las acciones obsoletas titubeen. |
| Un trabajador completa la reserva activa de otro trabajador | El diario vincula las identidades de trabajador e intentos nunca reutilizados; los registros de progreso deben presentar el par exacto. |
| Recibo falsificado, efecto cruzado o conflicto | Autoridad de recibo calificada y vínculo exacto de efecto/clave; cuarentenas de conflicto. |
| El diario se acuña a sí mismo como recibo o calificación de testigo | Las acciones del diario consumen hechos de calificación pre-admitidos exactos; almacenar un identificador no puede crear autoridad de origen. |
| La identidad del recibo se reutiliza | La propiedad del recibo es funcional y la reutilización de la identidad a través de hechos de diario aceptados falla en cerrado. |
| Un resultado de consulta autorizada se sustituye por un recibo de efecto | Consulta realizada, consulta no realizada y material de recibo estable son familias de testigos tipadas distintas con propietarios exactos. |
| El resolvedor informa falsamente que se realizó o no se realizó | PF-06A verifica solo la relación de calificación importada exacta y lleva el testigo; el verificador externo sigue siendo una premisa nombrada que requiere calificación PF-06C. |
| Reclamación falsa de pre-efecto o no ocurrencia | Se requiere un testigo nombrado exacto; la ambigüedad post-límite permanece indeterminada, y un fallo pre-límite posterior no puede borrar la deuda de ocurrencia no resuelta anterior. |
| Testigo de no ocurrencia reutilizado o sin nombre | Las identidades de testigos de pre-efecto, consulta autorizada y caducidad/actualidad se retienen, tipadas por familia, de un solo propietario y nunca reutilizadas. |
NoResolver se confunde con “no puede tener éxito” | Los recibos de éxito en vivo calificados son independientes de la resolución de ambigüedad posterior; todos los perfiles pueden registrar éxito sincrónico testificado, pero solo los resolvedores calificados pueden cerrar la ambigüedad automáticamente. |
| Reintento inseguro o cambio de vínculo de invocación | El reintento requiere el perfil de clave exacta calificada y preserva la identidad lógica, objetivo, contenido, revisión de ejecutor, vínculo de autorización, perfil de recuperación y clave de idempotencia. |
| Efecto lógico duplicado después de la pérdida de respuesta | El recuento de invocaciones de DG, el recuento de ejecución física externa y una ocurrencia lógica son separados; la idempotencia de clave exacta limita la ejecución física solo para un perfil de ejecutor calificado. |
| La invocación de límite se trata como prueba de ocurrencia | El recuento de invocaciones y la ocurrencia externa son independientes; realizado implica invocación, pero la invocación puede permanecer no realizada hasta que un resolvedor calificado cierre el conocimiento. |
El fallo olvida Started, recibo o estado terminal | El perfil duradero preserva el conocimiento del diario; la memoria explícitamente no hace ninguna reclamación de reinicio. |
| Fallo después del compromiso de intención de dominio/gobernanza pero antes de la primera adición de sumidero | La tupla de dominio y de intención de gobernanza comprometida es monótona y la reconciliación de reinicio se reanuda desde la intención retenida. |
| Reconocimiento de gobernanza antes de la adición duradera | El reconocimiento requiere un recibo estable exacto después del compromiso de sumidero duradero. |
| Sustitución de identidad/carga de gobernanza | Registros de gobernanza de clave independiente y relación de redelivery exacta. |
| Tupla de intención de dominio/gobernanza importada incompleta | PF-06A requiere la tupla PF-04 monótona completa y no reclama falsamente volver a probar el compromiso atómico de PF-04. |
| La compensación se admite a partir de la verdad de ocurrencia oculta o borra la historia original | La compensación requiere un estado realizado conocido por DG y es un efecto vinculado completamente separado con un diario independiente. |
| Perfil de compensación no calificado | La creación de compensación requiere el perfil de familia de efecto admitido exacto además del rendimiento conocido por DG. |
| Bypass de cuarentena o mutación de propietario/índice de efecto cruzado | La cuarentena es monótona; los índices de propiedad de efecto y las proyecciones de diario/versiones están de acuerdo; los efectos registrados de forma independiente no se mutan entre sí. |
| Se asume implícitamente un progreso justo o durabilidad de memoria | Registro de suposiciones nombradas más modelos de contraejecución de no equidad y durabilidad de memoria falsa; ninguna de las reclamaciones sigue de la seguridad. |
| Sondeo no autorizado de recibo/estado | PF-06B debe autorizar antes de la divulgación; PF-06A no modela los internos de autenticación. |
| Retroceso coherente del diario de despacho | No reclamación de anclaje externo; los auto-hashes locales no pueden probar frescura. |
DG-DECISION-DISPATCH-MODEL-001 permanece abierto. El candidato v5 es InvalidatedForApproval; su informe acotado es evidencia de regresión histórica, no un sujeto de aprobación. Aún no existe un tiempo de ejecución de diario/recuperación permanente. La intención aceptada, un bloqueo local, la satisfacción del modelo acotado y la invocación como máximo una vez no son un efecto externo exactamente una vez.
Amenazas de frontera de garantía formal
| Amenaza | Límite de control/reclamación permanente |
|---|---|
| Una propiedad de estado alcanzable está mal etiquetada como inductiva | TLAPS debe descargar obligaciones exactas de inicialización, preservación e implicación; la alcanzabilidad de TLC por sí sola no puede acuñar InductivelyProved. |
| Refinamiento está mal etiquetado como inducción | Las filas de prueba de modelo a modelo informan RefinementSatisfied; la correspondencia de producción sigue siendo una reclamación separada de propiedad del protocolo. |
| Un modelo vacío/no alcanzable produce una propiedad verde | El estado inicial, acción, rama y no vacuidad del antecedente requieren cobertura más oráculos de alcanzabilidad de contraejemplo esperados. |
| La matriz de límites se describe pero no se ejecuta | Cada fila de perfil compilado produce un acuerdo positivo exacto o una ejecución de desacuerdo testificada. |
| El denominador de mutación omite una guardia o escritura autorizada | Cada conjunción de máquina de estados registrada tiene un punto de mutación exacto y cada propiedad posee al menos un operador de eliminación. |
| La ambigüedad del analizador admite suposiciones ocultas o cocientes | Filas de suposición de propiedad exacta del módulo; sintaxis de configuración cerrada; rechazo insensible a la indentación de VIEW, SYMMETRY, restricciones, sobreescrituras y modos de inicialización dual. |
| La proposición de prueba es reemplazada mientras los tokens de táctica parecen válidos | La propiedad exacta de la proposición canónica rechaza comentarios, LET, filas de teoremas desconocidos y hojas no probadas/omitidas. |
| Ambos caminos semánticos comparten el mismo error de transición | Comparación exhaustiva de relación finita TLA/Python, separación explícita de gráfico de importación y detección deliberada de desacuerdo; la independencia de autoría sigue siendo una no reclamación de revisión humana. |
| El checkout mutable cambia después de la admisión | Cada herramienta ejecuta un snapshot de fuente verificado por digest externo inmutable y el denominador de fuente en vivo se vuelve a verificar después de la ejecución. |
| La instalación de herramientas o evidencia es sustituida | Archivos/instaladores oficiales, manifiestos, recibos de instalación, árboles de tiempo de ejecución e informes son separados por digestión. |
| El árbol TLAPS no determinista se llama falsamente reproducible | El sujeto candidato vincula la política de instalador oficial fijada; cada informe de ejecución vincula su árbol instalado exacto; la reproducibilidad del árbol instalado en bruto es una no reclamación explícita. |
| La calificación sintética se interpreta como prueba del protocolo DG | El límite de reclamación candidato y la identidad del protocolo son verificados por máquina; el re-cierre de PF-03 y un sucesor PF-06A siguen siendo aprobaciones separadas. |
El candidato de fundación compartida actual satisface su denominador sintético registrado pero espera aprobación humana explícita. No cambia la capacidad de tiempo de ejecución de producción y no autoriza ninguna reclamación de protocolo PF-03 o PF-06A.
Amenazas de almacenamiento y reproducción
Todos los bytes almacenados/ejecutados son hostiles. Los controles incluyen rechazo de versiones, decodificación limitada antes de la asignación, aritmética verificada, rechazo de duplicados/bytes finales, reconstrucción mediada por constructor, recomputación de identidad canónica, verificaciones exactas de cabeza/historia y dependencias de retención explícitas.
Los antiguos formatos previos al lanzamiento rechazan sin migración. Un digest prueba solo su relación de integridad nombrada, no la autenticidad de origen, la autoridad de cabeza actual, la protección contra retrocesos o el enlace externo. La reconsulta en vivo es nueva evidencia. Los informes de repetición indican exactamente qué adquisición original, esquema, autorización, frescura y relaciones de política pueden ser reconstruidas.
PF-05 asume además árboles de manifiesto/objetos hostiles, bytes suplementarios suministrados de forma hostil, contenidos de repositorio local comprometidos, ordenación/rangos de registros maliciosos, bombas de descomposición, carreras de publicación, sustitución de rutas/símbolos, confusión de dependencia de reclamaciones y agotamiento de recursos del verificador. Los controles son doce raíces de familia obligatorias, identidades de ancho fijo separadas nominalmente por dominio, objetos acotados canónicos, verificaciones de rango/salida/profundidad, aritmética verificada, páginas limitadas por puntos de control, un reductor independiente, un DAG de reclamaciones cerrado, presupuestos de trabajo deterministas, objetivos de sistema de archivos relativos a capacidades, publicación de nuevos objetos, comparación exacta de bytes retenidos y visibilidad de manifiesto final.
El verificador resuelve solo material local empaquetado o explícitamente suministrado. No tiene autoridad de red, proveedor, reloj, SQLite, MCP, ruta ambiental o resolutor genérico. Un localizador nunca satisface la disponibilidad de material. Los bytes suplementarios externos en bruto solo pueden satisfacer relaciones de resumen/estructura; no pueden acuñar autenticidad de fuente, actualidad, resistencia a retrocesos, despacho, implementación o reclamaciones de procedencia de construcción.
Amenazas de despliegue
El espacio de nombres, la ruta, la caché, la identidad del nodo, la etiqueta de región o la configuración no prueban la asignación de servicio, la autorización, la capacidad, la residencia, la autoridad de clave o la calificación del evaluador. Los adaptadores de perfil consumen testigos externos exactos con sujeto, revisión de autoridad, alcance, actualidad y operación.
Las rutas de escala iniciales ejecutan distintas ejecuciones hacia nodos de evaluador/compromiso co-localizados resueltos. La transferencia dinámica de propietarios, la conmutación automática, la finalización activa-activa, la finalización móvil, subceldas y protocolos de recursos físicos/sanitización se posponen para plataformas externas/familias DG-E. Su estado no se refleja en el núcleo semántico.
Controles aplicados actuales
El código actual tiene análisis/errores tipados útiles, muchos límites, hash canónico, evaluación de tres estados, verificaciones de identidad de gráfico/ley, apertura de etapa explícita, autenticación/autorización de herramientas, validación de esquema, tiempos de espera de proveedor y límites de respuesta, algunos controles de SSRF/ruta, redacción, verificaciones de firma/ancla, transacciones de SQLite, eventos de auditoría y verificaciones de integridad de ejecución.
El código actual impone identificadores mediados por constructores acotados, coordenadas de espacio de nombres no cero, vocabularios finitos canónicos, procedencia de transporte revisada, identidad de ley de escenario nominal, DgValueFormatV1, dominios de condición tipados y predicados, vinculaciones de adquisición independientes, admisión de evidencia factorizada, instantáneas canónicas y evaluación pura sin I/O. El tiempo de ejecución soportado contiene solo la presentación del llamador, tiempo nombrado, instantáneas de entorno inmutables en la lista blanca, y adquisición estricta de JSON/YAML basada en capacidades; las rutas de red y proveedor ejecutable no son alcanzables.
PF-04 además impone identidad de ejecución acuñada por autoridad, familias de operación nominal, resolución de recibo solo aceptada primero, aceptación condicional de cabeza exacta, tiempo de aceptación tipado nombrado, tuplas aceptadas atómicas, estado actual acotado, historia inmutable indexada, rehidratación hostil de esquema-12 y cuarentena de integridad a través de memoria y SQLite. La resolución de recibo de creación está limitada al espacio de nombres, y la relación de admisión sellada no puede ser acuñada a través de la construcción de variante de enumeración pública.
El esquema 12 también vincula la identidad de evidencia de gobernanza sellada en la misma transacción de ejecución aceptada. La auditoría y la entrega de uso son idempotentes por la identidad de evento estable y devuelven un recibo solo después de la entrada duradera. La entrega sigue siendo una obligación separada de la transacción de base de datos de ejecución aceptada; la intención almacenada evita que la mutación se convierta en libre de evidencia.
PF-05 impone puntos de control de auditoría coherentes y neutrales al backend, exportación indexada acotada con propiedad de revisión/cursor verificada, construcción hostil de runpack-v6, publicación inmutable local enraizada en capacidades, reducción de historia aceptada de material suministrado independiente, informes de reclamación total y presupuestos de trabajo deterministas. La integridad estructural se completa de forma independiente antes de la interpretación semántica, y MCP autoriza el namespace vinculado al manifiesto antes de la travesía completa del objeto. La configuración/tiempo de ejecución de OSS no tiene ruta de runpack de S3/almacenamiento de objetos o modo de verificador capaz de obtener.
Las brechas actuales incluyen la aprobación humana explícita de la base formal de garantía compartida sintética, un cierre de garantía PF-03 separado y un pase de correspondencia de implementación adversarial, un cierre de modelo de despacho PF-06A sucesor, tiempo de ejecución de recuperación local PF-06B, refinamiento de modelo/backend y reclamación fuera de línea PF-06C, contrato de adaptador de plataforma PF-06D, integración de producto estable de asignación PF-06E y conformidad PL-05; autenticidad/actualidad externa PF-07, anclaje de retroceso coherente y calificación de despliegue; calificación de publicación remota PF-08; ejecución de DG de los arneses PF-05 verificados a través de la autoridad Kani aislada y fijada del repositorio; un resultado dorado de Windows observado; transmisión de un millón de registros, memoria máxima y evidencia calibrada del corredor de productos; evidencia portable de Certesa; y aprobación de lanzamiento. Los pines de Rust de producción y Rust empaquetados con Kani son autoridades separadas, por lo que su diferencia de versión no es en sí misma una brecha.
Evidencia requerida
- Pruebas de sellado de fallo de compilación y bypass de constructor.
- evidencia de referencia y propiedad de RET/Xarxa.
- Pruebas adversariales de condición/evidencia/esquema/almacenamiento/runpack.
- Pruebas adversariales específicas de fuente de llamador/tiempo/entorno/documento.
- Instantánea/evaluación determinista y equivalencia en vivo/reproducción.
- Alcance negativo para capacidades de adquisición/ejecución no soportadas.
- Modelo/mutación/evidencia de traza de ejecución aceptada PF-03 y refinamiento independiente de modelo a Rust/backend PF-04; cierre de suposición de fundación compartida, no vacuidad, inducción, corroboración simbólica, refinamiento, mutación sistemática y calificación de oráculo independiente; re-cierre de garantía PF-03 separado; y un cierre de despacho PF-06A sucesor bajo esa autoridad.
- Autorización, atribución, obsolescencia/carrera, pérdida de respuesta, fallo, corrupción y pruebas de retención.
- Objeto/árbol/manifiesto de runpack-v6 hostil, paridad de punto de control, sustitución/carrera de sistema de archivos local, mutación de reductor independiente, dependencia de reclamo, material suministrado, presupuesto determinista, convergencia de creación nueva concurrente y pruebas de identidad canónica dorada cruzada entre sistemas operativos.
- Autoridad externa específica de perfil y calificación de despliegue.
Cada informe indica lo que su evidencia establece y lo que permanece no probado. El volumen de prueba nunca es la preparación para el lanzamiento.
Modelo de Amenaza Delta (2026-07-17, corte duro de corrección): actualizado. El esquema 12 vincula atómicamente la identidad de intención de gobernanza, las costuras de auditoría y uso de MCP son falibles y portadoras de recibos, y los sumideros no duraderos fallan en cerrado. El registro coincidente es Docs/security/deltas/2026-07-17-certesa-decision-gate-correctness-hard-cut.md.
Modelo de Amenaza Delta (2026-07-18, corte duro de autoridad de ventana fija): actualizado. Decision Gate ahora tiene una autoridad de solicitud de ventana fija acotada, respaldada por un reloj monótono, sellada y compartida por la entrada de MCP y la composición de herramientas con alcance de cuenta. Las formas deshabilitadas de valor cero, el muestreo de corrección ambiental, los algoritmos de cubo duplicados y los caminos de mutación antes de fallar son rechazados. El registro coincidente es Docs/security/deltas/2026-07-18-fixed-window-rate-limit-authority-hard-cut.md.
Modelo de Amenaza Delta (2026-07-18, exactitud de cable cerrado de ejecución aceptada): actualizado. Los estados etiquetados Unset, RunWide y Empty de la ejecución aceptada ahora rechazan campos hostiles en exceso en su frontera de cable de propiedad central. El registro coincidente es Docs/security/deltas/2026-07-18-accepted-run-closed-wire-exactness-hard-cut.md.