Se il ricercatore ha trovato soddisfacibilità in qualsiasi software, questa è una minaccia per la sicurezza? In caso di risposta - "Sì", in che modo l'attaccante può utilizzare SAT?
Se il ricercatore ha trovato soddisfacibilità in qualsiasi software, questa è una minaccia per la sicurezza? In caso di risposta - "Sì", in che modo l'attaccante può utilizzare SAT?
La tecnica di esecuzione simbolica , usata in KLEE, è solo un modo per chiedere a un solutore SAT di validare / invalidare le possibili esecuzioni nel software senza eseguirlo per davvero. Permette di concentrarsi solo sui percorsi ammissibili.
Quindi, questa non sarà una minaccia alla sicurezza se puoi eseguire un solutore SAT e convalidare / invalidare i percorsi del tuo software. Voglio solo dire che sarai in grado di esplorare tutti i suoi percorsi di esecuzione di sicuro (esaurientemente).
Significa anche che l'interno del tuo software può essere completamente esplorato, il che potrebbe essere un problema se vuoi nascondere qualcosa (un algoritmo brevettato, una chiave crittografica, ...). In tal caso, le persone tendono a utilizzare tecniche specifiche di offuscamento (di solito predicati opachi specifici per sconfiggere i solutori del SAT) per rendere più difficile l'esplorazione di tutti i percorsi eseguibili.
Spero che questo ti aiuti a capire meglio l'intera cosa.
Leggi altre domande sui tag c++ c binary-code fuzzing