Attack trees (ATs) are a popular method for modeling security threats, but they typically assume a “perfect knowledge” where all actions and the state of the systems are fully known. This is unrealistic in practice, where attackers and defenders operate with limited visibility and finite resources. We introduce Supervised Attack Trees (SATs), a framework that extends ATs to model the strategic interaction between an attacker and a defender under partial observability and simultaneous budget constraints. In an SAT, each player sees only a subset of the system’s nodes. The defender (supervisor) can dynamically allocate a limited budget to postpone attacks, while the attacker spends a budget to compromise nodes. We formalize the concept of consistent observation, a snapshot of the partially visible state of the system, and provide an algorithm to verify its validity. Finally, we show how key questions like “given SATs, a defender budget, and an attacker budget, is there a strategy for the supervisor based solely on observations that guarantees the root will never be compromised, no matter how the attacker spends?” or “What is the minimum budget needed to guarantee an attack?” can be reduced to model-checking problems.

This paper investigates the enforcement of state-based security properties in process systems through supervisory control. We introduce a supervisor that operates under the assumption of incomplete system knowledge, mirroring the challenges faced in real-world deployments where both the supervisor and potential adversaries possess limited information. The proposed supervisor rectifies insecure process behaviors by strategically restricting actions or injecting timed events. Our study focuses on analyzing the necessary and sufficient conditions for the existence of such a supervisor capable of guaranteeing process security despite the knowledge limitations.

Algebraic methods are employed in order to define language-based security properties of processes. A supervisor is introduced that can disable unwanted behavior of an insecure process by controlling some of its actions or by inserting timed actions to make an insecure process secure. We assume a situation where neither the supervisor nor the attacker has complete information about the ongoing systems behavior. We study the conditions under which such a supervisor exists, as well as its properties and limitations.

This paper presents a novel approach to formal modeling and analyzing the resilience of networked sensor and actuator systems against targeted cyber-attacks, leveraging Timed Process Algebra (TPA). Recognizing the critical role of these systems in modern infrastructures and their inherent vulnerabilities, we develop a formal TPA-based model to represent sensors, actuators, communication channels, and malicious intruders as interacting processes. This model captures the dynamic behavior of the network, including data flow, control commands, and timing constraints, enabling the analysis of attack scenarios such as sensor disabling, actuator compromise, and communication disruption. We demonstrate some decidable and undecidable properties regarding the precise modeling of intruders, as well as employ model checking and an equivalence approach to verify some safety properties concerning intruders and supervisors.

Cyber-Physical Systems (CPS) are special kinds of systems with seamless integration of different entities. They are deployed mostly in safety-critical sectors, which make them a target for a wide range of attacks. Identifying potential threats to these kinds of systems is crucial and difficult as they consist of many modules, different producers, different technologies like programming, machine learning, and sometimes different manufactures. In this paper, we proposed a way of model potential ways in which attackers may compromise such systems using attack trees. We define a set of threat environments (i.e., changes in the vulnerability landscape of the system overtime) with each consisting of different sets of vulnerabilities, and use an attack tree generation algorithm to produce a tree at each threat environment. We further apply an information flow property - the opacity, to check a special kind of attacker who can observe the systems' non-secret states.

Autonomous systems are special kinds of systems that are complex, consist of many modules, different producers, different technologies like programming, machine learning, and sometimes different manufacturers. As such, checking for their properties, or even determining which state they are at a given moment, is a difficult task. To study the latter problem we use two models, originally developed in security theory, namely we combine attack trees and the information flow security. Hence a question of whether we can decide that a system has reached a given state (i.e., whether the root node of the attack tree is reached) is translated to checking current state opacity.

Formal definitions of state-based and language-based security with respect to timing attacks are proposed and studied. Then various ways how to secure systems with respect to such attacks are discussed. First, we investigate time insertion functions. Conditions, when such functions exist and could protect systems, are investigated. Then we discuss the concept of supervisor control which can be used if there is no appropriate time insertion function to protect the systems.

Time insertion functions as a tool to guarantee security of processes with respect to timing attacks are discussed and studied. We work with a security property called opacity and we investigate how it can be enforced by such functions. The time insertion function can alter time behaviour of original system by inserting some time delays to guarantee its security. We investigate conditions under which such functions do exist and also some of their properties.

This special issue contains articles selected from CS&P 2018, the 27th Workshop on Concurrency, Specification, and Programming. CS&P deals with formal specification of concurrent and parallel systems, mathematical models for describing such systems, and programming and verification concepts for their implementation. The workshop is one of a series of events organised every even year by Humboldt University of Berlin and every odd year by Warsaw University. Dating back to the midseventies, CS&P has become an important forum for researchers from European and Asian countries. CS&P 2018 was held at Humboldt University Berlin-Adlershof, Germany, in September 24-26, 2018, and featured 20 papers accepted for presentation by the program committee. After the conference, six outstanding papers were selected by the Steering Committee based on the previous reviews and the quality of the presentations. Their authors were given time to integrate the reviewer’s and audience’s feedback, as well as to substantially improve and extend their contributions. After the second round of reviewing by additional experts, during the pandemic year of 2020 the authors polished and finalized their contributions, to yield the mature articles which can be found in this special issue.

