In welcher Beziehung steht die Theoretische Informatik zur Sicherheit?

11

Wenn ich an unsichere Software denke, denke ich, dass sie "zu nützlich" ist und von einem Angreifer missbraucht werden kann. In gewissem Sinne bedeutet das Sichern von Software, dass Software weniger nützlich ist. In der Theoretischen Informatik arbeiten Sie nicht mit der realen Welt. Gibt es also Sicherheitsbedenken bei der Arbeit mit reiner Theorie? Oder auf der anderen Seite der Medaille: Beeinflusst die Theoretische Informatik die reale Welt der Menschen, die gehackt werden? Wenn ja, welche Sicherheitsthemen gelten als theoretisch?

Der Turm
quelle
9
Die vorgestellte Perspektive der CS-Theorie ist subjektiv und sehr umstritten und muss auch nicht gestellt werden, um die Frage zu stellen. Die Frage scheint sich speziell auf das Hacken zu konzentrieren, das an und für sich ein weites Thema ist (bis hin zu Social-Engineering-Techniken) und nicht annähernd dem entspricht, was "sicher sein" bedeutet. Aus diesen Gründen habe ich abgelehnt. Ich habe jedoch das Gefühl, dass die Frage von einem guten Ort kommt und einige interessante Aspekte hat, daher habe ich unten geantwortet.
Ross Snider

Antworten:

20

Ihre Intuition, dass "Unsicherheit" auf Software zurückzuführen ist, die "zu nützlich" ist, ist in gewissem Sinne richtig. Es gibt eine große und wachsende theoretische Literatur zum Thema "Differential Privacy", die Ihre Intuition formalisiert. Siehe zum Beispiel hier: research.microsoft.com/en-us/projects/databaseprivacy/dwork.pdf

Hier stellen wir uns die Eingabe in einen Algorithmus als "Datenbank" vor, und der Algorithmus ist "unsicher", wenn er zu viele Informationen über die Daten einer Person in der Datenbank enthält. Ein Algorithmus ist -differenziell privat, wenn die Ausgabe des Algorithmus nicht stark von einer Eingabe abhängt: Insbesondere sollte das Ändern eines einzelnen Eintrags in der Eingabedatenbank die Wahrscheinlichkeit einer Ausgabe des Algorithmus nur um höchstens ein ändern Faktor.e ϵϵeϵ

Wenn Sie einen Algorithmus privat machen, ist dies natürlich weniger nützlich: Ein differenziell privater Algorithmus erzeugt Ausgaben, die überhaupt nicht von den Eingaben abhängen! Es stellt sich jedoch heraus, dass Sie versuchen können, den Kompromiss zwischen Datenschutz und Nutzen sorgfältig auszugleichen, und sehr private Algorithmen erhalten können, die dennoch nicht trivial nützlich sind.0

Aaron Roth
quelle
14

Auf verschiedener Weise:

Ross Snider
quelle
Ich glaube ehrlich gesagt nicht, dass Sie jemals eine Sicherheitsanfälligkeit gefunden, einen einzelnen Code gepatcht oder sogar das Innenleben einer realen Sicherheitsanfälligkeit gesehen haben.
Der Turm
8
Mit OllyDbg habe ich meine gdi-DLL gepatcht, um die (zweite) Cursor-Sicherheitslücke (offensichtlich ohne Quellcode) vor dem Microsoft-Patch am Dienstag zu beheben. Wieder mit OllyDbg habe ich einen Closed-Source-Emulator gepatcht, um ihn für (peinlich) einen Pokemon-Wettbewerb betrügerisch zu machen. Ich habe einen 0-Tag in einem Webcam-Projekt gefunden und bei einer großen Anzahl von Kriegsspielen (einschließlich Blacksun, für das ASLR und PaX aktiviert sind) einigermaßen gute Ergebnisse erzielt. Ich werde einige der schändlicheren Dinge, die ich getan habe, nicht erwähnen ... Achselzucken; Warum sollte es wichtig sein, ob ich hatte oder nicht? Bitte nicht flammen.
Ross Snider
13
@ The Rook: Wenn Sie glauben, dass Ross 'Liste wenig mit der tatsächlichen Praxis der Software-Sicherheit zu tun hat, dann sagen Sie es. Vielleicht wäre es sogar hilfreich, einige Beispiele zu nennen oder eine Antwort auf Ihre eigenen Details hinzuzufügen, wie weit die TCS-Sicherheitsforschung von der tatsächlichen Sicherheitspraxis entfernt ist (was meiner Meinung nach sehr interessant zu lesen wäre). Aber es besteht keine Notwendigkeit, Ross zu erniedrigen.
Joshua Grochow
10

Es gibt eine Menge realer Motivation für das Studium von Streaming-Algorithmen, die aus der Erkennung von Netzwerkeinbrüchen stammen. Das folgende Papier verwendet Streaming-Algorithmen für die empirische Entropie, um Anomolien in Ihrem Netzwerkverkehr zu erkennen.

Yu Gu, Andrew McCallum und Don Towsley. Erkennen von Anomalien im Netzwerkverkehr mithilfe der maximalen Entropieschätzung. In IMC '05: Proceedings der 5. ACM SIGCOMM-Konferenz zur Internetmessung, Seiten 1–6, 2005

