Mitigating Runtime Errors in Infrastructure as Code Programs Using Static Type Analysis

Abstract

Infrastructure as Code (IaC) ist essenziell für die Verwaltung von Cloud-Infrastrukturen,aber Laufzeitfehler treten selbst in den am sorgfältigsten geschriebenen Programmen auf, was zu teuren Ausfallzeiten und Sicherheitslücken führt. Trotz der weit verbreiteten Nutzung von Tools wie Pulumi zeigt unsere Arbeit, dass eine bedeutende Möglichkeit zur Reduzierung dieser Fehler durch statische Typensysteme ungenutzt bleibt. Diese Arbeit befasst sich mit der kritischen Frage, wie die statische Typentheorie genutzt werden kann,um Laufzeitfehler in IaC-Programmen zu verringern.Wir finden und unterteilen echte Laufzeitfehler in drei Kategorien zunehmender Komplexität — Enumerations, Refinements und Dependencies — und verbinden sie mit Enums, Refinement Types und Dependent Types aus der statischen Typentheorie. Zur Formalisierung dieser Typen führen wir einen minimalen Lambda-Kalkül λ→ und darauf basierende Erweiterungen ein, um diese Fehler statisch zu erkennen. Unsere Analyse zeigt, dass viele Laufzeitfehler in IaC-Programmen durch statische Typanalyse verhindert werden können.Durch eine umfassende Evaluierung von Pulumi, einem führenden IaC-Tool, das mehrere Programmiersprachen unterstützt, stellen wir fest, dass Pulumi statische Typinformationen oft nicht nutzt, selbst wenn sie verfügbar sind. Konkret zeigen wir, dass bis zu 48.68%der AWS-Repositories, 22.29% der Azure-Repositories und 28.45% der GCP-Repositories aus einem Datensatz von 1023 Repositories von Enums profitieren würden – diese werden jedoch in den am häufigsten genutzten Pulumi-Provider-Varianten ignoriert. Darüber hinaus zeigen wir, dass Pulumi Refinement Types in Form von Validierungsparametern,die in den Cloud-Provider-APIs vorhanden sind, übersieht und somit eine Möglichkeit zur Vermeidung von Laufzeitfehlern verpasst.Wir zeigen außerdem, dass während Dependent Types die komplexesten Fehler, bei denen Parameter voneinander abhängen, abfangen könnten, weder Cloud-Provider-APIs, noch Pulumi, noch die von Pulumi unterstützten Programmiersprachen native Unterstützung für Dependent Types bieten.Diese Arbeit schließt mit der Empfehlung, diese statische Typinformation zu verwenden,um die Zuverlässigkeit von IaC-Programmen zu verbessern, Laufzeitfehler deutlich zu reduzieren und das Management von Cloud-Infrastrukturen zu optimieren.

Infrastructure as Code (IaC) is essential for managing Cloud infrastructure, but runtime errors occur even in the most carefully written programs, leading to costly downtime and vulnerabilities. Despite the widespread adoption of tools like Pulumi, our investigation reveals that a significant opportunity to mitigate these errors through static type systemsis being missed. This thesis addresses the critical issue of how to leverage static type theory to reduce runtime errors in IaC programs.We find and divide real runtime errors into three categories of escalating levels of complexity — Enumerations, Refinements, and Dependencies — and connect them to enums, refinement types, and dependent types from static type theory. To formalise them, we introduce a minimal lambda calculus, λ→, and extensions to it to recognise these errors statically. Our analysis shows that many runtime errors in IaC programs can be prevented by statically enforcing enums, refinement types and dependent types.Through an extensive evaluation of Pulumi, a leading IaC tool supporting multiple programming languages, we find that Pulumi often fails to use static type information,even when it is readily available. Specifically, we show that up to 48.68% of AWS repositories, 22.29% of Azure repositories, and 28.45% of GCP repositories of a dataset of 1023 repositories would benefit from enum types—yet these are ignored in Pulumi’s most common provider variants. Additionally, we demonstrate that Pulumi overlooks refinement type information in the form of validation constraints present in Cloud provider APIs, missing an opportunity to prevent runtime errors.We show that, while dependent types could mitigate the most complex errors involving interdependent parameters, neither Cloud provider APIs, Pulumi, nor the programming languages it supports offer native support for dependent types.This thesis concludes by advocating for the adoption of these type systems to enhance the reliability of IaC programs, making significant strides toward reducing runtime errors and improving Cloud infrastructure management.