Ok, quindi la fiducia viene trasferita dal componente al correttore di prove. Su quali basi può essere considerato attendibile il processo di certificazione del correttore di bozze?
Il processo di certificazione del controllo bozze può essere considerato attendibile perché:
- il controllore di prove definisce la politica di sicurezza;
- il correttore di bozze utilizza i suoi assiomi per convalidare il predicato di sicurezza, e quindi sa se il predicato di sicurezza soddisfa o meno le condizioni della politica di sicurezza;
- Il correttore di prove stabilisce le regole di generazione VC, le regole di prova e le precondizioni, (essenzialmente la "convenzione di chiamata") che definisce in che modo il consumatore del codice richiama i binari.
Sembra tutto a posto, giusto? Tuttavia, prima che ciò accada, il consumatore del codice definisce e pubblica la sua politica di sicurezza.
- Le politiche di sicurezza rimangono statiche?
- Le politiche di sicurezza, in qualsiasi momento, sono sufficienti con le regole di generazione VC, le regole di dimostrazione e le condizioni preliminari per certificare che i predicati di sicurezza stabiliscono veramente il codice non dannoso conforme?
- I produttori di codice possono realmente certificare un predicato di sicurezza utilizzando la logica del primo ordine in tempo polinomiale?
To the first point, if the safety policy is found to be too simplistic, or ineffective lacking the proper axioms, it will change, which means it must be rewritten and republished, which means the code producer must redevelop a safety predicate and safety proof for re-certification.
Quale produttore di codice (sperando di riutilizzare il codice in ambienti diversi) sta costantemente ricreando i predicati di sicurezza e riprogettando le prove di sicurezza ogni volta che la politica di sicurezza di qualcuno cambia, per ogni possibile scenario? La questione della fiducia è un vincolo per il consumatore del codice, non per il produttore del codice a cui potrebbe importare se i suoi binari sono attendibili.
To the second point,
To formulate safety policy, code consumers must make assumptions about what constitutes sufficient conditions to certify a safety predicate. Simply because a safety predicate receives certification, does not mean it is truly safe. Rather, it only means that it has meet the minimal necessary conditions imposed by the code consumers; so some minimal threshold for sufficiency which may not be enough to ensure real safety.
Se un consumatore di codice costruisce e pubblica una politica di sicurezza inefficace, il processo di certificazione non fornisce un controllo sufficiente contro l'esecuzione di codice dannoso. In realtà, questo modello ha il produttore del codice che abroga la propria responsabilità per la scrittura di codice attendibile, a favore della scrittura di codice che passa semplicemente le condizioni minime per la certificazione (cioè uno che produce un predicato di sicurezza minimamente accettabile).
Finally, to the third point,
The author notes "In order to create a safety proof, the code producer must prove a predicate in first-order logic. In general, this problem is undecidable."
Se la creazione di una prova di sicurezza richiede di dimostrare un predicato nella logica del primo ordine che è "in generale" indecidibile, ciò implica che il produttore del codice non può in generale creare una prova di sicurezza, quindi quale è la certificazione in primo luogo? Non è tutto semplicemente accademico?
Ci sono altri problemi che gli autori fanno riferimento nell'introduzione che " ... ci sono molti problemi difficili che rimangono da risolvere. " Veramente!
RISPOSTA :
You ask Is there any reason PCC is not more widely used?
It sounds like there's very little incentive on the part of code producers to be more widely using this model, given the apparently impossible battle they face in creating a safety proof for their predicate and in having their safety predicate meet conditions of some particular certification process.