Verification and synthesis of Infrastructure-as-Code through satisfiability modulo theories

This thesis explores formal verification and synthesis of Infrastructure-as-Code (IaC). Formal verification techniques for IaC are not widespread and literature about IaC synthesis is absent. Our work improves upon an existing model checker developed at PoliMi as part of PIACERE, an European DevSecOps framework, focusing on the IaC language DOML. The input model, along the DOML metamodel, is represented as a SMT problem, and then solved by the Z3 SMT solver. We developed a Domain Specific Language to let user declare custom requirements in a natural first-order logic inside a DOML file, allowing them to extend the model checker without touching the code base. We also designed an experimental synthesis module that receives an incomplete model and returns one satisfying the requirements. Model checking for IaC proved to be a useful tool to detect and fix structural problems before deployment, saving time and resources. Synthesis of IaC looks promising, as it can be a useful tool for users to further automate the IaC writing process.

Questa tesi esplora la verifica formale e la sintesi di Infrastructure-as-Code (letteralmente “Infrastruttura sotto forma di Codice”, abbreviato in IaC). Le tecniche di verifica formale per l’IaC non sono molto diffuse, mentre la letteratura riguardo la sintesi di esso e’ assente. Il nostro lavoro si concentra su un model checker sviluppato presso il PoliMi per PIACERE, un framework europeo per DevSecOps, ed il suo linguaggio IaC chiamato DOML. Il modello da verificare, insieme al metamodello del DOML, viene rappresentato come un problema di SMT, poi risolto dal solver Z3. Abbiamo sviluppato un linguaggio di dominio specifico che permette agli utenti di definire requisiti personalizzati sottoforma di formule logiche del primo ordine, anche all’interno di un file DOML, permettendo così di estendere il model checker senza dover modificare il codice sorgente. Abbiamo anche progettato un modulo sperimentale di sintesi che riceve un modello incompleto e ne produce uno che soddisfa tutti i requisiti. Il model checking per l’IaC si è dimostrato essere uno strumento utile per rilevare e aggiustare problemi architetturali e strutturali prima del deployment, facendo risparmiare tempo e risorse. La sintesi di IaC sembra promettente, potendo diventare uno strumento per automatizzare ancora di più il processo di scrittura dell’IaC.