Joshua Brody
quelle
8

Im Gegensatz zu den anderen Antworten handelt es sich hier eher um "Dinge, über die wir uns Sorgen machen sollten, wenn wir sagen, dass etwas" nachweislich sicher "ist", als um Orte, an denen TCS für die Sicherheit verwendet wurde. Damit wird die erste Frage der Sicherheitsbedenken bei der Arbeit mit der Theorie angesprochen.

Wie Hacker sagen, sind theoretische Ergebnisse oft tangential zur realen Sicherheit. Diese Art von Argumentation wurde von Alfred Menezes und Neal Koblitz in ihrer Reihe von " Another Look " -Papieren theoretischer, wissenschaftlicher und präziser formuliert (Warnung: Die Website scheint mir ein wenig konfrontativ zu sein, aber ich denke, die Grundidee, Annahmen in Frage zu stellen ist sehr wichtig). Sie weisen auf Schwachstellen bei Standardannahmen in der Kryptographie hin, selbst in wegweisenden Arbeiten.

Einige Beispiele (Zitieren / Paraphrasieren einiger Punkte von ihrer Site):

  1. Ein Sicherheitssatz ist bedingt - er setzt die Unlösbarkeit eines mathematischen Problems voraus.

  2. Oft wird die Unlösbarkeitsannahme für ein kompliziertes und erfundenes Problem gemacht: In einigen Fällen entspricht das Problem trivial dem Kryptoanalyseproblem für das Protokoll, dessen Sicherheit "bewiesen" wird.

  3. Manchmal hat ein Proof eine große Dichtheitslücke, aber es werden immer noch Parametergrößen empfohlen, als ob der Proof dicht gewesen wäre. In solchen Fällen gibt der Beweis normalerweise eine nutzlose Untergrenze für die Laufzeit eines erfolgreichen Angriffs. Darüber hinaus bietet ein asymptotisches Ergebnis nicht unbedingt eine Sicherheit für Parameter in dem in der Praxis verwendeten Bereich.

  4. Ein Sicherheitssatz verwendet ein bestimmtes Sicherheitsmodell. Bestimmte Angriffe - insbesondere Seitenkanalangriffe - sind sehr schwer zu modellieren, und die vorgeschlagenen Modelle sind absolut unzureichend.

Artem Kaznatcheev
quelle
6

Theoremprüfer wurden in gewissem Umfang verwendet, um die Richtigkeit von Software, Hardware und Protokollen zu beweisen. Siehe zum Beispiel hier oder hier .

Das Problem, dass Daten auf unerwünschte Weise durch Programme fließen (und somit ein potenzielles Leck verursachen), wurde theoretisch unter Verwendung des Begriffs (Nicht-) Interferenz modelliert. erhalten Zeiger hier .

Raphael
quelle
3

Entscheidbarkeit ist ein zentrales Anliegen in der Programmiersprachenforschung. Das heißt, es werden große Anstrengungen unternommen, um Programmiersprachen zu erstellen, die nur Code akzeptieren, der bestimmte Eigenschaften erfüllt. Typische statische Sprachen bieten nur schwache Garantien, z. B. das Ablehnen eines Programms, wenn bestimmte Methoden nicht vorhanden sind. Stellen Sie sich jedoch vor, die Sprache könnte auch Programme ausgeben, die beispielsweise Mutexe nicht ordnungsgemäß verwenden oder versuchen, über das Ende der Speicherbereiche hinaus zu lesen. Es ist klar, dass Entscheidbarkeitsprobleme schnell auftreten (einfachstes Szenario: Geben Sie an, dass Ihr Compiler nur das Beenden von Programmen akzeptieren soll), und es gibt sicherlich Effizienzprobleme (der ML-Typprüfer hat doppelt exponentielle Fälle).

In jedem Fall ist die PL-Forschungsgemeinschaft sehr an Sicherheit interessiert (vertrauen Sie darauf, dass Ihr Browser beliebigen Fremdcode ausführt?!), Und ihre Fragen führen zu vielen Fragen der klassischen CS-Theorie.

Matus
quelle
Eine richtige Hochsprache (lesen: außer C [++]) gibt dem Programmierer keine Kontrolle über den Speicherzugriff, daher würde ich dieses Problem als gelöst betrachten.
Raphael
@Raphael: Da in C und C ++ immer noch eine große Menge an Software geschrieben ist, kann dieses Problem nicht einfach als gelöst betrachtet werden. Darüber hinaus stecken Techniken zur Bekämpfung von Code-Injection-Angriffen auf Javascript beispielsweise noch in den Kinderschuhen. Es gibt viel zu tun.
Dave Clarke
1
Die Tatsache, dass bestimmte Umgebungen vorhandene Lösungen ignorieren (manchmal aus guten Gründen), macht das Problem (hier: Zugriff auf verbotene Speicheradressen) nicht weniger gelöst. Einige Dinge, die schwer zu überprüfen sind, können durch geeignete Invarianten leicht umgangen werden. Sie können beispielsweise von Ihrem Programmierer (siehe Isabelle / HOL) einen formellen Kündigungsnachweis verlangen.
Raphael