Teorema de seguretat
DG tracta les especificacions, l’evidència, els comandaments, els bytes emmagatzemats, la sortida del proveïdor, l’entrada de l’operador, els artefactes generats i els testimonis d’autoritat externa com a hostils als seus límits propietaris.
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 fracàs d’adquisició operativa no mintarà cap candidat semàntic. Un candidat obsolet no canvia cap estat acceptat. Una intenció acceptada no és un efecte extern realitzat. L’autoritat de desplegament s’importa a través de testimonis exactes i mai s’infereix de l’espai de noms, ruta, memòria cau, o configuració local.
Actius protegits
- Lleis, gràfics, condicions, polítiques i identitats de l’escenari canònic.
- Adquisició, admissió, política d’ús, progrés, preparació, i testimonis de completament.
- Valors d’evidència, referències, procedència, abast, temps, sensibilitat, i metadades de retenció.
- Caps d’execució acceptats, història immutable, rebuts d’idempotència, intencions d’evidència de governança, i registres de despachament.
- Autenticació, autorització, atribució, contracte de proveïdor, i fets d’admissió de desplegament extern.
- Runpacks, informes de verificació, registres d’auditoria, acreditacions, i claus de signatura.
- Capacitat, autoritat, decisió, prova, i registres de publicació.
Adversaris
Suposem que hi ha agents maliciosos o compromesos, autors d’escenaris, fonts d’evidència, proveïdors, emmagatzematge, dipòsits de despachament, operadors, complements, proxies, CI, SDKs, i poblacions de nodes qualificades. Suposem reproducció, reordenament, duplicació, omissió, equívoc, lectures obsoletes, retrocés, procedència falsificada, confusió d’esquema, diputat confós, fallida parcial, travessia de camins, curses de symlink, SSRF, injecció de subprocessos, esgotament de recursos, i divulgació d’acreditacions.
Un host/kernel compromès està fora de l’habilitat del procés per neutralitzar, però la seva autoritat, material retingut, i radi d’explosió romanen explícits.
Mapa de límits
| Límite | Únic propietari d’admissió | Resultat permanent |
|---|---|---|
| Sintaxi de l’escenari | constructor de llei d’escenari | ValidatedScenarioLaw |
| Sintaxi RET i refinaments | RET | requisit validat/satisfactori/monotònic |
| Topologia de dependència | Xarxa | identitat de gràfic, progrés, preparació, delta de completament |
| Evidència del cridant | constructor de font del cridant | testimoni d’adquisició del cridant |
| Evidència de temps/env/document | constructors de font local | testimoni d’adquisició específica de la font |
| Ús d’evidència | avaluador de política de condicions | testimoni de satisfacció de política i instantània canònica |
| Acceptació de candidats | autoritat d’execució acceptada | revisió acceptada o rebuig tancat |
| Bytes d’emmagatzematge | rehidratació d’emmagatzematge local | valors acceptats reconstruïts o rebuig |
| Exportació d’auditoria acceptada | backend d’execució acceptada seleccionat | punt de control exactament acceptat més pàgines de punt de control limitades |
| Bytes de runpack | constructors runpack-v6 | identitats exactes de manifest/objecte/arbre o rebuig tipat |
| Avaluació RET | requisit/pla validat i executor limitat | resultat semàntic o fracàs operatiu tipat |
Font de broker file:// | AdmittedFileRoot explícit | capacitat de directori retinguda o denegació tipada |
| Publicació de runpack local | repositori arrelat a capacitats | resultat exacte d’objecte/manifest nou creat |
| Material de verificació | constructor de material subministrat | conjunt de material local/agrupat limitat sense autoritat de resolució |
| Reclamacions de verificació | registre de reclamacions tancades i verificador independent | informe total de dependències comprovades |
| Execució d’intencions | autoritat de despach | resultat exacte de diari/rebut |
| Fets d’autenticació i desplegament | adaptadors d’autoritat externa/incrustada | testimoni d’admissió d’operació exacte |
Amenaces de l’escenari i del gràfic
| Amenaça | Control requerit |
|---|---|
| Gràfic o testimoni falsificat | Construcció segellada; bytes hostils es reconstrueixen a través de constructors. |
| Substitució de gràfic/llei | Cada progrés, frontera, delta, execució, registre, i empaquetat d’execució vincula exactament la identitat de gràfic/llei. |
| Topologia penjant, auto, cíclica, duplicada, no-monòtona, o esgotada | Xarxa/RET rebutja abans de validar la llei. |
| Regressió de progrés o gràfic incorrecte | El progrés vinculat al gràfic i el delta de completament comparen identitat i inclusió monòtona. |
| Obertura/completament duplicada | Cicle de vida segellat més idempotència/conflicte d’execució acceptada. |
| Fan-out implícit, selecció de branca, o cancel·lació | La frontera és només descriptiva; l’operador obre explícitament una etapa. |
| Obertura d’etapa interpretada com a assignació | L’atribució roman fora de la propietat de gràfic/etapa; la coordinació és externa. |
| Full estructural interpretat com a èxit | Només llei de completament d’escenari explícita. |
| Execució recursiva oculta | L’avaluació mai comença/evalua un altre escenari. |
| Fet d’execució externa obsolet | L’evidència vincula exactament la llei/execució/capçalera externa i la política d’actualitat. |
Amenaces de representació i identitat
| Amenaça | Control requerit |
|---|---|
| Identitat invàlida construïda per API o deserialització | Emmagatzematge de domini privat, transportador hostil privat, constructor fallible, i Serde mediada per constructor. |
| Normalització o aliasing d’identificador | Gramàtica ASCII exacta sensible a majúscules; sense retallades, plegament Unicode, plegament de majúscules, o coerció per a identificadors DG autoritzats. |
| Substitució d’identitat nominal | Tipus de domini Rust distint; sense identificador de cadena genèric o conversió no verificada. |
| Deriva de token de vocabulari tancat | Una taula total de variants/token generada posseeix anàlisi, visualització, Serde, OpenAPI, i JSON Schema. |
| Camps excedents contrabandats en un estat de suma tancada sense camps | Estats sense camps etiquetats internament utilitzen variants d’objecte buit exactes més evidència de rebuig de fils hostils; les variants d’unitat Serde no són admeses per a sumes d’objectes tancats. |
| Procedència de sol·licitud només d’agent | El constructor de procedència compartida retorna un error tipat a menys que hi hagi una identitat de sol·licitud emesa pel servidor present. |
| Identitat de sol·licitud d’agent tractada com a autoritat o idempotència | La procedència de transport roman no autoritzada i nominalment separada de la identitat d’operació semàntica. |
| Ambigüitat d’amplada/codificació de digest | Bytes SHA-256 fixos internament i projecció de fils exacta de 64 caràcters en minúscules. |
| Substitució de digest entre subjectes | Identitat de subjecte nominal més separador de domini fix i revisió de format; els digests de contingut genèrics no poden entrar en consumidors d’identitat de llei d’escenari. |
| Format antic acceptat a través d’un alias o migració | dag-v2 i anteriors, runpack v5 i anteriors, i cada esquema SQLite diferent de 12 rebutgen com a entrades hostils no suportades. |
PF-04 tanca la execució propietària del protocol, intent, obertura, presentació, intenció, registre acceptat/capçalera, i identitats d’idempotència a través de tipus mediats per constructors nominals. Les projeccions emmagatzemades o de runpack romanen hostils i es reconstrueixen a través d’aquests constructors.
Amenaces de condició i evidència
Confusió de categoria i autoritat
La implementació ha de prevenir:
- canal d’adquisició interpretat com a autoritat de font o rang de confiança;
- localitzador/referència interpretat com a canal d’adquisició;
- l’atestació interpretada com a veritat universal o transport;
- identitat de condició fusionada per text de consulta de proveïdor igual;
- el proveïdor/consulta es tracta com a semàntica de condició inherent;
- estat, confiança, procedència, absència, o resultat de comparador subministrat per l’agent;
- l’evidència que falta s’interpreta com a absència observada;
- error del proveïdor emmagatzemat com a evidència semàntica;
- violació de contracte reetiquetada com a
Unknownsemàntic.
Només els fets factoritzats més un testimoni de política d’ús de condicions exactes autoritzen l’ús.
Presentació d’agent
Les amenaces inclouen la falsificació de la identitat del cridant, material de mida excessiva, substitució entre execucions/condicions, temps de procedència o observació autoassignats, inflació de reintents de quòrum d’origen del mateix principal, afirmacions obsoletes, i retenció excessiva de dades sensibles. L’admissió vincula el context d’autoritat autenticada o incrustada, la procedència de la sol·licitud revisada, l’autoritat estable del principal/perfil, el contingut exacte, els límits, l’abast objectiu, el temps de rebut propietat del límit, i la política de divulgació/retenció. Les identitats de sol·licitud mai defineixen la independència de l’origen. Les reclamacions del cridant romanen distingibles dels fets verificats.
Temps
Les lectures del rellotge ambiental poden fer que la reproducció sigui no determinista o permetre la falsificació de frescor. L’avaluació rep un context temporal explícit. El temps utilitzat com a evidència prové d’una autoritat nomenada i vincula interval, resolució, incertesa, i domini del rellotge. El fracàs mai fabrica un segell temporal.
Entorn
Les amenaces inclouen filtració secreta, lectures mutables, accés a claus no configurades, esgotament de codificació/tamany, i falsa absència. El perfil inicial utilitza claus validades en la llista blanca i una instantània d’inici immutable per defecte. Cada observació vincula la identitat de la instantània, la clau, un resultat explícit present-o-observat-absent, sensibilitat, i divulgació/retenció. Les codificacions opcionals/null no poden crear absència, i una reclamació d’instantània hostil incompleta no pot substanciar cap forma de contingut.
JSON/YAML arrelat
Les amenaces inclouen la travessia de pares, camí absolut, cursa de symlink, escapament de root, accés a dispositius/FIFO/socket, substitució després de la comprovació, fitxers massa grans, arbres profunds o amplis, amplificació d’alias/tag YAML, claus duplicades, documents de retallada, inclusions de xarxa, anàlisi parcial, i falsa absència.
Els controls requereixen arrels registrades, rutes relatives validades, contenció canònica, objectes oberts regulars, digest de bytes exactes oberts, anàlisi completa limitada, política de duplicats/retallades, sense escapament de xarxa/incloure, i anàlisi completa abans de l’absència. Els constructors de testimonis de temps nomenats, entorn i document comparteixen el límit de privadesa del nucli central amb la construcció d’evidència segellada; un nucli Rust separat no pot cridar aquests constructors per auto-mintar un fet de font local.
Instantània i política
La identitat d’evidència duplicada, la dependència de l’ordre d’arribada, la fabricació de zero-quorum, l’avaluació incompleta del candidat, la reutilització entre objectius sense un testimoni, la revocació obsoleta, i la inflació de Sybil de línia fallen tancades. Una instantània canònica i una avaluació total de política d’ús posseeixen el resultat.
Amenaces d’incapacitat excloent
La xarxa anterior, MCP remot, subprocess, i la línia de temps del proveïdor executable estan absents de la implementació inicial. Si alguna família exclosa es torna a introduir, roman no suportada i inaccessibilitat des de tots els camins de configuració i eines suportades fins que la seva pista independent PF-08 es tanqui.
Adquisició de xarxa
Les amenaces inclouen SSRF, reassignació de DNS, redireccions, accés privat/local de vincle, exfiltració d’acreditacions, confusió de proxy, contraban de respostes, cossos il·limitats, tempestes de reintents, DNS/política obsolets, deriva de contractes i equívoc de fonts remotes. DG-DECISION-NETWORK-ACQUISITION-001 ha d’aprovar la llei del testimoni de la font, l’autoritat d’egressió/acreditació, els límits i la qualificació abans del suport.
Subprocessos i execució arbitrària
Les amenaces inclouen injecció de comandament/argument, substitució executable, secrets/entorn heretat, confusió de directori de treball, processos orfes, falsificació de sortida, escape de recursos, i compromís d’amfitrió. El DG inicial no carrega codi de proveïdor natiu arbitrari i no suporta cap adquisició de MCP stdio/subprocess. L’execució futura prefereix un procés aïllat, WASM, o protocol remot versionat amb manifest signat, capacitats, pressupostos de recursos/xarxa, validació de sortida hostil, i qualificació.
Avaluació remota
Els bytes de proposta segellada i amb aspecte de segell no demostren l’avaluació. Un treballador remot pot reclamar cada etapa superada. Els perfils inicials co-localitzen l’avaluació i el compromís. La verificació de proves remotes o l’execució attestada requereix un perfil independent; l’attestació només prova la seva reclamació d’execució mesurada exacta, no la veritat del món o la correcció matemàtica.
Amenaces d’execució acceptada
| Ameaça | Propietat de protocol requerida |
|---|---|
| El cridant tria una identitat de execució reutilitzada | DG genera un RunId opac no reutilitzable a partir de la sol·licitud de creació idempotent. |
| Mateixa sol·licitud, contingut diferent | Conflicte d’idempotència tipada. |
| Repetició de la mateixa sol·licitud | Resultat original exacte; sense intent o intent de duplicat. |
| Dos candidats competeixen des d’una capçalera | Com a màxim un successor directe; el perdedor és obsolet i no canvia res. |
| Resposta perduda després de l’acceptació | Resolució per identitat d’operació estable. |
| Caiguda abans/després de la transacció | El backend refina el model aprovat i preserva l’atomicitat/comportament de rebut. |
| Capçalera falsificada | Validació hostil; sense mutació d’estat. |
| Desacord entre capçalera/historial emmagatzemat | Fallida d’integritat, quarantena/recuperació; mai reparació local per suposicions. |
| Confusió d’autorització/atribució | L’adaptador deriva un testimoni exacte; la sol·licitud semàntica no pot auto-seleccionar un principal/agent. |
| La cerca de rebut es produeix després d’una comparació obsoleta | La cerca de rebut acceptada és la primera; una capçalera posterior no pot ocultar un resultat acceptat. |
| Eliminació de rebut acceptat o tombstone de RunId | Autoritats indexades permanents; la compactació requereix prova de dependència i no pot debilitar la repetició/no reutilització. |
| Compromís d’estat/historial/rebut/capçalera/intenció dividida | Un únic tuple acceptat atòmic o un tartamudeig autoritari complet. |
| La mutació acceptada manca d’evidència de governança | El tuple acceptat atòmic porta una identitat GovernanceEvidenceIntent segellada i retorna CommittedWithGovernanceIntent. |
| L’auditoria o l’ús del resultat es descarta | Cada autoritat de destí retorna un rebut estable o un fracàs tipat; els destins no duradors rebutgen, i el fracàs primari més el de governança roman un compost. |
| Resultat fals conegut-no acceptat després d’un possible compromís | Unavailable requereix prova de no acceptació; l’ambigüitat és Indeterminate. |
| El cridant o el rellotge ambiental subministren el temps de compromís | L’autoritat de temps injectada nomenada genera un testimoni tipat abans del compromís; la revisió per si sola ordena la història. |
| La repetició torna a mostrejar el temps d’acceptació | El rebut acceptat retorna el testimoni de temps original. |
| Bypass de quarantena d’integritat | La quarantena bloqueja cada acceptació posterior per a l’autoritat afectada. |
| Prova de rebut no autoritzada/divulgació de resultats | L’autorització precedeix la cerca de rebut i governa la divulgació exacta del resultat. |
| Prova de creació-rebut entre espais de noms | La resolució de creació vincula l’espai de noms autoritzat abans de la cerca de rebut; un rebut estranger és indistinguible de l’absència delimitada. |
| Identitat d’operació semàntica utilitzada sota una família d’operacions diferent | Les famílies d’operacions nominals romanen distintes; els resultats abstractes i els rebuts acceptats satisfan la invariant de família-abast comprovada. |
| Construcció directa del material d’admissió reclamat | El testimoni d’admissió de l’execució acceptada té estat privat, sense deserialitzador brut, constructors de límits explícits i projecció de persistència de només lectura. |
| Canvis d’encoding específics del backend limiten l’admissió | Els límits semàntics canònics propietat del nucli són idèntics per a la memòria i SQLite; l’overhead de l’envolupant de persistència té un sostre immutable separat. |
| Exhauriment d’emmagatzematge de rebut/tombstone | Els límits immutables nomenats i les fallades de capacitat fallen conegut-no acceptat abans del compromís; els fets semàntics no són expulsats silenciosament. |
| Retrocessió coherent d’una base de dades local completa | No reclam extern d’ancoratge explícit; els auto-hashtags locals no fabriquen resistència a la retrocessió. |
VIEW formal o restricció oculta un successor que viola | Les configuracions autoritàries rebutgen VIEW, SYMMETRY, i restriccions d’estat; les empremtes dactilars TLC completen l’estat del model. |
| Coordinades de cadena d’eines no aprovades arriben a la descàrrega o execució | El bootstrap valida el tancament complet aprovat abans de l’ús de xarxa o Java, i després permet només espais de noms de versions exactes i artefactes fixats per digest. |
| L’acció modelada no té traç de refinament PF-04 | L’esquema de traç, el mapa d’accions, i els vocabularis del corpus observat han de ser exactament iguals; una transició independentment incorrecta ha de fallar l’oracle TLA. |
PF-03 tanca la decisió de propietat/model abstracte amb evidència TLC limitada, contraexemples de mutació esperats i traçades deterministes de PF-04. PF-04 implementa la relació i reprodueix setze traçades genèriques de protocol contra la memòria i SQLite més dues traçades de reinici durables contra SQLite. La memòria té evidència de reinici negativa explícita. Aquesta refinament local no estableix propietat distribuïda, resistència a retrocessos externs, o recuperació de despach.
Amenaces de despach
El model de candidat PF-06A tracta aquests com a casos adversarials explícits:
| Amenaça | Límits de control/reclamació permanents |
|---|---|
| Despatx d’una intenció no acceptada | Només una mutació propietària acceptada pot entrar en elegibilitat. |
| Substitució de targeta, executor, autorització o perfil de recuperació | Un vincle immutable d’un sol objectiu es manté en cada registre del diari. |
| Capçalera de diari falsificada, intent o completament ABA | Caps exactes i identitats d’intent mai reutilitzades fan que les accions obsoletes es retardi. |
| Un treballador completa la reserva en viu d’un altre treballador | El diari vincula les identitats del treballador i d’intent mai reutilitzades; els registres de progrés han de presentar el parell exacte. |
| Rebut falsificat, efecte creuat o conflictiu | Autoritat de rebut qualificada i vinculació exacta d’efecte/clau; quarantena de conflicte. |
| El diari s’auto-emiteix rebut o qualificació de testimoni | Les accions del diari consumeixen fets de qualificació exactament pre-admesos; emmagatzemar un identificador no pot crear autoritat d’origen. |
| La identitat del rebut es reutilitza | La propietat del rebut és funcional i la reutilització de la identitat a través de fets del diari acceptats falla tancada. |
| Un resultat de consulta autoritzada es substitueix per un rebut d’efecte | Consulta realitzada, consulta no realitzada, i material de rebut estable són famílies de testimonis tipificades distintes amb propietaris exactes. |
| El resolutor informa falsament que s’ha realitzat o no s’ha realitzat | PF-06A només comprova la relació de qualificació importada exacta i porta el testimoni; el verificator extern roman com una premissa nomenada que requereix qualificació PF-06C. |
| Reclamació falsa d’efecte previ o no ocorregut | Es requereix un testimoni nomenat exacte; l’ambigüitat post-límit roman indeterminada, i un fracàs pre-límit posterior no pot esborrar el deute d’ocurrència no resolta anterior. |
| Testimoni de no ocurrència reutilitzat o sense nom | Les identitats de testimoni d’efecte previ, consulta autoritzada, i caducitat/exactitud es mantenen, tipificades per família, de propietari únic, i mai reutilitzades. |
NoResolver es confon amb “no pot tenir èxit” | Els rebuts d’èxit en viu qualificats són independents de la resolució post-ambigüitat; tots els perfils poden registrar l’èxit sincrònic testificat, però només els resolutors qualificats poden tancar l’ambigüitat automàticament. |
| Reintents insegurs o vinculació d’invocació canviada | El reintentar requereix el perfil de clau exacta qualificat i preserva la identitat lògica, objectiu, contingut, revisió d’executor, vinculació d’autorització, perfil de recuperació, i clau d’idempotència. |
| Efecte lògic duplicat després de la pèrdua de resposta | El recompte d’invocacions de DG, el recompte d’execució física externa, i una ocurrència lògica són separades; la idempotència de clau exacta limita l’execució física només per a un perfil d’executor qualificat. |
| La invocació de límit es tracta com a prova d’ocurrència | El recompte d’invocacions i l’ocurrència externa són independents; realitzat implica invocació, però la invocació pot romandre no realitzada fins que un resolutor qualificat tanqui el coneixement. |
El xoc oblida Started, rebut, o estat terminal | El perfil durable preserva el coneixement del diari; la memòria explícitament no fa cap reclamació de reinici. |
| El xoc després de l’compromís d’intenció de domini/governança però abans de l’append de primer dipòsit | La tupla d’intenció de domini i governança compromesa és monòtona i la reconciliació de reinici es reprèn des de la intenció retinguda. |
| Reconeixement de governança abans de l’append durable | El reconeixement requereix un rebut estable exacte després del compromís de dipòsit durable. |
| Substitució d’identitat/payload de governança | Registres de governança amb clau independent i relació de redelivery exacta. |
| Tupla d’intenció de domini/governança importada incompleta | PF-06A requereix la tupla PF-04 monòtona completa i no reclama falsament tornar a provar el compromís atòmic de PF-04. |
| La compensació s’admet de la veritat d’ocurrència oculta o esborra la història original | La compensació requereix un estat realitzat conegut per DG i és un efecte vinculat completament separat amb un diari independent. |
| Perfil de compensació no qualificat | La creació de compensació requereix el perfil d’efecte-família exactament admès a més de la performance coneguda per DG. |
| Bypass de quarantena o mutació d’index/propietari d’efecte creuat | La quarantena és monòtona; els índexs de propietat d’efecte i les projeccions de diari/versiones coincideixen; els efectes registrats de manera independent no es muten entre si. |
| El progrés just o la durabilitat de la memòria es suposen implícitament | Registre d’assumpcions nomenades més models de contraexemple d’execució sense justícia i de falsa durabilitat de memòria; cap reclamació no segueix de la seguretat. |
| Prova no autoritzada de rebut/estat | PF-06B ha d’autoritzar abans de la divulgació; PF-06A no modela els interiors d’autenticació. |
| Retrocés coherent del diari de despach | No reclam de l’ancoratge extern; els auto-hashes locals no poden provar la frescor. |
DG-DECISION-DISPATCH-MODEL-001 roman obert. El candidat v5 és InvalidatedForApproval; el seu informe limitat és evidència de regressió històrica, no un subjecte d’aprovació. Encara no existeix cap temps d’execució de diari/recuperació permanent. La intenció acceptada, un bloqueig local, la satisfacció del model limitat, i la invocació com a màxim una vegada no són efectes externs exactament una vegada.
Amenaces de límit d’assegurament formal
| Amenaça | Control/limitació permanent |
|---|---|
| Una propietat d’estat accessible està mal etiquetada com inductiva | TLAPS ha de descarregar les obligacions exactes d’inicialització, preservació i implicació; la capacitat d’abast de TLC per si sola no pot crear InductivelyProved. |
| El refinament està mal etiquetat com inducció | Les files de prova model-a-model informen RefinementSatisfied; la correspondència de producció roman una reclamació propietat d’un protocol separat. |
| Un model buit/inaccessible genera una propietat verda | L’estat inicial, l’acció, la branca i l’antecedent de no vacuïtat requereixen cobertura més oracles d’abast d’exemple esperat. |
| La matriu limitada es descriu però no s’executa | Cada fila de perfil compilada produeix un acord positiu exacte o una execució de desacord testimoniada. |
| El denominador de mutació omet una guàrdia o escriptura autoritzada | Cada conjunció de màquina d’estat registrada té un punt de mutació exacte i cada propietat posseeix almenys un operador de kill. |
| L’ambigüitat del parser admet suposicions ocultes o quocients | Files de suposicions exactes propietat del mòdul; sintaxi de configuració tancada; rebuig insensible a la indentació de VIEW, SYMMETRY, restriccions, sobrescriptures i modes d’inicialització duals. |
| La proposició de prova es reemplaça mentre els tokens tàctics semblen vàlids | La propietat exacta de la proposició canònica rebutja comentaris, LET, files de teoremes desconeguts i fulles no provades/omitides. |
| Ambdós camins semàntics comparteixen el mateix error de transició | Comparació exhaustiva de relacions finites TLA/Python, separació explícita del gràfic d’importació i detecció deliberada de desacords; la independència d’autoria roman una no-reclamació de revisió humana. |
| El checkout mutable canvia després de l’admissió | Cada eina executa una instantània de font verificada per digest extern immutable i el denominador de la font en viu es torna a comprovar després de l’execució. |
| La instal·lació d’eines o proves es substitueix | Arxius/instal·ladors oficials, manifestos, rebuts d’instal·lació, arbres d’execució i manifestos d’artefactes estan separadament vinculats per digest. |
| L’arbre TLAPS no determinista es denomina falsament reproductible | El subjecte candidat vincula la política d’instal·lador oficial fixat; cada informe d’execució vincula el seu arbre instal·lat exacte; la reproductibilitat de l’arbre instal·lat en brut és una no-reclamació explícita. |
| La qualificació sintètica s’interpreta com a prova del protocol DG | La frontera de reclamació candidata i la identitat del protocol són verificades per màquina; la reclusió PF-03 i un successor PF-06A romanen aprovacions separades. |
El candidat de fundació compartida actual satisfà el seu denominador sintètic registrat però espera l’aprovació humana explícita. No canvia la capacitat d’execució de producció i no autoritza cap reclam de protocol PF-03 o PF-06A.
Amenaces d’emmagatzematge i reproducció
Tots els bytes emmagatzemats/runpack són hostils. Els controls inclouen rebuig de versió, decodificació limitada abans de l’assignació, aritmètica comprovada, rebuig de duplicats/traçadors, reconstrucció mediada per constructors, recomputació d’identitat canònica, comprovacions exactes de cap/història i dependències de retenció explícites.
Els antics formats de prellançament rebutgen sense migració. Un digest només prova la seva relació d’integritat nomenada, no l’autenticitat de l’origen, l’autoritat del cap actual, la protecció contra retrocessions, o l’ancoratge extern. La reconsulta en viu és nova evidència. Els informes de repetició indiquen exactament quina adquisició original, esquema, autorització, frescor, i relacions de política poden ser reconstruïdes.
PF-05 assume a més arbres de manifest/objecte hostils, bytes suplementaris subministrats de manera hostil, continguts de repositori local compromesos, ordenació/rangs de registres maliciosos, bombes de decomposició, curses de publicació, substitució de camins/símbols, confusió de dependències de reclamació i esgotament de recursos de verificació. Els controls són dotze arrels familiars obligatòries, identitats fixes de separació de domini nominal, objectes limitats canònics, comprovacions de rang/fanout/profunditat, aritmètica comprovada, pàgines limitades per punts de control, un redactor independent, un DAG de reclamacions tancat, pressupostos de treball deterministes, objectius de sistema de fitxers relatius a capacitats, publicació de creació de nous objectes, comparació exacta de bytes retinguts i visibilitat de manifest últim.
El verificador resol només material local empaquetat o explícitament subministrat. No té autoritat de xarxa, proveïdor, rellotge, SQLite, MCP, camí ambiental, o resolutor genèric. Un localitzador mai no satisfà la disponibilitat del material. Els bytes suplementaris externs en brut només poden satisfer relacions de digest/estructura; no poden mintar autenticitat de font, actualitat, resistència al retrocés, despachament, desplegament, o reclamacions de procedència de construcció.
Amenaces de desplegament
L’espai de noms, la ruta, la memòria cau, la identitat del node, l’etiqueta de regió o la configuració no demostren l’assignació de servei, l’autorització, la capacitat, la residència, l’autoritat de clau, o la qualificació de l’evaluador. Els adaptadors de perfil consumeixen testimonis externs exactes amb subjecte, revisió d’autoritat, abast, actualitat i operació.
Les rutes d’escala inicial distingeixen execucions a nodes d’evaluació/compromís co-localitzats resolts. La transferència dinàmica de propietaris, el failover automatitzat, la finalitat activa-activa, les subcèl·lules i els protocols de recursos físics/sanitització es deixen per a famílies externes de plataforma/DG-E. El seu estat no es reflecteix en el nucli semàntic.
Controls actuals imposats
El codi actual té un útil anàlisi/error tipat, molts límits, hashing canònic, avaluació tri-estat, comprovacions d’identitat de gràfics/llei, obertura de fase explícita, autenticació/autorització d’eines, validació d’esquema, temps d’espera del proveïdor i límits de resposta, alguns controls SSRF/camí, redacció, comprovacions de signatura/ancoratge, transaccions SQLite, esdeveniments d’auditoria, i comprovacions d’integritat de runpack.
El codi actual imposa identificadors mitjançant constructors limitats, coordenades d’espai de noms no zero, vocabularis finits canònics, procedència de transport revisada, identitat de llei de situació nominal, DgValueFormatV1, dominis de condicions tipades i predicats, vinculacions d’adquisició independents, admissió d’evidència factoritzada, instantànies canòniques, i avaluació lliure d’E/S pura. El temps d’execució suportat conté només la presentació de l’agent, temps nomenat, instantànies d’entorn immutables autoritzades, i adquisició JSON/YAML estricta arrelada a capacitats; les rutes de xarxa i proveïdors executables no són accessibles.
PF-04 a més imposa identitat de run mintada per autoritat, famílies d’operació nominal, resolució de rebut acceptat només primer, acceptació condicional exacta, temps d’acceptació tipat nomenat, tuples acceptades atòmiques, estat actual limitat, història immutable indexada, rehidratació hostil d’esquema-12, i quarantena d’integritat a través de memòria i SQLite. La resolució de rebut de creació és limitada a l’espai de noms, i la relació d’admissió segellada no pot ser mintada a través de la construcció de variants d’enumeració pública.
L’Esquema 12 també vincula la identitat de governança-evidència segellada dins de la mateixa transacció d’execució acceptada. L’auditoria i la entrega d’ús són idempotents per identitat d’esdeveniment estable i retornen un rebut només després d’un ingrés durable. La entrega roman com una obligació separada de la transacció de base de dades d’execució acceptada; la intenció emmagatzemada impedeix que la mutació esdevingui lliure d’evidència.
PF-05 imposa punts de control d’auditoria coherents i neutres al backend, exportació indexada limitada amb propietat de revisió/cursor comprovada per constructors, construcció hostil runpack-v6, publicació immutable local arrelada a capacitats, reducció d’història acceptada de material subministrat independent, informes totals de reclamacions, i pressupostos de treball deterministes. La integritat estructural es completa de manera independent abans de la interpretació semàntica, i MCP autoritza l’espai de noms vinculat al manifest abans de la travessia completa de l’objecte. El runtime/configuració OSS no té camí de runpack S3/object-store ni mode de verificador capaç de recuperar.
Les llacunes actuals inclouen l’aprovació humana explícita de la fundació formal d’assegurança compartida sintètica, un tancament d’assegurança PF-03 separat i un pas de correspondència d’implementació adversarial, un tancament de model de despach PF-06A successor, un temps d’execució de recuperació local PF-06B, refinament de model/backend i reclamació fora de línia PF-06C, contracte d’adaptador de plataforma PF-06D, integració de producte estable d’assignació PF-06E i conformitat PL-05; PF-07 autenticitat/exactitud externa, ancoratge de retrocés coherent, i qualificació de desplegament; PF-08 qualificació de publicació remota; execució de DG dels arnesos PF-05 registrats a través de l’autoritat Kani aïllada del repositori; un resultat daurat de Windows observat; streaming de milions de registres, memòria màxima, i evidència calibrada de corredor de productes; evidència Certesa portàtil; i aprovació de llançament. Els pins de Rust de producció i Rust empaquetat amb Kani són autoritats separades, així que la seva diferència de versió no és en si mateixa una llacuna.
Evidència requerida
- Proves de segellament de fallida de compilació i bypass de constructors.
- evidència de referència i propietat RET/Xarxa.
- Proves hostils de condició/evidència/esquema/emmagatzematge/runpack.
- Proves adversarials específiques de font d’agent/temps/entorn/document.
- Instantània/evaluació determinista i equivalència en viu/reproducció.
- Abast negatiu per a capacitats d’adquisició/execució no suportades.
- Model/mutació/evidència de traç acceptat PF-03 amb un model/mutació/traç independent PF-04; tancament d’assumpcions de fonament compartit, no-vacuitat, inducció, corroboració simbòlica, refinament, mutació sistemàtica, i qualificació d’oracle independent; re-tancament d’assegurament PF-03 separat; i un tancament de despachament PF-06A successor sota aquesta autoritat.
- Autorització, atribució, obsolet/cursa, pèrdua de resposta, fallada, corrupció, i proves de retenció.
- Objecte/arbre/manifesta hostile runpack-v6, paritat de punts de control, substitució/cursa del sistema de fitxers local, mutació de reductor independent, dependència de reclamació, material subministrat, pressupost determinista, convergència de creació nova concurrent, i proves d’identitat canònica daurada entre sistemes operatius.
- Autoritat externa específica del perfil i qualificació de desplegament.
Cada informe indica el que la seva evidència estableix i el que roman no provat. El volum de prova no és mai preparat per al llançament.
El Model d’Amenaça Delta (2026-07-17, tall dur de correcció): actualitzat. L’Esquema 12 vincula atòmicament la identitat d’intenció de governança, les costures d’auditoria i ús de MCP són fallibles i portadores de rebut, i els dipòsits no durables fallen tancats. El registre coincident és Docs/security/deltas/2026-07-17-certesa-decision-gate-correctness-hard-cut.md.
Model de Amenaces Delta (2026-07-18, tall dur d’autoritat de finestra fixa): actualitzat. Decision Gate ara té una autoritat de sol·licitud fixada, segellada, amb rellotge monòton, compartida per l’entrada MCP i la composició d’eines amb abast d’account. Les formes desactivades de valor zero, l’amplada de mostreig de correcció ambiental, els algorismes de cubs duplicats i els camins de mutació abans de fallar són rebutjats. El registre coincident és Docs/security/deltas/2026-07-18-fixed-window-rate-limit-authority-hard-cut.md.
Model de Ameaça Delta (2026-07-18, exactitud de cable tancat d’execució acceptada): actualitzat. Els estats etiquetats Unset, RunWide, i Empty de l’execució acceptada ara rebutgen camps hostils superflus a la seva frontera de cable propietat del nucli. El registre coincident és Docs/security/deltas/2026-07-18-accepted-run-closed-wire-exactness-hard-cut.md.