Questo esperimento dimostra la potenza della matematica basata sulla forza bruta

Nel mondo dell'informatica, la soluzione "a forza bruta" di solito è ben lontana dall'essere quella migliore. Presto o tardi finisce per funzionare, ma è anche incredibilmente poco efficiente e decisamente poco "furba". Il fatto che esista una soluzione a forza bruta per un problema, di solito implica l'esistenza di un'altra soluzione più elegante, ma anche meno ovvia.

Per capire meglio cosa intendo si può partire da un problema base di algebra: 2x + 100 = 500. Per risolvere questo problema con un approccio "a forza bruta" basta semplicemente provare ogni valore possibile per x fino a quando l'equazione non diventa vera. Sappiamo, però, che è molto più efficiente riorganizzare l'equazione usando le regole algebriche, e così facendo ci basteranno soltanto due passi computazionali per trovare una soluzione.

Gli informatici, però, stanno cercando di guardare gli attacchi a forza bruta da un altro punto di vista. In un paper pubblicato sull'ultimo Communications of the ACM, Marijn Heule e Oliver Kullman sostengono che stiamo entrando in una nuova era in cui l'approccio a forza bruta potrebbe avere un ruolo chiave, in particolare quando si tratta di sistemi critici dal punto di vista della sicurezza. Tutto ciò grazie a una tecnologia relativamente recente chiamata Satisfiability (SAT) solving, un metodo che permette di generare delle dimostrazioni attraverso la logica proposizionale.

In pratica, possiamo unire un approccio di problem solving ottimizzato ma basato sulla forza bruta con i moderni e accessibili super computer per ottenere un metodo sufficientemente conveniente per risolvere problemi molto complessi. La tecnologia a disposizione è abbastanza potente che spesso non avremo più bisogno della furbizia per risolvere i problemi quando in sostituzione di essa abbiamo un gran bel mucchio di processori.

"Oggi, il SAT solving sfruttato su sistemi computerizzati ad alta performance ci permette di risolvere problemi di grandissima complessità attraverso un approccio pratico," scrivono Heule e Kullmann. "La combinazione di questa enorme potenza computazionale con questa 'forza bruta magica' ci permette oggi di risolvere probleme combinatori molto difficili."

Per comprendere questo potenziale, c'è bisogno di spiegare due cose sulla logica formale.
Nella logica proposizionale, una proposizione è una dichiarazione che può essere vera o falsa.

La cosa più importante è questa dichiarazione ha la proprietà di poter essere negato. La dichiarazione "Vado a prendermi un kebab," per esempio, può essere svolta in forma negativa dicendo "Non vado a prendermi un kebeb." Quindi, la dichiarazione è una proposizione. La logica proposizione prevede la certificazione che una determinata dichiarazione sia vera attraverso l'utilizzo di diversi operatori logici come AND o OR oppure NOT. Come nell'esempio algebrico fatto sopra, dichiarazioni apparentemente molto complicate possono essere trasformate in dichiarazioni la cui veridicità è ovvia.

L'informatica prevede molte proposizioni, o dichiarazioni vero/falso. Questa è un po' la sua essenza, a dir la verità. Nella logica proposizionale formale, possiamo immaginarci una serie di unità atomiche individuali di verità (che possono essere vere o false e possono essere combinate attraverso gli operatori logici di cui abbiamo parlato prima. Per esempio, potremmo avere la dichiarazione ((true AND false) OR true) AND NOT (true OR false) e ci si può chiedere se, in via definitiva, la dichiarazione sia vera o falsa. Non lo è, ma probabilmente non è ovvio. Questi ragionamenti possono diventare molto complicati da valutare, e se hai mai avuto a che fare con la logica formale sai che molto spesso trovare la soluzione significa andare per tentativi, sfruttando ovvero un approccio a forza bruta.

Il SAT solving è più simile a un insieme di approcci diversi per arrivare ad una soluzione ottenuta con la forza bruta. Ci sono diversi modi per decomporre in maniera intelligente dei grossi problemi — pensate alla dichiarazione di prima, ma aggiungeteci milioni di clausole 'true' e 'false' — cercando certi tipi di sotto-problemi ed eliminando le contraddizioni interne. Sono scorciatoie, in pratica, ma sono comunque a forza bruta.

Il risultato finale del SAT solving è una prova, che consiste di solito in una lista noiosa ma esaustiva di tutti i passaggi necessari per trasformare o decostruire la dichiarazione iniziale in più dichiarazione nette di verità o falsità. Come parte della loro ricerca, Heule e Kullmann hanno dimostrato un SAT solver automatico che ha prodotto una prova da 200 terabyte, che per capirci è una prova di dimensioni davvero davvero gigantesche.

Resta da chiedersi perché tutto ciò abbia a che fare con la sicurezza: bisogna pensare al concetto di correttezza. Nell'informatica, significa che un algoritmo risponde a determinate specifiche. Si comporta come previsto e a un certo punto si arresta. La correttezza è dimostrata attraverso il processo della verifica formale. Gli algoritmi, o le dichiarazioni che compongono gli algoritmi, possono essere ridotti a logica proposizionale così da poter essere verificati. Il problema è che quando gli algoritmi si complicano, la verifica formale diventa più complicata. Allo stesso tempo, la complessità degli algoritmi rende la verifica formale sempre più importante. Più complesso è l'algoritmo più spazio hanno i bug per nascondersi.

Quindi, l'approccio SAT offre un modo per avere una verifica formale automatizzata e la possibilità di utilizzare a poco prezzo dei supercomputer nel 2017 rendere la verifica formale fattibile.

"Ora bisogna riuscire a gestire i sistemi molto complessi, e bisogna riuscire a comprendere le nuove possibilità," concludono Heule e Kullman.