1 Especificación y verificación de routers software (12 Créditos) J. Guadalupe Ramos Díaz Tutor: Dr. Germán Vidal DOCTORADO EN PROGRAMACIÓN DECLARATIVA E INGENIERÍA DE LA PROGRAMACIÓN DSIC-PLIS-ELP-MIST

2 2 1. Currículum 1.1 Formación 1.2 Materias impartidas en México 1.3 Participación en proyectos 1.4 Ponencias en Congresos Nacionales 2. Docencia 3. Investigación 3.1 Definición de router 3.2 Objetivo 3.3 Anotaciones 3.4 Especificación de circuitos 3.5 Lenguaje anfitrión 3.6 Solución 4. Conclusiones 5. Trabajos futuros 6. Plan de trabajo Agenda :

3 3 Maestría en Ciencias Computacionales I. T. León (1998) Adiestramiento en Investigación Tecnológica Instituto de Investigaciones Eléctricas (Cuernavaca, México, 1995) Ingeniería en Sistemas Computacionales I. T. Morelia (1994) 1. Currículum: Formación

4 4 Programación Programación de sistemas Programación para Internet Administración de archivos Redes de área local Sistemas abiertos Tópicos de redes Teleproceso Graficación 1. Currículum: Materias impartidas

5 5 1. Currículum: Proyectos de I+D Sistema de graficación para QNX Instituto de Investigaciones Eléctricas Asesor de proyectos de creatividad en etapas nacionales – –Servidor genérico P2P – –Sistema de monitoreo y control remoto por Internet – –Aplicaciones P2P

6 6 1. Currículum: Ponencias en Congresos Nacionales Intermediario para sistemas de información distribuida Congreso de Ing. en Sist. Computacionales e Informática (I.T.Tuxtla Gutiérrez, Chiapas): CISCI’02 Propuesta de middleware para aplicaciones P2P Simposium Intertecnológico de Ciencias Computacionales: SICI’01 Servidor genérico para aplicaciones P2P 1er. Congreso Nacional de Calidad en la Educación Superior Tecnológica: CNCEST’00

7 7 2. Etapa de Docencia MateriaCréditos Ingeniería de requisitos O.O.5 Bases de datos avanzadas4 Tecnología software para ambientes web5 Fundamentos lógicos de la Ingeniería de Software 4 Ingeniería de Software automática4

8 8 3. Investigación: Definición cabecera Carga útil Paquete Router Dirección destino Puertos de salida Estructura de datos de rutas Red destino Puerto Tabla de encaminamiento 65.0.0.0/8 128.9.0.0/16 149.12.0.0/19 3 1 2 +Protocolos de encaminamiento Routers extensibles Seguridad Políticas QoS Direcciones Evolución

9 9 3. Investigación: Definición Ejecución en un PC: Enchufes [Decasper et al. 1998], ETH Zurich & U. Washington Enchufes [Decasper et al. 1998], ETH Zurich & U. Washington Scout [Peterson et al. 1999], U. Arizona, U. Princeton Scout [Peterson et al. 1999], U. Arizona, U. Princeton Click [Kohler et al. 1999], MIT Click [Kohler et al. 1999], MIT Ejecución en un PC + Procesador de Red: VHDL + FPGA [Lee et al. 1999], I.P. Virginia VHDL + FPGA [Lee et al. 1999], I.P. Virginia Intel IXP1200 + Ensamblador [Spalink et al. 2001], U. Princeton Intel IXP1200 + Ensamblador [Spalink et al. 2001], U. Princeton NPClick + Intel IXP1200 [Shah et al. 2003], U. Berkeley NPClick + Intel IXP1200 [Shah et al. 2003], U. Berkeley Router Modular Click Forma de grafos : [Spalink et al., 2001] Existen dos tipos: [Spalink et al., 2001]

10 10 3. Investigación: Objetivo Ventajas claras de los routers extensibles (tema actual) respecto a los routers hardware Actividad en una red  Click debería tener un y verificación de routers software, etc. Actividad crucial en una red  Click debería tener un entorno para especificación y verificación de routers software, etc. ¡No lo tiene! Objetivo : Desarrollar un lenguaje de dominio específico sobre un lenguaje declarativo (multi-paradigma) para la especificación y verificación de routers Click

