Nowadays, IT infrastructures are involved in making innumerable aspects of our lives convenient, starting with water or energy distribution systems, and ending with e-commerce solutions and online banking services. In the worst case, cyberattacks on such infrastructures can paralyze whole states and lead to losses in terms of both human lives and money.One of the approaches to increase security of IT infrastructures relies on modeling possible ways of compromising them by potential attackers. To facilitate creation and reusability of such models, domain specific languages (DSLs) can be created. Ideally, a user will employ a DSL for modeling their infrastruc-ture of interest, with the domain-specific threats and attack logic being already encoded in the DSL by the domain experts.The Meta Attack Language (MAL) has been introduced previously as a meta-DSL for development of security-oriented DSLs. In this work, we define formally the syntax and a semantics of MAL to ease a common understanding of MAL's functionalities and enable reference implementations on different tech-nical platforms. It's applicability for modeling and analysis of security of IT infrastructures is illustrated with an example.

Connecting critical infrastructure assets to the network is absolutely essential for modern industries. In contrast to the apparent advantages, network connectivity exposes other infrastructure vulnerabilities that can be exploited by attackers. To protect the infrastructure, precise countermeasure identification is necessary. In this regard, the objective for the security officers is to identify the optimal set of countermeasures under a variety of budgetary restrictions. Our approach is based on the Meta Attack Language framework, which allows for convenient modelling of said infrastructures, as well as for automatic generation of attack graphs describing attacks against them. We formalize the problem of the selection of countermeasures in this context. The formalization makes it possible to deal with an arbitrary number of budgets, expressing available resources of both monetary and time-like nature, and to model numerous dependencies between countermeasures, including order dependencies, mutual exclusivity, and interdependent implementation costs. We propose a flexible and scalable algorithm for the problem. The whole methodology is validated in practice on realistic models.

Selecting the most pertinent countermeasures to secure a system is one of the ultimate goals of risk assessment. In this context, it is important to rely on modeling methods that the security experts are already familiar with, so that the solution can be smoothly adopted within industry. We propose a full-fledged framework, relying on attack-defense trees and integer linear programming, to find an optimal set of countermeasures. We use attack-defense trees formalized with directed acyclic graphs. This enables us to conveniently reason about attacker's actions that can contribute to several distinct attacks, and countermeasures that can block different ways of attacking. We provide a constructive way of extracting all reasonable behaviors of the two actors from such models. We then exploit this extracted information to formulate a generic solution, based on integer linear programing, to address a wide class of optimization problems. We show how to instantiate it for specific security-relevant optimization criteria. We cover deterministic and probabilistic cases. The framework has been implemented in a prototype tool, and validated in a real-life case study.