Lehrplan: Logische / Formale Methoden in der Sicherheit

22

Gegenwärtig unterrichte ich einen kleinen Kurs (vier zweistündige Vorlesungen auf der Masters-Ebene) über logische Methoden in der Sicherheit , obwohl der Titel formale Methoden in der Sicherheit geeigneter sein könnte. Es werden kurz die folgenden Themen behandelt (mit den zugehörigen logischen Methoden):

  • Digital Rights Management und Policy Enforcement (allgemeine Formalisierung, modale Logik, Durchsetzung über Automaten)

  • Nachweiscode und Nachweisauthentifizierung (Beweistheorie, logische Systeme, Curry-Howard-Isomorphismus, Verifikation)

  • Zugriffskontrolle (nicht-klassische Logik, Beweistheorie)

  • Stack Inspection (Programmiersprachensemantik, Kontextäquivalenz, Bisimulation)

Natürlich hat der Kurs mehrere Ziele, von denen eines potenzielle Doktoranden anzieht.

In den kommenden Jahren kann der Kurs zu einem regulären Kurs erweitert werden, der mehr Inhalte benötigt. Angesichts der Tatsache, dass der Hintergrund der Menschen hier ganz anders ist als der meine, würde ich gerne wissen, welche Inhalte Sie in einen solchen Kurs einbeziehen würden.

lo.logic cr.crypto-security teaching security formal-methods Dave Clarke
quelle

Antworten:

15

Ich schlage vor, die Schüler mit den folgenden Logik vertraut zu machen:

  • Epistemische Logik: Wird verwendet, um das Wissen verschiedener am Protokoll beteiligter Parteien zu modellieren und zu beweisen, dass ein Gegner kein Geheimnis erkennen kann.
  • BAN-Logik: Eine alte Logik zum Prüfen verschiedener Eigenschaften von Authentifizierungsprotokollen. (Andere Glaubenslogiken sind ebenfalls angemessen.)
  • Logik für Übergangssysteme: Dies umfasst Logik wie LTL, CTL und LTL *. (Solche Logiken wirken auf Kripke-ähnliche Modelle des Protokolls.)
  • Prozessalgebren: Verschiedene Prozessalgebren, wie Spi-Calculus (oder CSP ) und das sicherheitsrelevante Tool Casper, eignen sich zur Modellierung von Sicherheitsprotokollen.
  • Die Einführung von Tools wie AVISPA von NuSMV ist sehr nützlich.
  • Ich empfehle auch die formale Korrektheit von Sicherheitsprotokollen als eines der Lehrbücher.

Ein Freund von mir, Morteza Amini , hat kürzlich seinen Ph.D. zur Modellierung der Zugriffskontrolle mit Logik. Er entwickelte eine neue Logik, mit dem Namen , das steht für „Multi-Behörde deontische Logik und Beschreibung Logik.“ Wie der Name schon sagt, werden zwei nicht-klassische Logiken (deontische Logik + Beschreibungslogik) kombiniert, um zu entscheiden, ob eine Entität Zugriff auf ein Objekt hat. Wenn Sie möchten, kann ich ihn ermutigen, weitere Informationen bereitzustellen.MA(DL)2

MS Dousti
quelle
Vielen Dank, Sadeq. In früheren Jahren habe ich Epistemic Logic in meiner Einführung in Modal Logic für den Kurs behandelt, aber ich habe es in diesem Jahr fallen gelassen. Schüler wählen oft BAN-Logik für ein Aufsatzthema. Die anderen Vorschläge sind sehr nützlich, insbesondere die Tools, die immer mögliche studentische Aufgaben vorschlagen.
Dave Clarke
@ Dave: Freut mich das zu hören! Ich habe einmal an einem hervorragenden Schnellkurs (ca. 3 Stunden) über "Epistemische Logik für Sicherheitsprotokolle" von Dr. Ramaznian teilgenommen. Die Präsentation finden Sie hier: ifile.it/xljn9s8/EpistemicLogic.rar . Ich schlage vor, dass Sie sich das ansehen, bevor Sie das Thema ganz streichen.
MS Dousti
Danke für den Link. Epistemic Logic wurde nicht vollständig entfernt. Dieses Jahr hat es einfach nicht gepasst.
Dave Clarke
12

Vor einigen Jahren gab es einen Lesekurs bei Carnegie Mellon, Languages ​​and Logics for Security , in dem versucht wurde, einen Teil der Literatur zu Authentifizierung, Autorisierung, Informationsfluss, Protokollkalkülen, Schutz und Vertrauensmanagement zu durchsuchen. Die Webseite des Kurses enthält Folien für die von uns besprochenen Artikel sowie eine weitere Referenzliste für jedes Thema. Insbesondere der Informationsfluss kann einen Blick auf die von Ihnen aufgeführten Themen wert sein.

Der Lehrplan für Anupam Dattas Kurs Grundlagen der Sicherheit und des Datenschutzes ist ebenfalls relevant.

Rob Simmons
quelle
Vielen Dank, Rob. Tatsächlich habe ich diese beiden Seiten verwendet, als ich den ursprünglichen Kursinhalt entworfen habe.
Dave Clarke
Aah. Na dann denke ich, dass sein zusätzlicher Nutzen für Sie begrenzt ist! Hoffentlich finden es auch andere nützlich :).
Rob Simmons
10

Robs Antwort erinnerte mich an eine ähnliche Cornell-Lesegruppe, die Michael Clarkson einige Jahre lang organisiert hatte: die Cornell Security Discussion Group . Vielleicht lohnt es sich, dort nach ein paar Zeitungen zu suchen.

Mark Reitblatt
quelle
6

Ich bin nicht sicher, was Sie unter dem Wort "Verifikation" verstecken, also versuche ich es. Vielleicht können Sie etwas über die quantitative Verifizierung von Markov-Entscheidungsprozessen und die Verwendung probabilistischer zeitlicher Logik (pLTL und PCTL) hinzufügen. In diesem Framework haben Sie eine ziemlich gute Möglichkeit, Gegner zu modellieren, Eigenschaften auszudrücken und es gibt einfach zu verwendende Überprüfungswerkzeuge ( z. B. PRISM ).

Sylvain Peyronnet
quelle
Interessant. Kennen Sie Sicherheitsanwendungen von PRISM oder von diesen Logiken?
Dave Clarke
In den Fallstudien ( prismmodelchecker.org/casestudies/index.php ) gibt es einige Beispiele in Bezug auf Sicherheit. Die meisten von ihnen sind MDP, aber es geht eher um die Sicherheit von Protokollen als um die Sicherheit von Implementierungen.
Sylvain Peyronnet
1

Ein Vortrag über beweisbare Sicherheit könnte interessant sein, insbesondere unter Verwendung der Spieltheorie. Ich denke, dass die Kapitel 8 und 25 des Buches von Nisan et al. Über algorithmische Spieltheorie eine gute Grundlage bieten könnten.

Ich würde auch eine kurze Beschreibung der bestehenden Sicherheitsstandards wie ITSEC / TCSEC und Common Criteria hinzufügen. Es ist immer gut darauf hinzuweisen, dass es zur Erreichung der höchsten Stufe der Common Criteria erforderlich ist, ein System formal zu verifizieren, zu entwerfen und zu testen.

Charles
quelle