Mi sono imbattuto in questo termine chiamato "Satisfiability Modulo Theories", che quando ho cercato su Google, era qualcosa che si relazionava a varie teorie sui linguaggi di basso livello. In che modo questo aiuta a scoprire 0 giorni? Ho visto anche persone che usano qualcosa chiamato "risolutore Z3" potrebbe qualcuno dare una spiegazione più breve di ciò che è?
Satisfiability Modulo Theories (SMT) sono concetti matematici che esaminano come è possibile calcolare qualcosa. Queste teorie si riferiscono a cose che troverete in molti linguaggi di programmazione come numeri reali e interi, elenchi, ecc. E che sono essenziali per i computer.
I solutori SMT (come Z3) sono programmi per computer che generano automaticamente prove per problemi matematici correlati. Quindi, se si dispone di una dichiarazione di un problema (un teorema) che è possibile codificare nella lingua di input per tale risolutore, il risolutore restituirà una prova, se possibile.
Un'area di applicazione per i risolutori SMT è un approccio chiamato "esecuzione simbolica". Nell'esecuzione simbolica, sei meno interessato all'esecuzione effettiva di un programma per computer, ma a esplorare quali sono le esecuzioni generali con input diversi. Ad esempio, in un calcolo reale, ti piacerebbe ottenere un numero come output definitivo. Nell'esecuzione simbolica sarai più interessato a cose più generali come il tipo di output.
L'esecuzione simbolica può essere utilizzata per eseguire analisi di sicurezza come il controllo dell'inquinamento, ovvero tracciare un input durante l'esecuzione di un programma. Questo aiuta a scoprire tutti i tipi di vulnerabilità, compresi gli exploit zero-day.
Leggi altre domande sui tag zero-day