Die "brutalste" Methode zum Passwortknacken läutet eine neue Ära der IT-Sicherheit ein

In der Informatik gilt die sogenannte "Brute-Force"-Methode normalerweise als wenig effiziente Vorgehensweise, um eine Aufgabe zu knacken. Zwar produziert sie am Ende das gesuchte Ergebnis, braucht dafür aber sehr lange – auf Deutsch wird sie auch als "Methode der rohen Gewalt" bezeichnet. Wenn es für ein bestimmtes Problem eine Brute-Force-Lösung gibt, bedeutet das normalerweise, dass es auch einen eleganteren Weg gibt. Zwei Informatiker setzen jedoch große Hoffnung in die alte Methode und sagen ihr dank einer neuen Anwendungstechnik ein Comeback voraus.

Um die Funktionsweise der Brute-Force-Methode zu verstehen, schaut man sich am besten eine einfache Gleichung an: 2x + 100 = 500. Jeder mit ein paar Algebra-Grundkenntnissen sieht, dass man die Gleichung schnell lösen kann, indem man sie umstellt. So erhält man in zwei Rechenschritten den gesuchten Wert 200 für x. Die Brute-Force-Methode hingegen geht stumpf so lange alle Möglichkeiten für x durch, bis sie den passenden Wert gefunden hat. Das dauert zwar länger, bringt aber irgendwann ebenfalls das richtige Ergebnis.

Folgt Motherboard auf Facebook, Instagram, Snapchat und Twitter

Die Brute-Force-Methode – also einfach jede mögliche Lösung durchzuprobieren – wird besonders gerne zum Knacken von Passwörtern verwendet. Aus diesem Grund ist es auch sinnvoll, ein besonders sicheres Passwort zu wählen, da die Schwierigkeit, das Problem zu lösen mit der Anzahl der möglichen Lösungen exponentiell steigt.

Doch zwei Informatiker geben der Brute-Force-Methode gerade noch eine weitere Chance, sich im digitalen Zeitalter als nützlich zu erweisen. In einem Paper, das in der aktuellen Ausgabe von Communications of the ACM (Association for Computing Machinery) erschienen ist, argumentieren die Informatiker Marjin Heule und Oliver Kullmann, dass wir am Beginn "einer neuen Ära" stehen. Sie glauben, dass die Brute-Force-Methode eine Schlüsselrolle spielen könnte, wenn es um Systemsicherheit und Systemschutz geht. Den Aufschwung verdankt die Brute-Force-Methode einer verhältnismäßig neuen Technologie zur Problemlösung, den sogenannten Satisfiability (SAT)-Solvern, die untersuchen, ob eine aussagenlogische Formel erfüllbar ist.

Die Idee von Heule und Kullmann: Kombiniert man die durch die SAT-Solver optimierte Brute-Force-Methode mit modernen Supercomputern, kann man damit hochkomplexe Aufgaben lösen. Dank dieser Technologie braucht man nicht mehr unbedingt viel Raffinesse bei der Problemlösung, solange man über genug leistungsfähige Prozessoren verfügt.

"Diese Kombination von enormer Rechenleistung mit der 'magischen Brute-Force' kann heute sehr schwierige kombinatorische Probleme lösen oder beispielsweise die Sicherheit von Systemen wie Eisenbahnstrecken prüfen", schreiben die Autoren in ihrem Paper.

Um das Potenzial der Brute-Force zu verstehen, muss man erstmal ein wenig über mathematische Logik, speziell die sogenannte Aussagenlogik, wissen.

In der Aussagenlogik kann jede Aussage entweder wahr oder falsch sein. Somit muss jede Aussage auch negiert werden können. Die Aussage "Ich kaufe mir jetzt einen Döner" wird in verneinter Form zu "Ich kaufe mir jetzt NICHT einen Döner". In der Aussagenlogik wird mit sogenannten logischen Operatoren wie UND und ODER und NICHT nachgewiesen, dass Aussagen wahr sind. Wie im Algebra-Beispiel weiter oben können die kompliziert aussehenden Aussagen oft so umgestellt werden, dass ihr Wahrheitswert schnell offensichtlich wird.

Auch die Informatik basiert im Grunde auf "wahr"- und "falsch"-Aussagen. In der klassischen Aussagenlogik können wir uns eine Reihe von individuellen Wahrheitswerten (die entweder wahr oder falsch sind) in Kombination mit den oben genannten logischen Operatoren vorstellen.

Nehmen wir beispielsweise die Aussage: ((wahr UND falsch) ODER wahr) UND NICHT (wahr ODER falsch). Ist diese Aussage nun insgesamt wahr oder falsch? Die Aussage ist falsch, aber das ist möglicherweise nicht auf den ersten Blick erkennbar. Solche Aufgaben können schnell sehr kompliziert werden und jeder, der schon mal mit mathematischer Logik gerungen hat, hat irgendwann wahrscheinlich einfach nur noch geraten und das Ergebnis überprüft – und somit unbewusst die Brute-Force-Methode verwendet.

Ebenfalls auf Motherboard: Die Mathematik eines Massenaufstands

SAT-Solver sind eine Art Werkzeugkasten, die auf der Brute-Force-Methode basieren. Sie identifizieren Teilprobleme und spüren interne Widersprüche auf – im Endeffekt funktionieren sie wie Abkürzungen. Das Endergebnis vom SAT-Solving ist ein mathematischer Beweis, der in vielen, extrem mühsamen Teilschritten die ursprüngliche Aussage umstellt und neu arrangiert, sodass klare Aussagen herauskommen, die wahr oder falsch sind. Als Teil ihrer Forschung führten Heule und Kullmann einen automatisierten SAT-Solver vor, der einen Beweis in Größe von 200 Terabyte produzierte. Als jemand, der selbst schon ganz tief in den Irrgarten der mathematischen Logik vorgedrungen ist, wird mir bei diesen Zahlen ganz schwindelig.

Die Informatik basiert auf dem Prinzip der Korrektheit, ein Algorithmus muss bestimmte Kriterien erfüllen, damit er funktioniert. Diese Korrektheit lässt sich durch formale Verifikation nachweisen. Algorithmen – oder die Aussagen, die die Algorithmen bilden – können auf Aussagenlogik heruntergebrochen werden und somit als korrekt verifiziert werden. Allerdings dauert das sehr, sehr lange: Da die Algorithmen immer komplizierter werden, wird auch die Verifikation immer schwieriger. Doch die formale Verifikation ist sehr wichtig, um Sicherheitslücken auszuschließen.

Die Studie kommt zu dem Schluss, dass SAT-Solving-Methoden und kostengünstige Supercomputer zusammen eine neue Lösung für die formale Verifikation darstellen. "Jetzt müssen wir uns der wachsenden Komplexität stellen und die neuen Möglichkeiten ergreifen", folgern Heule und Kullmann. "Mathematische Beweise müssen zum Forschungsgegenstand werden, so dass wir mehr darüber verstehen, wie wir sie finden und mit ihnen umgehen können."