Actions over Core-closed Knowledge Bases

TL;DR

This paper introduces a formal framework using description logic to analyze cloud deployment configurations, focusing on security verification and planning of mutating actions within Infrastructure as Code.

Contribution

It presents an action language for modeling configuration changes and provides complexity results and decision procedures for security verification and planning problems.

Findings

Decidability results for static verification and planning problems.

Complexity classifications for various reasoning tasks.

Decision procedures for action-based configuration analysis.

Abstract

We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by adding, modifying, or deleting resources. We mainly focus on two problems: the problem of determining whether the execution of an action, no matter the parameters passed to it, will not cause the violation of some security requirement (static verification), and the problem of finding sequences of actions that would lead the deployment to a state where (un)desirable properties are (not) satisfied (plan existence and plan synthesis). For all these problems, we provide definitions, complexity results, and decision procedures.