Publicación:
Implementación de CoAP verificada formalmente en SPARK/Ada

Vista sencilla de ítem
dc.contributor.authorGómez Rojo, Manuel
dc.contributor.directorPastor Vargas, Rafael
dc.date.accessioned2026-03-19T12:37:19Z
dc.date.available2026-03-19T12:37:19Z
dc.date.issued2026-03-01
dc.description.abstractEste Trabajo Fin de Máster aborda la verificación formal de software como medio de mejorar la ciberseguridad en el ámbito de los dispositivos IoT. Con el objetivo de comprobar la viabilidad y conveniencia de este enfoque, se aplica un proceso de desarrollo seguro en la implementación del protocolo Constrained Application Protocol (CoAP), basándose principalmente en la verificación formal del software escrito en el lenguaje SPARK/Ada. Como parte de la introducción a la verificación formal, se compara este lenguaje con otros que poseen esta característica, como Frama-C o Dafny. También se realiza una breve descripción del protocolo CoAP. En su implementación, se emplean herramientas como GNATprove para demostrar la corrección del código, RecordFlux para la especificación y generación de parsers verificables, y WolfSSL para la seguridad con DTLS. Finalmente, se realiza una validación mediante pruebas de interoperabilidad con servidores CoAP y dispositivos IoT comerciales como el gateway TRÅDFRI. Las conclusiones destacan la viabilidad de la verificación formal para mejorar la ciberseguridad en IoT, pese a su mayor costo inicial.es
dc.description.abstractThis Master’s Thesis addresses formal software verification as a means to improve cybersecurity in the field of IoT devices. To assess the feasibility and benefits of this approach, a secure development process is applied in the implementation of the Constrained Application Protocol (CoAP), based primarily on the formal verification of software written in the SPARK/Ada language. As part of the introduction to formal verification, this language is compared with others that offer such capabilities, such as Frama-C and Dafny. An brief description of the CoAP protocol is also provided. In its implementation, tools such as GNATprove are employed to demonstrate code correctness, RecordFlux for the specification and generation of verifiable parsers, and WolfSSL for DTLS security. Finally, validation is carried out through interoperability tests with CoAP servers and commercial IoT devices such as the TRÅDFRI gateway. The conclusions underscore the viability of formal verification for enhancing IoT cybersecurity, despite its higher initial cost.en
dc.description.provenanceMade available in DSpace on 2026-03-19T12:37:19Z (GMT). No. of bitstreams: 1 Implementación de CoAP verificada formalmente en SPARK/Ada.pdf: 1209986 bytes, checksum: c3be514caf0dc982443a7170c2f41ac6 (MD5) Previous issue date: 2026-03-01en
dc.identifier.citationGómez Rojo, Manuel. Trabajo de Fin de Máster: Implementación de CoAP verificada formalmente en SPARK/Ada. Universidad Nacional de Educación a Distancia (UNED), 2026
dc.identifier.urihttps://hdl.handle.net/20.500.14468/32161
dc.language.isoes
dc.relation.centerEscuela Técnica Superior de Ingeniería Informática
dc.relation.degreeMáster Universitario en Ingeniería Informática
dc.relation.departmentSistemas de Comunicación y Control
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/deed.es
dc.subject1203.04 Inteligencia artificial
dc.subject.keywordsverificación formales
dc.subject.keywordsSPARK/Adaes
dc.subject.keywordsCoAPes
dc.subject.keywordsIoTes
dc.subject.keywordsciberseguridades
dc.subject.keywordsRecordFluxes
dc.subject.keywordsformal verificationen
dc.subject.keywordsSPARK/Adaen
dc.subject.keywordsCoAPen
dc.subject.keywordsIoTen
dc.subject.keywordscybersecurityen
dc.subject.keywordsRecordFluxen
dc.titleImplementación de CoAP verificada formalmente en SPARK/Adaes
dc.typetesis de maestríaes
dc.typemaster thesisen
dspace.entity.typePublication
relation.isDirectorOfPublicationf93103de-336d-47ac-886b-e2cbd425ed87
relation.isDirectorOfPublication.latestForDiscoveryf93103de-336d-47ac-886b-e2cbd425ed87
Archivos
Bloque original
Mostrando 1 - 1 de 1
Miniatura
Nombre:
Implementación de CoAP verificada formalmente en SPARK/Ada.pdf
Tamaño:
1.15 MB
Formato:
Adobe Portable Document Format
Descargar
Bloque de licencias
Mostrando 1 - 1 de 1
No hay miniatura disponible
Nombre:
license.txt
Tamaño:
3.62 KB
Formato:
Item-specific license agreed to upon submission
Descripción:
Descargar
Colecciones
Trabajos de fin de máster (TFM)