(openPR) Der von QBF Deutschland vor einem Jahr angekündigte SAT Solver hat seine Feuertaufe überstanden.
Das Wiesbadener Unternehmen QBF Deutschland kündigte Anfang 2019 einen SAT Solver an, der möglicherweise alle Instanzen des als schwierig geltenden Erfüllbarkeitsproblems der Aussagenlogik in polynomialer Laufzeit lösen kann. Vor einer Veröffentlichung des SAT Solvers sollte laut Unternehmen jedoch zunächst ein rigoroser mathematischer Beweis für das Funktionieren des zugrundeliegenden Algorithmus gefunden und die Auswirkungen auf die Internetsicherheit evaluiert werden.
„Ich habe durchaus lange überlegen müssen, wie es jetzt genau weiter gehen sollte“, so der Unternehmensinhaber Christopher Heiling. „Wir waren in einer Art Dilemma gefangen. Zum einen enthält der Beweis, dass der Algorithmus tatsächlich jede Instanz in Polynomialzeit löst, grundlegende und lang erwartete Einsichten in Aussagenlogik im Speziellen und theoretische Informatik im Allgemeinen. Zum anderen würde eine Veröffentlichung des Beweises nicht nur ein Reverse Engineering des Algorithmus erlauben, sondern damit auch gleichzeitig eine schwer zu rechtfertigende Gefährdung der Internetsicherheit darstellen. Nach Abwägung verschiedener Aspekte haben wir uns aus ethischen Gründen dazu entschlossen sowohl den Beweis, als auch den Algorithmus zunächst für Universitäten und Forschungsinstitute auf Anfrage freizugeben. Sobald wir ein angemessenes System zur Risikokontrolle entwickelt haben, werden wir den Algorithmus auch für private Unternehmen veröffentlichen. Bis dahin werden wir bei Bedarf einen Lösungsservice für NP-Probleme anbieten.“
Nicht selten ist die Grundlage der Verschlüsselung von Daten im Internet der sogenannte Diffie-Hellman Key Exchange. Die so ausgetauschten Informationen können im Prinzip durch ein Faktorisierungsproblem wiederhergestellt werden. Ein solches Faktorisierungsproblem kann mit Hilfe des SAT Solvers effizient gelöst werden, was in der Praxis bedeutet, dass gegenwärtig ein gesicherter Austausch von verschlüsselten Informationen im Rahmen dieses Verfahrens nicht länger gegeben ist.
Neben den Schattenseiten, die mit der Lösung des Erfüllbarkeitsproblems der Aussagenlogik einhergehen gibt es allerdings auch durchaus positive Effekte. So können viele Probleme der Wirtschaft und auch der Wissenschaft und Forschung, für die man bisher – wenn überhaupt - lediglich suboptimale Lösungen finden konnte, jetzt auch optimal gelöst werden.
