Scenario design and validation for next generation cyber ranges

Cyber Ranges are (virtual) infrastructures for the execution of cyber exercises of the highest quality that simulate cyber scenarios of real-world complexity. Building the computing infrastructure is only the first step towards the successful execution of the cyber exercises. The design, validation, and deployment of scenarios are costly and error-prone activities that may require specialized personnel for weeks or even months. Furthermore, a misconfiguration in the resulting scenario can spoil the entire cyber exercise. In this paper, we propose a framework for automating the (i) design, (ii) model validation, (iii) generation and (iv) testing of cyber scenarios. We introduce a Scenario Definition Language (SDL) based on the OASIS Topology and Orchestration Specification for Cloud Applications (TOSCA). SDL allows for the high level, declarative specification of the components and their interplay. We show that SDL specifications can be encoded into Datalog and that this allows for the automatic checking of the resulting model against a set of validation goals. If the check fails, then a design modification process is triggered. Otherwise, the validated scenario can be automatically deployed on the cyber range. The validation proof is then automatically converted into test cases whose successful execution gives evidence that also the deployed scenario meets the validation goals.