Systematic API Testing Through Model Checking and Executable Contracts

Titolo: Testing Sistematico delle API tramite Model Checking e Contratti Esecutivi

Autore: Ana Catarina Ribeiro, Margarida Mamede, Carla Ferreira (Università NOVA di Lisbona).

1. Il Problema

Il testing automatico "black-box" delle API RESTful si scontra con diverse limitazioni critiche:

• Divario Semantico: Le specifiche standard (come OpenAPI Specification - OAS) definiscono schemi dati e operazioni, ma mancano di semantica comportamentale dettagliata. Non descrivono come lo stato del sistema evolve o le dipendenze logiche tra le operazioni.
• Il Problema dell'Oracolo: Gli strumenti esistenti spesso usano i codici di stato HTTP (es. 2xx, 5xx) come unici oracoli di verifica. Questo è inaffidabile: un errore 5xx può essere causato da fattori esterni e non necessariamente da una violazione dei requisiti, mentre un 2xx può nascondere errori logici o violazioni di invarianti di stato.
• Copertura Limitata: La generazione di sequenze di chiamate è spesso casuale o basata su dipendenze superficiali, fallendo nel coprire stati complessi del sistema o interazioni multi-operazione (es. violazioni di integrità referenziale tra risorse).
• Scalabilità e Complessità: I sistemi microservizi sono spesso opachi e le loro implementazioni nascoste rendono difficile la generazione di test che esplorino sistematicamente lo spazio degli stati.

2. Metodologia: Il Framework ICEPICK

Gli autori introducono ICEPICK, un framework che combina il model checking formale con la generazione di test black-box. Il flusso di lavoro si divide in due fasi principali:

Fase 1: Pre-elaborazione della Specifica e Modellazione

1. Generazione dei Contratti (GLACIER):
   • Viene proposto GLACIER, un linguaggio di contratti basato sulla logica del primo ordine, esteso per le API RESTful.
   • Un generatore automatico deriva contratti (precondizioni e postcondizioni) dai file OAS utilizzando la semantica CRUD (Create, Read, Update, Delete).
   • I contratti includono invarianti globali (es. "il numero di giocatori iscritti non supera la capacità del torneo") e possono essere arricchiti manualmente per catturare vincoli specifici del dominio.
2. Modellazione TLA+:
   • Le specifiche OAS estese con i contratti GLACIER vengono trasformate in una specifica TLA+ (Temporal Logic of Actions).
   • Il modello TLA+ astrae lo stato del sistema (mappe di risorse) e le transizioni (azioni delle API).
   • Vengono definiti invarianti di tipo e invarianti di sistema che il model checker deve verificare.

Fase 2: Testing Sistematico

1. Esplorazione dello Spazio degli Stati (SSG):
   • Il model checker TLC (di TLA+) esplora esaurientemente lo spazio degli stati raggiungibili del modello, generando un State Space Graph (SSG).
   • Per mitigare l'esplosione dello spazio degli stati, viene utilizzata una traversata guidata dalla copertura (BFS) per estrarre percorsi dal nodo iniziale a quello finale.
2. Generazione delle Sequenze di Chiamata:
   • Un algoritmo personalizzato analizza l'SSG per generare sequenze di chiamate API che garantiscono la copertura di tutti gli stati e delle transizioni (quando non ci sono transizioni parallele).
3. Esecuzione e Verifica:
   • Le sequenze generate vengono eseguite contro l'API reale (SUT).
   • Un emulatore di stato traccia le risorse create/modificate durante il test.
   • Un evaluator verifica i contratti GLACIER in tempo reale: controlla precondizioni prima dell'invio, postcondizioni dopo la risposta e invarianti globali.
   • I risultati sono classificati in: OK, WARN, ERR, NOT_TESTED, fornendo un feedback granulare oltre al semplice pass/fail.

3. Contributi Chiave

• GLACIER: Un linguaggio di contratti eseguibile per API RESTful che arricchisce le specifiche OAS con semantica comportamentale, permettendo la verifica automatica durante l'esecuzione. Include un generatore automatico e un catalogo di formule riutilizzabili.
• Framework ICEPICK: Un approccio integrato che utilizza TLA+ e TLC per generare suite di test con garanzie di copertura dello spazio degli stati, risolvendo il problema dell'oracolo tramite contratti eseguibili.
• Algoritmo di Copertura: Un metodo basato su BFS per l'estrazione di percorsi dall'SSG che minimizza la lunghezza delle sequenze garantendo la copertura completa.
• Valutazione Empirica: Analisi su sistemi benchmark (EvoMaster) che dimostra la capacità di rilevare errori sottili e multi-operazione.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su tre sistemi: Tournaments (creato dagli autori), Swagger-Petstore e Features-Service.

• Scalabilità (RQ1-RQ3):
  • TLC è in grado di generare SSG per modelli di dimensioni moderate (fino a ~20-50 GB di stato) in tempi accettabili (minuti/ore), ma diventa impraticabile per modelli molto grandi (es. 467 GB in 16 ore).
  • L'algoritmo di generazione sequenze gestisce efficacemente grafi con decine di migliaia di stati e centinaia di migliaia di transizioni entro limiti di memoria ragionevoli (100 GB heap).
  • La copertura dello stato è del 100% per i modelli conformi a REST.
• Rilevamento dei Difetti (RQ4):
  • ICEPICK ha rilevato tutti i difetti iniettati nel sistema Tournaments, incluse violazioni di integrità referenziale che gli strumenti basati solo su codici HTTP non avrebbero trovato.
  • Su Features-Service, il framework ha identificato 97 errori legati alla mancanza di definizioni nei corpi delle richieste e alla non conformità con la semantica HTTP, dimostrando la sua capacità di esporre problemi strutturali.
• Impatto dei Contratti Manuali (RQ5):
  • Nel contesto dei difetti iniettati (principalmente errori CRUD e HTTP), i contratti generati automaticamente sono stati sufficienti. Tuttavia, gli autori sottolineano che i contratti manuali sono essenziali per difetti semantici specifici del dominio non catturabili dalla logica CRUD generica.

5. Significatività e Conclusioni

Il lavoro dimostra che combinare il model checking formale con l'inferenza di contratti eseguibili è un approccio potente per il testing black-box delle API.

• Vantaggi: Fornisce suite di test riproducibili con garanzie matematiche di copertura comportamentale e supera i limiti degli oracoli basati sui soli codici di stato HTTP.
• Limiti: L'efficacia dipende fortemente dalla conformità dell'API ai principi REST (codici di stato corretti, design orientato alle risorse). Se l'API viola questi principi, la generazione di contratti e modelli diventa difficile o impossibile. Inoltre, richiede uno sforzo manuale per scrivere le specifiche TLA+ (sebbene parzialmente automatizzabili).
• Impatto Futuro: Il paper evidenzia la necessità di benchmark più conformi a REST e suggerisce come direzione futura l'automazione completa della generazione delle specifiche TLA+ partendo da OAS arricchiti, per rendere l'approccio scalabile a sistemi complessi reali.

In sintesi, ICEPICK sposta il paradigma del testing API da una generazione casuale o basata su pattern superficiali a un'esplorazione sistematica e formalmente verificata dello spazio degli stati, offrendo una maggiore affidabilità per sistemi critici.