Adolescence is often associated with emotional upheaval and teens themselves value support with their emotions. HCI research on emotion regulation has focused on lab-based interventions for those with the greatest needs. This paper explores how adolescents use commercially available videogames in their daily environments and how these practices relate to emotion regulation. We conducted a 2-week diary and interview study with eleven teens asking them to reflect on their videogame practices and emotions. We deployed a multimodal diary to encourage authentic teen voice on factors not typically considered in intervention studies. Our findings indicate that teens use videogames to regulate their emotions and to recover from stress in diverse ways. These processes are often intertwined with adolescents’ social relationships and can be mediated through game affordances. We argue that traditional approaches to emotion regulation may be too individualistic to recognise or support the social dynamics that define teens’ emotional lives.

With the advent of Industry 4.0 , industrial facilities and critical infrastructures are transforming into an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers , increasingly interconnected and therefore exposed to cyber-physical attacks , i.e., security breaches in cyberspace that may adversely affect the physical processes underlying industrial control systems . In this article, we propose a formal approach based on runtime enforcement to ensure specification compliance in networks of controllers, possibly compromised by colluding malware that may locally tamper with actuator commands, sensor readings, and inter-controller communications. Our approach relies on an ad-hoc sub-class of Ligatti et al.’s edit automata to enforce controllers represented in Hennessy and Regan’s Timed Process Language . We define a synthesis algorithm that, given an alphabet 𝒫 of observable actions and a timed correctness property e , returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet 𝒫, and complying with the property e . Our monitors do mitigation by correcting and suppressing incorrect actions of corrupted controllers and by generating actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical requirements, such as transparency and soundness , the proposed enforcement enjoys deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers. Finally, we test the proposed enforcement mechanism on a non-trivial case study, taken from the context of industrial water treatment systems, in which the controllers are injected with different malware with different malicious goals.

Cyber-Physical systems (CPSs) are exposed to cyber- physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes of the systems.We define two probabilistic metrics to estimate the physical impact of attacks targeting cyber-physical systems formalised in terms of a probabilistic hybrid extension of Hennessy and Regan's Timed Process Language. Our impact metrics estimate the impact of cyber-physical attacks taking into account: (i) the severity of the inflicted damage in a given amount of time, and (ii) the probability that these attacks are actually accomplished, according to the dynamics of the system under attack. In doing so, we pay special attention to stealthy attacks, i. e., attacks that cannot be detected by intrusion detection systems. As further contribution, we show that, under precise conditions, our metrics allow us to estimate the impact of attacks targeting a complex CPS in a compositional way, i.e., in terms of the impact on its sub-systems.

With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into “smart” systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.'s edit automata, to enforce specification compliance in networks of potentially compromised controllers, formalised in Hennessy and Regan's Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers.

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1) We define a hybrid process calculus to model both CPSs and physics-based attacks. (2) We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands to drive a CPS into an undesired state; we group these attacks into classes and provide the means to assess attack tolerance/vulnerability with respect to a given class of attacks, based on a proper notion of most powerful physics-based attack. (3) We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4) We illustrate our definitions and results by formalising a non-trivial running example in U PPAAL SMC, the statistical extension of the U PPAAL model checker; we use U PPAAL SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.