Building next generation Cyber Ranges with CRACK

Cyber Ranges are complex infrastructures hosting high quality exercises that simulate cybersecurity scenarios of real-world complexity. Building the computing infrastructure is only the first step towards the successful execution of the cyber exercises. The design, verification and deployment of scenarios are costly and error-prone activities. As a matter of fact, a misconfiguration in the scenario can compromise the exercise and the training goals. This makes the design, development, and deployment of live-fire cyber exercises of real-world complexity so expensive that can be afforded only by a limited number of organizations. In this paper we present CRACK, a framework for the (i) design, (ii) model verification, (iii) generation, and (iv) automated testing of cyber scenarios. We introduce the CRACK SDL, a Scenario Definition Language based on TOSCA, an OASIS standard for the specification and orchestration of virtual infrastructures. CRACK SDL allows for the declarative specification of the scenario elements and their interplay, e.g., a vulnerability affecting a system. Through a formal encoding of the properties of an SDL specification, CRACK also supports the automatic verification of a scenario against its training objectives. After a successful verification, the scenario is automatically deployed in the Cyber Range and automatically tested to check the correspondence between the behavior of the deployed system and its specification. The key functionalities offered by CRACK are presented through a simple, yet representative case study. Experimental results confirm the effectiveness of the proposed approach.