Resumen

La técnica de comprobación de modelos (MC) de lógica temporal de intervalos (ITL) mejora la capacidad de los sistemas de detección de intrusos (IDS) para detectar ataques concurrentes debido a la gran capacidad expresiva de la ITL. Sin embargo, una fórmula ITL adolece de dificultad en la descripción de las restricciones temporales entre las distintas acciones de un mismo ataque. Para resolver este problema, formalizamos una nueva lógica temporal de intervalos en tiempo real: la lógica de firma de ataques en tiempo real (RASL). Basándonos en esta nueva lógica, proponemos un algoritmo de comprobación de modelos RASL. Además, utilizamos fórmulas RASL para describir firmas de ataque y empleamos autómatas temporales discretos para crear un registro de auditoría. Como resultado, el algoritmo de comprobación de modelos RASL puede utilizarse para verificar automáticamente si los autómatas satisfacen las fórmulas, es decir, si el registro de auditoría coincide con las firmas de ataque. Los experimentos de simulación muestran que el nuevo enfoque mejora eficazmente el poder de detección de los métodos de detección de intrusiones basados en MC para una serie de ataques telnet, ataques p-trace y los otros dieciséis tipos de ataques. Y estos experimentos indican que el nuevo algoritmo puede encontrar varios tipos de ataques en tiempo real, mientras que los enfoques existentes de detección de intrusiones basados en MC no pueden hacerlo.

• Materias:Matemáticas Análisis Matemático Álgebra Ingeniería Matemática aplicada Lógica matemática
• Subjects:mathematics Mathematical Analysis Algebra Engineering Applied Mathematics Mathematical logic
• Palabras claves:algoritmo de comprobación de modelos rasl, firmas de ataques, lógica temporal, lógica de firmas de ataques temporales, enfoques de detección de intrusos, métodos de detección de intrusos, sistemas de detección de intrusos, fuerte poder expresivo, itl, autómatas
• Keywords:rasl model checking algorithm, attack signatures, temporal logic, time attack signature logic, intrusion detection approaches, intrusion detection methods, intrusion detection systems, strong expressive power, itl, automata