Título: Abstraktor: Generación automática de abstracciones de protocolo mediante instrumentación de código para fuzzing de sistemas distribuidos

Directores: Sebastián Uchitel y Víctor Braberman
Jurados: Prof. Diego Garbervetsky, Prof. Hernan Melgratti

Resumen: El testing de sistemas distribuidos es un problema de alta complejidad, donde los bugs más críticos emergen únicamente ante secuencias específicas de fallas. Si bien la especificación formal permite verificar las propiedades lógicas de un protocolo, garantizar que la implementación concreta en software sea fiel a dicho modelo abstracto continúa siendo un desafío abierto. Esta tesis aborda dicho problema investigando la viabilidad de sintetizar abstracciones generadas dinámicamente a partir de la ejecución real de un sistema para contrastarlas directamente contra una abstracción de la especificación formal. Con este propósito se desarrolló Abstraktor, una herramienta de instrumentación y análisis que captura variables dinámicas en tiempo de ejecución durante campañas de fuzzing guiadas, tomando el comportamiento del sistema como una abstracción de predicados. Como caso de estudio, la técnica se aplicó sobre el motor de almacenamiento distribuido Dqlite, regido por el protocolo de consenso Raft, comparando el modelo dinámica resultante contra el modelo de referencia derivado de la especificación formal en TLA+. A diferencia de un método de verificación exhaustiva, nuestro enfoque utiliza el fuzzing para sondear el espacio de estados y medir la divergencia entre el comportamiento del sistema y el modelo matemático. Los resultados evidencian una aproximación significativa, pero también revelan discrepancias que categorizamos en dos dimensiones: anomalías funcionales (que pueden ser bugs) y limitaciones de granularidad en la especificación. Esta clasificación no solo mide la conformidad actual, sino que funciona como un mecanismo de diagnóstico para refinar tanto la fidelidad del modelo como la robustez del código fuente.

Palabras clave: Sistemas distribuidos, Abstracción de predicados, Verificación formal,TLA+, Fuzzing, Raft.