Plan de estudios: métodos lógicos / formales en seguridad

22

Actualmente doy un pequeño curso (cuatro conferencias de dos horas a nivel de maestría) sobre Métodos lógicos en seguridad , aunque el título Métodos formales en seguridad podría ser más adecuado. Cubre brevemente los siguientes temas (con métodos lógicos asociados):

  • Gestión de derechos digitales y aplicación de políticas (formalización general, lógica modal, aplicación a través de autómatas)

  • Código de prueba y autenticación de prueba (teoría de prueba, sistemas lógicos, isomorfismo de Curry-Howard, verificación)

  • Control de acceso (lógicas no clásicas, teoría de la prueba)

  • Inspección de pila (semántica de lenguaje de programación, equivalencia contextual, bisimulación)

Naturalmente, el curso tiene múltiples objetivos, donde uno de ellos es atraer a potenciales estudiantes graduados.

En los próximos años, el curso puede ampliarse a un curso regular, que necesitará más contenido. Dado que los antecedentes de las personas aquí son bastante diferentes a los míos, me gustaría saber qué contenido incluirías en dicho curso.

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

Respuestas:

15

Sugiero familiarizar a los estudiantes con las siguientes lógicas:

  • Lógica epistémica: se utiliza para modelar el conocimiento de varias partes que participan en el protocolo y demostrar que un adversario no puede obtener conocimiento de algún secreto.
  • Lógica BAN: Una lógica antigua para probar varias propiedades de los protocolos de autenticación. (Otras lógicas de creencias también son apropiadas).
  • Lógicas para sistemas de transición: esto incluye lógicas como LTL, CTL y LTL *. (Dichas lógicas actúan sobre modelos de protocolo similares a Kripke).
  • Álgebras de procesos: varias álgebras de procesos, como Spi-calculus (o CSP , y su herramienta relacionada con la seguridad, Casper ) son útiles para modelar protocolos de seguridad.
  • La introducción de herramientas como AVISPA de NuSMV son muy útiles.
  • También sugiero la corrección formal de los protocolos de seguridad como uno de los libros de texto del curso.

MA(DL)2

MS Dousti
fuente
Gracias sadeq En años anteriores, cubrí Epistemic Logic en mi introducción a Modal Logic para el curso, pero lo dejé este año. Los estudiantes suelen elegir la lógica BAN para un tema de ensayo. Las otras sugerencias son muy útiles, especialmente las herramientas, que siempre sugieren posibles tareas de los estudiantes.
Dave Clarke el
@Dave: ¡Me alegra escuchar eso! Una vez participé en un excelente curso intensivo (~ 3 horas) sobre "Lógica epistémica para protocolos de seguridad" del Dr. Ramaznian. La presentación se puede encontrar aquí: ifile.it/xljn9s8/EpistemicLogic.rar . Sugiero echarle un vistazo a eso, antes de dejar el tema por completo.
MS Dousti
Gracias por el enlace. La lógica epistémica no se ha descartado por completo; Simplemente no encaja este año.
Dave Clarke
12

Hubo un curso de lectura en Carnegie Mellon hace unos años, Idiomas y lógica para la seguridad , que trató de examinar parte de la literatura sobre autenticación, autorización, flujo de información, cálculo de protocolos, protección y gestión de confianza; la página web del curso tiene diapositivas para los documentos que discutimos, así como una lista adicional de referencias para cada tema. El flujo de información en particular podría ser algo que vale la pena echarle un vistazo en relación con los temas que enumeró.

El plan de estudios para el curso Fundamentos de seguridad y privacidad de Anupam Datta también es relevante.

Rob Simmons
fuente
Gracias Rob De hecho, utilicé estas dos páginas cuando diseñé el contenido original del curso.
Dave Clarke el
Aah Bueno, entonces supongo que su utilidad adicional es limitada. Esperemos que otros lo encuentren útil también :).
Rob Simmons el
10

La respuesta de Rob me recordó a un grupo similar de lectura de Cornell que Michael Clarkson organizó durante algunos años: el Grupo de discusión sobre seguridad de Cornell . Puede valer la pena pasar por allí para algunos papeles.

Mark Reitblatt
fuente
6

No estoy seguro de lo que ocultas bajo la palabra "verificación", así que lo intento. Tal vez pueda agregar algo sobre la verificación cuantitativa de los procesos de decisión de Markov y el uso de la lógica temporal probabilística (pLTL y PCTL). En este marco, tiene una forma bastante buena de modelar adversarios, de expresar propiedades y existen herramientas de verificación fáciles de usar ( PRISM, por ejemplo).

Sylvain Peyronnet
fuente
Interesante. ¿Conoces alguna aplicación de seguridad de PRISM o de estas lógicas?
Dave Clarke el
En los estudios de caso ( prismmodelchecker.org/casestudies/index.php ), hay algunos ejemplos relacionados con la seguridad. La mayoría de ellos son MDP, pero se trata más de la seguridad de los protocolos que de la seguridad de las implementaciones.
Sylvain Peyronnet
1

Una conferencia sobre Provable Security podría ser interesante, en particular utilizando Game Theory. Creo que los Capítulos 8 y 25 del libro de Nisan et al sobre Algorithmic Game Theory podrían proporcionar una buena base.

También incluiría una breve descripción de los estándares de seguridad existentes, como ITSEC / TCSEC y los Criterios comunes. Siempre es bueno señalar que para alcanzar el nivel más alto de los Criterios comunes, es necesario verificar formalmente , diseñar y probar un sistema.

Charles
fuente