Utilizzo di dimostratori di teoremi per trovare gli attacchi

Question

Ho sentito parlare dell'utilizzo di dimostratori di teoremi automatici nel tentativo di dimostrare che le vulnerabilità di sicurezza non esistono in un sistema software. In generale questo è diabolicamente difficile da fare.

La mia domanda è: qualcuno ha mai lavorato su come utilizzare strumenti simili a trovare le vulnerabilità nei sistemi esistenti o proposti?

---

Eidt: Sono NON chiedendo di dimostrare che un sistema software è sicuro. Sto chiedendo di trovare (idealmente precedentemente sconosciute) vulnerabilità (o anche classi di esse). Sto pensando come (ma non è) un cappello nero qui: descrivi la semantica formale del sistema, descrivi ciò che voglio attaccare e poi lascia che il computer capisca quale catena di azioni devo usare per prendere il controllo del tuo sistema.

Answer 1

Quindi, almeno in un senso significativo, l'opposto di provare che qualcosa è sicuro è trovare percorsi di codice per i quali non lo è.

Prova Byron Cook's TERMINATOR project.

E almeno due video su Channel9. Here's one of them

La sua ricerca è probabilmente un buon punto di partenza per imparare su questa area di ricerca estremamente interessante.

Anche progetti come SpeC# e Typed Assembly Language sono correlati. Nel loro tentativo di spostare la possibilità di verifiche di sicurezza da runtime in fase di compilazione, consentono al compilatore di rilevare molti percorsi di codice errati come errori di compilazione. Rigorosamente, non aiutano il tuo dichiarato intento, ma la teoria che sfruttano potrebbe esserti utile.

Answer 2

Non è realmente correlato alla dimostrazione teorica, ma fuzz testing è una tecnica comune per la ricerca di vulnerabilità in modo automatico.

Answer 3

C'è lo L4 verified kernel che sta cercando di fare proprio questo. Tuttavia, se si guarda alla storia dello sfruttamento, si trovano modelli di attacco completamente nuovi e quindi un sacco di software scritto fino a quel punto è molto vulnerabile agli attacchi. Ad esempio, le vulnerabilità delle stringhe di formato non sono state scoperte fino al 1999. Circa un mese fa H.D. Moore ha rilasciato DLL Hijacking e letteralmente tutto sotto Windows is vulnerable.

Non credo sia possibile dimostrare che un software è sicuro contro un attacco sconosciuto. Almeno non prima che un teorema sia in grado di scoprire un simile attacco e, per quanto ne so, questo non è accaduto.

Answer 4

Disclaimer: hanno poca o nessuna esperienza con provers teorema automatizzati

alcune osservazioni

• Cose come la crittografia sono raramente mai "provato", solo che si ritiene essere sicuro. Se il tuo programma usa qualcosa di simile, sarà forte quanto la crittografia.
• I tester di teoremi non possono analizzare tutto (o potrebbero risolvere il problema di interruzione)
• È necessario definire in modo molto chiaro che cosa significa non valido per il rilevatore.Questo di per sé è una grande sfida

Answer 5

Sì. Molti progetti di dimostrazione di teoremi mostrano la qualità del loro software dimostrando buchi o difetti nel software. Per renderlo correlato alla sicurezza, immagina di trovare un buco in un protocollo di sicurezza. Il dottorato di Carlos Olarte la tesi di Ugo Montanari ha un esempio del genere.

È nell'applicazione. Non proprio lo stesso dimostratore di teoremi che ha qualcosa a che fare con la sicurezza o la conoscenza speciale di ciò.

Answer 6

Attualmente sto scrivendo un parser PDF in Coq insieme a qualcun altro. Mentre l'obiettivo in questo caso è quello di produrre un pezzo di codice sicuro, fare qualcosa del genere può sicuramente aiutare a trovare bug di logica fatale.

Una volta acquisito familiarità con lo strumento, la maggior parte delle prove diventa facile. Le prove più difficili producono casi di test interessanti, che a volte possono far scattare bug in programmi reali esistenti. (E per trovare i bug, puoi semplicemente assumere teoremi come assiomi una volta che sei sicuro che non ci siano errori da trovare, nessuna seria dimostrazione necessaria.)

Circa una falena fa, abbiamo riscontrato un problema durante l'analisi di PDF con più/vecchi Tavoli XREF. Non siamo riusciti a dimostrare che l'analisi termina. Pensando a questo, ho costruito un PDF con i puntatori loop/prev nel trailer (chi lo avrebbe mai pensato? :-P), che naturalmente ha fatto sì che alcuni spettatori continuassero per sempre. (In particolare, praticamente tutto il visore poppler basata su Ubuntu. Mi ha fatto ridere e la maledizione Gnome/evince-Thumbnailer per mangiare tutta la mia CPU. Credo che è stato risolto ora, tho.)

---

Utilizzando Coq a trovare bug di livello inferiore sarà difficile. Per provare qualcosa, hai bisogno di un modello del comportamento del programma. Per problemi stack/heap, probabilmente dovrai modellare l'esecuzione a livello di CPU o almeno a livello di C. Anche se tecnicamente possibile, direi che non ne vale la pena.

L'utilizzo di SPLint per C o la scrittura di un correttore personalizzato nella lingua scelta dovrebbe essere più efficiente.

Answer 7

Sì, molto lavoro è stato fatto in questo settore. I solutori Satisfiability (SAT e SMT) vengono regolarmente utilizzati per trovare vulnerabilità di sicurezza. Ad esempio, in Microsoft, uno strumento chiamato SAGE viene utilizzato per eliminare i bug di sovraccarico del buffer da Windows. SAGE utilizza lo Z3 theorem prover come verificatore di soddisfacibilità. Se si cerca su internet usando parole chiave come "fuzzing intelligente" o "fuzzing white-box", si troveranno molti altri progetti che utilizzano controlli di soddisfacibilità per trovare vulnerabilità di sicurezza. L'idea di alto livello è la seguente: raccogli i percorsi di esecuzione nel tuo programma (che non sei riuscito a esercitare, cioè non hai trovato un input che lo ha eseguito), converti questi percorsi in formule matematiche e fornite queste formule a un risolutore di soddisfacibilità. L'idea è di creare una formula che sia soddisfacibile/fattibile solo se c'è un input che farà eseguire il programma il percorso specificato. Se la formula prodotta è soddisfacente (vale a dire fattibile), allora il risolutore di soddisfacibilità produrrà un'assegnazione e i valori di input desiderati. I fuzzer a scatola bianca usano strategie diverse per selezionare i percorsi di esecuzione. L'obiettivo principale è trovare un input che faccia in modo che il programma esegua un percorso che porta a un arresto anomalo.

Answer 8

STACK e KINT risolutori di vincoli utilizzati per trovare le vulnerabilità in molti progetti OSS, come il kernel linux e ffmpeg. Le pagine del progetto indicano documenti e codice.