In che modo la verifica formale garantisce un codice sicuro e privo di errori?

Non garantisce che il codice sia privo di vulnerabilità. Tuttavia, se la verifica viene utilizzata in modo appropriato, può aumentare la certezza (riservatezza) che l'applicazione è sicura.

Parlando da una prospettiva molto ampia, ci sono due aspetti di questo problema:

• Verifica. Dato un modello matematico del sistema e una specifica matematica dei requisiti, il sistema soddisfa le specifiche?

• Convalida. abbiamo l'insieme di requisiti giusto ? Le specifiche matematiche riflettono accuratamente i veri requisiti? Il modello matematico corrisponde esattamente e completamente al codice?

A volte le persone si concentrano solo sulla verifica, ma entrambe sono importanti.

Nella tua situazione, se la specifica incorpora tutti i requisiti di sicurezza pertinenti e se il modello matematico corrisponde correttamente al codice e se la verifica viene eseguita in modo appropriato e ha esito positivo, quindi possiamo avere una base per aumentare significativamente la certezza che il sistema soddisferà i nostri requisiti di sicurezza.

Nel migliore dei casi, la verifica può essere un potente strumento per garantire la sicurezza, una delle più potenti che abbiamo. Tuttavia, come con qualsiasi altra cosa, è possibile abusare della tecnologia o ottenere un falso senso di sicurezza se non viene usato in modo appropriato. Una delle modalità di errore più comuni è che il processo di verifica non verifica tutti i requisiti di sicurezza pertinenti (alcuni sono trascurati o omessi).

Per dire molto di più potrebbe essere necessario approfondire i dettagli del sistema, i requisiti di sicurezza e la natura della verifica, ma si spera che questo ti fornisca una panoramica.

La verifica formale non garantisce un sistema sicuro. Niente garantisce un sistema sicuro. Ciò che la verifica formale può fare è fornire una garanzia molto elevata che alcune parti del sistema sono sicure.

La verifica formale fornisce una prova matematica che, in base a determinati presupposti, un modello del sistema ha determinate proprietà. Pertanto, se una parte del sistema è stata verificata formalmente, rimangono ancora diverse condizioni per la sicurezza del sistema:

• Le ipotesi sottostanti alla verifica sono soddisfatte?
• Il sistema corrisponde al modello che è stato verificato?
• La prova fornita dal sistema di verifica è corretta?
• Le proprietà comprovate sono sufficienti per garantire la sicurezza del sistema?

L'entità della verifica formale può variare molto. Ad esempio, buffer overflow - un tipo comune di vulnerabilità - può essere individuato abbastanza facilmente: la maggior parte delle lingue che sono di livello superiore a C o C ++ garantiscono l'assenza di buffer overflow nel programma compilato. Può comunque accadere che il compilatore permetta il passaggio del codice - mentre i bug del compilatore sono molto più rari dei bug del programma, non sono impossibili. Gli overflow del buffer sono solo un tipo, tuttavia; la maggior parte della sicurezza dei sistemi dipende molto più dal sapere che non ci sono buffer overflow. (Lettura correlata: Perché i computer non controllano se ci sono contenuti di memoria in qualche spazio di memoria? )

Per illustrare le limitazioni di cui sopra, vorrei fare un esempio concreto. Alcune smart card eseguono una Java Card macchina virtuale ed esegui solo bytecode che è stato verificato . Il verificatore bytecode, in linea di principio, garantisce che il codice non possa sbirciare o colpire al di fuori dello spazio di memoria assegnato. Questo evita alcune vulnerabilità ma non tutte:

• La verifica garantisce le sue proprietà solo se l'interprete bytecode si comporta secondo le sue specifiche. Inoltre, se l'hardware non esegue correttamente l'interprete, tutte le puntate sono disattivate (ad esempio, un modo per attaccare una smartcard è provocare un power glitch che comporta l'ignoranza di alcune istruzioni).
• Se è presente un bug che consente di caricare il codice senza passare attraverso il verificatore, è possibile che il codice sulla scheda non abbia le proprietà garantite dalla verifica.
• Il verificatore stesso potrebbe essere bacato e consentire il caricamento di codice errato.
• Anche se il codice delle applicazioni sulla scheda non accede direttamente alla memoria di altre applicazioni, potrebbe comunque spiarle o perturbarle in altri modi. Ad esempio, può sfruttare un canale laterale come il tempismo per dedurre le proprietà di altro codice in esecuzione sullo stesso dispositivo.
  Inoltre, la sicurezza del sistema può dipendere da cose diverse dall'isolamento tra le applicazioni sulla scheda. Ad esempio, il sistema di autenticazione può consentire a un utente malintenzionato di assumere il controllo della carta, potrebbe esserci una vulnerabilità a livello di protocollo che consente all'autore dell'attacco di interrompere le comunicazioni, ecc.

In un sistema ad alta sicurezza, la verifica formale può aiutare in due modi:

• Dimostrando che il codice corrisponde alle sue specifiche. Ciò richiede un modello formale dell'ambiente di esecuzione (hardware, compilatore o interprete, libreria standard, ...) e molto lavoro.
• Dimostrando che le specifiche hanno alcune proprietà desiderabili. Ciò richiede una formalizzazione delle specifiche, una scelta giudiziosa delle proprietà e molto lavoro.

I Common Criteria per le valutazioni di sicurezza definiscono diversi livelli di garanzia . Solo il livello di garanzia più elevato (EAL7) richiede una verifica formale. Questo non è l'unico requisito: la verifica formale non preclude la valutazione di altri aspetti del sistema, tra cui documentazione, test di penetrazione, ecc.

La verifica formale funziona davvero solo in casi estremamente limitati in cui un sistema può essere modellato come una serie di trasformazioni con domini, intervalli e regole chiaramente comprensibili che definiscono il comportamento di una funzione - in molti casi questo significa che tu? si tratta di un sistema che è la realizzazione del software di un modello matematico, o che è (relativamente :-)) facile derivare un modello dal comportamento del sistema (circuiti digitali di una complessità significativamente inferiore rispetto a una CPU generica)

Ho lavorato in alcuni precursori a questo negli anni '80, dove lo sforzo era nel generare "codice provabilmente corretto". Un sistema che ricordo si chiamava Adele e operava su programmi scritti in (uggh) Ada. Aneddoticamente, scherzavamo dicendo che usare Adele significava che impiegava 10 volte più tempo per scrivere, che funzionava 10 volte più lentamente, e che si riduceva solo del 10% - Potresti voler guardare gli scritti di Bertrand Meyer su Eiffel, ha messo pensiero e sforzo significativi su come un linguaggio potrebbe fornire controlli di verifica interni tramite precondizioni, postcondizioni, invarianti e un sacco di altre cose che ho dimenticato da allora .....

Verifiche per verificare se il sistema ha una proprietà specificata. Proprietà espresse in varie notazioni e logiche. Specificare queste proprietà è difficile. Quindi, se un designer può esprimere la sua idea di sicurezza in una notazione formale adatta per la verifica, e il software ha dimostrato di soddisfare la proprietà, allora sì è sicuro. Nella vita reale, il suo obiettivo quasi impossibile è verificare proprietà non banali sul software reale in esecuzione su hardware di uso generale

Qualsiasi vulnerabilità è un termine troppo ampio, poiché la verifica formale (in effetti la prova automatica che un algoritmo / sistema possiede proprietà specifiche) è orientata verso minacce specifiche: dati sensibili che fuoriescono, informazioni esterne che filtrano attraverso le difese, le perdite di memoria, gli errori di allocazione, gli stack overflow ecc. Per alcune anteprime del lavoro corrente a questo proposito è possibile ad esempio visita Istituto di Ingegneria del Software presso Carnegie-Mellon Uni.

La verifica formale verifica solo la conformità della codifica alle specifiche fornite. Se una specifica stessa è impropria / errata, allora un'eventuale verifica non ha evidentemente valore. Per informazioni sulla verifica formale vedi per es. link e link

Qualsiasi modello non può garantire un codice sicuro e privo di errori. Solo i test continui possono darti una sicurezza temporanea. Finire un codice non significa che rimarrà sicuro, quindi sono necessari ulteriori test continui contro le nuove vulnerabilità.