Revisión de la descripción general del protocolo de comunicación SCHC y perfil Sigfox utilizando Model Checking

Abstract

La Internet de las Cosas o Internet of Things (IoT) permite conectar a Internet a dispositivos que no fueron originalmente diseñados para estarlo, permitiendo que estos puedan compartir datos a la nube. En este contexto, se crean las redes de bajo consumo y gran cobertura llamadas redes LPWAN de su definición en inglés Low Power Wide Area Networks. Estas redes buscan conectar dispositivos IoT de bajo consumo en grandes áreas geográficas. Para cumplir con una gran cobertura, las redes LPWAN deben sacrificar latencia y tasa de datos, por lo tanto, en estas redes se tiene una gran latencia, una baja tasa de datos y una baja unidad de transmisión máxima (MTU), restringiendo el número y tamaño de mensajes que un dispositivo puede enviar por estas redes. Debido a la restricción de MTU las redes LPWAN no soportan de forma nativa el direccionamiento IP, ya que esto implicaría un gran uso de memoria en los dispositivos y una mayor tasa de datos en la red. La Internet Engineering Task Foce (IETF) diseña y publica en 2020 en el documento RFC 8724 el protocolo Static Context Header Compression and Fragmentation (SCHC), el cual comprime y fragmenta encabezados de paquetes IPv6 para poder ser enviados en redes LPWAN, permitiendo así que dispositivos de bajo consumo conectados a redes LPWAN puedan enviar paquetes IPv6 a pesar de las restricciones que estas redes tienen. Esta tesis presenta la revisión del protocolo SCHC mediante la técnica basada en modelos Model Checking. Se presentan los modelos para los tres modos de transmisión del protocolo. La revisión busca mostrar que los modos de transmisión necesitan ser más específicos para evitar que el protocolo tenga vulnerabilidades y errores.