Formal verification of infrastructure as code

Infrastructure-as-Code (IaC) is a system administration and software management paradigm that gained relevance in the industry with the widespread adoption of cloud computing technologies. Although IaC theoretically opens up the possibility for automatic verification of infrastructural specifications, available works on the subject focus on analysing operational aspects of the infrastructure lifecycle, such as deployment, orchestration and management. Little effort has been performed towards verifying structural and qualitative aspects of infrastructural code. In this document, we present DOML-MC, a prototype model checker back-end for DOML, an IaC language that is being developed as part of the PIACERE project. Infrastructural elements, their attributes and associations between them are encoded as an SMT problem, which is solved by the Z3 SMT solver. This approach proved useful to check critical or desirable properties of the analysed IaC document, but also to seek ways in which the infrastructure could be enriched to meet such properties.

Infrastructure-as-Code (IaC) (in italiano “infrastruttura come codice”) è un paradigma di amministrazione di sistema e gestione del software che ha acquistato rilevanza nell’industria con l’adozione diffusa delle tecnologie di cloud computing. Sebbene l’IaC apra teoricamente alla possibilità di verificare formalmente specifiche infrastrutturali, i lavori disponibili sull’argomento si concentrano sull’analisi di aspetti operazionali del ciclo di vita dell’infrastruttura, come deployment, orchestrazione e gestione. Non molto è stato fatto allo scopo di verificare aspetti strutturali e qualitativi del codice infrastrutturale. In questo documento, presentiamo DOML-MC, un back-end di model checker prototipale per DOML, un linguaggio di IaC che è in corso di sviluppo come parte del progetto PIACERE. Elementi infrastrutturali, i loro attributi e le associazioni tra di essi sono codificati in un problema di SMT, che viene risolto dal solver SMT Z3. Questo approccio è risultato utile nel controllare proprietà critiche o desiderabili del documento IaC analizzato, ma anche per ricercare modi in cui l’infrastruttura possa essere arricchita per andare incontro a tali proprietà.