Curriculum: Méthodes logiques / formelles en sécurité

Actuellement, j'enseigne un petit cours (quatre conférences de deux heures au niveau Master) sur les méthodes logiques en sécurité , bien que le titre Méthodes formelles en sécurité soit peut-être plus approprié. Il couvre brièvement les sujets suivants (avec les méthodes logiques associées):

• Gestion des droits numériques et application des politiques (formalisation générale, logique modale, application via des automates)

• Code de preuve et authentification de preuve (théorie de la preuve, systèmes logiques, isomorphisme de Curry-Howard, vérification)

• Contrôle d'accès (logiques non classiques, théorie de la preuve)

• Inspection de pile (sémantique du langage de programmation, équivalence contextuelle, bisimulation)

Naturellement, le cours a plusieurs objectifs, dont l'un attire des étudiants diplômés potentiels.

Dans les années à venir, le cours pourrait être étendu à un cours régulier, qui nécessitera plus de contenu. Étant donné que les antécédents des gens ici sont très différents des miens, j'aimerais savoir quel contenu vous incluriez dans un tel cours.

Je suggère de familiariser les étudiants avec les logiques suivantes:

• Logique épistémique: utilisée pour modéliser les connaissances des différentes parties participant au protocole et prouver qu'un adversaire ne peut pas connaître un secret.
• Logique BAN: une ancienne logique pour prouver diverses propriétés des protocoles d'authentification. (D'autres logiques de croyance sont également appropriées.)
• Logiques pour les systèmes de transition: cela inclut les logiques comme LTL, CTL et LTL *. (ces logiques agissent sur des modèles de protocole de type Kripke.)
• Algèbres de processus: plusieurs algèbres de processus, comme le Spi-calcul (ou CSP , et son outil lié à la sécurité, Casper ) sont utiles pour la modélisation des protocoles de sécurité.
• L'introduction d'outils comme AVISPA de NuSMV est très utile.
• Je suggère également l' exactitude formelle des protocoles de sécurité comme l'un des manuels de cours.

Un de mes amis, Morteza Amini , a récemment obtenu son doctorat. sur la modélisation du contrôle d'accès avec la logique. Il a conçu une nouvelle logique, nommée , qui signifie «logique déontique multi-autorité et logique de description». Comme son nom l'indique, il combine deux logiques non classiques (logique déontique + logique de description) pour décider si une entité a accès à un objet. Si vous le souhaitez, je peux l'encourager à fournir plus d'informations.$MA(DL)^2$

Il y a quelques années, un cours de lecture à Carnegie Mellon, Langues et logiques pour la sécurité , a tenté d'étudier une partie de la littérature sur l'authentification, l'autorisation, le flux d'informations, les calculs de protocole, la protection et la gestion de la confiance; la page Web du cours contient des diapositives pour les articles dont nous avons discuté ainsi qu'une liste supplémentaire de références pour chaque sujet. Le flux d'informations en particulier pourrait être intéressant à examiner par rapport aux sujets que vous avez énumérés.

Le programme du cours Anupam Datta's Foundations of Security and Privacy est également pertinent.

La réponse de Rob m'a rappelé un groupe de lecture Cornell similaire que Michael Clarkson a organisé pendant quelques années: Cornell Security Discussion Group . Cela pourrait valoir la peine de parcourir certains documents.

Je ne suis pas sûr de ce que vous cachez sous le mot "vérification", alors j'essaie. Vous pouvez peut-être ajouter quelque chose sur la vérification quantitative des processus de décision de Markov et l'utilisation de la logique temporelle probabiliste (pLTL et PCTL). Dans ce cadre, vous avez une assez bonne façon de modéliser les adversaires, d'exprimer des propriétés et il existe des outils de vérification faciles à utiliser ( PRISM par exemple).

Vous pouvez également consulter le cours de deuxième cycle sur les protocoles de sécurité à Paris (le texte est principalement en français):

http://mpri.master.univ-paris7.fr/C-2-30.html

Une conférence sur Provable Security pourrait être intéressante, en particulier en utilisant la théorie des jeux. Je pense que les chapitres 8 et 25 du livre de Nisan et al sur la théorie des jeux algorithmiques pourraient fournir une bonne base.

Je voudrais également inclure une brève description des normes de sécurité / sûreté existantes, telles que ITSEC / TCSEC et les Critères communs. Il est toujours bon de souligner que pour atteindre le plus haut niveau des Critères communs, il est nécessaire de vérifier, concevoir et tester formellement un système.