11 11 3. Investigación: Anotaciones No existen antecedentes en la literatura del uso de un lenguaje declarativo para la especificación de routers software Existe un campo relacionado: especificación y verificación de hardware Explotamos la relación circuitos grafos Click Anfitrión Librería Dominio Un lenguaje declarativo empotrado es una librería que se incorpora a un lenguaje ya existente Librería = Lenguaje de dominio específico

12 12 3. Investigación: Especificación de circuitos Especificación del lenguaje empotrado: Lava [Claessen, 2001] Apoyado por Xilinx Inc. halfAdd (a, b) = (sum, carry) where sum = xor (a, b) carry = and (a, b) type Signal = [Bool] and :: (Signal,Signal)->Signal xor :: (Signal,Signal)->Signal Librería

13 13 3. Investigación: Especificación de circuitos sham1 (cmd, destReg, srcRegA, srcRegB) = (destReg’, aluOutput’) where (aluInputA, aluInputB) = regFile srcRegA srcRegB(destReg’,aluOutput’) aluOutput = alu cmd aluInputA aluInputB aluOutput’ = delay 0 aluOutput destReg’ = delay R0 destReg Especificación del lenguaje empotrado Hawk [Matthews, et al., 2000] Apoyado por Intel Inc.

14 14 3. Investigación: Lenguaje anfitrión Curry es una extensión conservativa de Haskell (base de Lava / Hawk) con características de la programación lógica Curry Proporciona el entorno apropiado para practicar verificación, simulación y análisis Permitirá adaptar inmediatamente Lava y Hawk Curry = lógica + funcional + concurrente + distribuida + OO = multi-paradigma

15 15 3. Investigación: Solución FromDevice(eth0)->Print (“Paq:”)->Discard type Packet = [ Char ] Caso Simple: fromDevice :: Int -> Packet fromDevice _ = newPacket print :: (String, Packet) -> Packet print (s, px) = let p= s++px in p discard :: Packet->Int discard p = 0 ->- ( ->- ) :: (a->b) -> ( b->c) -> a -> c (element1 ->- element2) inp = let mid = element1 inp in element2 mid Conector de orden superior ->- (fromDevice ->- discard) 1

16 16 3. Investigación: Solución Caso a modelar: : Principal problema propio a un router: La conexión = ¿funciones? o ¿conectores? o ¿condicionales?

17 17 3. Investigación: Solución router pkin = out where (pk, pto) = classifier pkin pk2 = if pto==2 then paint pk 2 else GOTO... Características: Problema de salidas múltiples y condicionales Poco declarativo En Click no hay condicionales

18 18 3. Investigación: Solución router:: Event -> Event router inp = out where outclassif = classifier inp out = routerBranch outclassif routerBranch (pk,0) = arpResponder (pk,0) routerBranch (pk,1) = arpQuerier (pk,1) routerBranch (pk,2) = out where st1 = paint (pk,2) 1111 st2 = strip st1 14 st3 = checkIPHeader st2 out = getIPAddress st3 type Event = (Packet, Puerto) :Escritura de router mas cercana a Click Características : Incorporación de abstracción de eventos Se aprovecha pattern matching para dar inteligencia a los elementos

19 19 4. Conclusiones Los routers extensibles son un tema de actualidad que madurará y en el que Click sobresale La especificación y verificación formal son de gran importancia para las empresas de hardware y ya hay esfuerzos basados en el uso de lenguajes declarativos. Curry podría tener un lugar ventajoso gracias a sus características multi-paradigma Se han comprobado las ventajas de escribir un lenguaje empotrado con respecto la creación de un lenguaje nuevo (con intérprete, compilador, herramientas de verificación... )

20 20 5. Trabajos futuros Enlazar nuestro lenguaje con Click: Traductor de especificaciones Curry a Click (colaboración con E. Kohler, MIT) Especificar los 242 elementos Click Definir e implementar técnicas de análisis, verificación, etc. (concretas al dominio del problema) – –Propiedades de un router: No puede haber ciclos infinitos, verificar que a una entrada hay una salida, excepto con paquetes vencidos El paquete sólo puede ser modificado en ciertos campos Para todo paquete debe haber una ruta de encaminamiento, etc.

21 21 6. Plan de trabajo Publicación PROLE’03 (Terceras Jornadas sobre Lenguajes de Programación ) TESIS: Especificación (presente) Y verificación (futuro) de routers software Metodología de trabajo: –Contacto regular vía email –Visita a la UPV –Asistencia a congresos Proyecto de I+D centrado en el tema

22 22...