Safety-critical assets are facing enormous threats, and their continue existence lies in the ability to identify and mitigate these threats before they are realised. One good example of such assets is autonomous vehicles, a form of (application) AI that is equipped with self-awareness mechanisms that allow it to interact with a set of objects from the physical surrounding. However, this interaction can result in exposing the asset to a new set of undesired vulnerabilities that are difficult to identify. One of the traditional threat analysis methods used for threat modelling of different kinds of assets is attack trees, a well-known formalism used in security, safety, as well as risk analysis. In this paper, we propose an extension of attack trees, called dynamic attack trees . This allows us to model and analyse assets with dynamic threat environments that can interacts with external objects over time.

Gene regulatory networks represent the interactions among genes regulating the activation of specific cell functionalities and they have been successfully modeled using threshold Boolean networks. In this paper we propose a systematic translation of threshold Boolean networks into reaction systems. Our translation produces a non redundant set of rules with a minimal number of objects. This translation allows us to simulate the behavior of a Boolean network simply by executing the (closed) reaction system we obtain. This can be very useful for investigating the role of different genes simply by “playing” with the rules. We developed a tool able to systematically translate a threshold Boolean network into a reaction system. We use our tool to translate two well known Boolean networks modelling biological systems: the yeast-cell cycle and the SOS response in Escherichia coli. The resulting reaction systems can be used for investigating dynamic causalities among genes.

Attack trees are threat modeling formalism for identifying potential ways a system may be compromised. The underlying idea of this formalism is that possible attack points of a system are modeled as a set of nodes, together with the set of atomic actions which an attacker may execute to compromise the system. However, as attack trees are not designed from the administrator’s point of view, they are not equipped with sets of protection actions which can be used to stop an ongoing attack. In this paper we introduce reversible attack trees, as a variant of attack trees for which an ongoing attack can be fully or partially reset to the original state of the system. Then, we investigate whether the system administrator can detect whether a possible attack has reached some critical point in which his or her action is needed to prevent the attack by bringing the system to its initial state. Later, we show how this can be modeled by Timed Automata and checked by software tool UPPAAL.

We propose how attack trees formalism can be extended with time constraints. An attack tree is a basic description of how an attacker can compromise an asset, we refine this basic description by adding time constraints which can prevent an attacker from reaching the root node, if the attack actions performed cannot be completed within the defined time constraint. Adding time to attack trees causes an infinite number of possible states, to overcome this problem, we translate the tree into (an extended version of) timed automata and later use UPPAAL verification tool to analyse.

Time insertion functions as a way how to guarantee state-based security with respect to timing attacks are proposed and studied. As regards the security property, we work with the property called process opacity. First, we define timing attacks and later we show how security with respect to them can be enforced by such functions. The time insertion function can alter the time behaviour of the original system by inserting some time delays to guarantee its security. We investigate conditions under which such functions do exist and also some of their properties.

In this paper, an extended model for attack tree, called attack protection tree, is presented. The traditional attack trees threat model is extended with protection actions on the leaf nodes to protect the intermediate nodes from malicious attack. The proposed formalism allows the protection actions to be defined at the leaf nodes, by doing so, eliminating the chances of attack(s) being successful through ORrefinement. The concepts are illustrated through examples and we use a model checker for attack protection tree analyses.

A combination of formal methods and security testing for communication layer of multi-agent systems is proposed and studied. We start with security property called bisimulation process opacity. Unfortunately, this property is undecidable in general so we propose its more realistic variant based on simulation and tests and testing. A test represents an attacker’s (i.e. possibly one of the agents) scenario to obtain some confidential information on systems. Here we consider system to be secure if it cannot be compromised by a given test or set of tests. By test we can express also capabilities of an attacker related to time properties such as time measurement accuracy, duration of tests (attacks), complete lack of attacker’s time information and so on. At the end we state a decidability result for testing.

Power consumption is one of the main concerns in developing IoT Wireless Sensor Networks (WSNs) due to the limited amount of energy and the difficulty of recharging them. The energy consumption rate in WSNs varies greatly based on the protocols used. Therefore, developing energy-efficient protocols is an unavoidable issue in WSNs. In addition, it is highly advisable both, verify algorithms before their implementation and carry out performance evaluation prior to the deployment of novel algorithms in real environments. Thus, in this paper we study the problem of optimally controlling the use of sleep states in an energy-aware algorithm, the so-called SustainaBLE, to save energy in IoT Bluetooth Low Energy (BLE) devices. Timed Coloured Petri nets (TCPNs) have been used to obtain complete and unambiguous specifications as well as CPNTools to evaluate the correctness of the protocol and carry out performance evaluation. We present the TCPN formal model for SustainaBLE, which allows input parameters to fulfil the requirements of the system under study, and conduct a neat study of SustainaBLE by modifying the intervals in which the nodes remain in a sleep state. The results conform to those harvest from our testbed allowing us to conclude that we have got a suitable model for different performance evaluation without the need to deploy the system to be studied.

Insertion functions as a tool to guarantee security of processes is discussed and studied. We work with security properties opacity and processes opacity and we investigate how they can be enforced. The insertion function can alter behaviour of the original systems by inserting some actions to guarantee its security. Here we propose time insertion functions which insert time delays to prevent timing attacks.

Cloud computing is the infrastructure of choice for compute–intensive and data–intensive systems providing a flexible resources for software applications; that is, the processing capacity assigned to an application can be adapted to its needs. Nevertheless, in a cloud pay–per–use model, the number of demanded resources must be taken into account in order to minimise the costs. Our main goal is to reason about a cloud–aware application's resource usage by means of our Timed Process Algebra called BTC (Bounded True Concurrency), that is, to study the trade–offs between an application's response time and resource usage.