Abstract
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HYBCORE with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HYBCORE as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HYBCORE, whose semantics is simpler and runnable, and yet intimately related with the semantics of HYBCORE at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCI for HASKELL and UTOP for OCAML. The major asset of our implementation is that it formally follows the operational semantic rules.

Abstract
Guaranteeing that safety-critical Cyber-Physical Systems (CPS) do not fail upon deployment is becoming an even more complicated task with the increased use of complex software solutions. To aid in this matter, formal methods (rigorous mathematical and logical techniques) can be used to obtain proofs about the correctness of CPS. In such a context, Runtime Verification has emerged as a promising solution that combines the formal specification of properties to be validated and monitors that perform these validations during runtime. Although helpful, runtime verification solutions introduce an inevitable overhead in the system, which can disrupt its correct functioning if not safely employed. We propose the creation of a Domain Specific Language (DSL) that, given a generic CPS, 1) verifies if its real-time scheduling is guaranteed, even in the presence of coupled monitors, and 2) implements several verification conditions for the correct-by-construction generation of monitoring architectures. To achieve it, we plan to perform statical verifications, derived from the available literature on schedulability analysis, and powered by a set of semi-automatic formal verification tools.

Abstract
Currently deployed in a wide variety of applicational scenarios, wireless sensor networks (WSNs) are typically a resource-constrained infrastructure. Consequently, characteristics such as WSN adaptability, low-overhead, and low-energy consumption are particularly relevant in dynamic and autonomous sensing environments where the measuring requirements change and human intervention is not viable. To tackle this issue, this article proposes e-LiteSense as an adaptive, energy-aware sensing solution for WSNs, capable of auto-regulate how data are sensed, adjusting it to each applicational scenario. The proposed adaptive scheme is able to maintain the sensing accuracy of the physical phenomena, while reducing the overall process overhead. In this way, the adaptive algorithm relies on low-complexity rules to establish the sensing frequency weighting the recent drifts of the physical parameter and the levels of remaining energy in the sensor. Using datasets from WSN operational scenarios, we prove e-LiteSense effectiveness in self-regulating data sensing accurately through a low-overhead process where the WSN energy levels are preserved. This constitutes a step-forward for implementing self-adaptive energy-aware data sensing in dynamic WSN environments.

Abstract
Monitoring current communication networks and services is an increasingly complex task as a result of a growth in the number and variety of components involved. Moreover, different perspectives on network monitoring and optimisation policies must be considered to meet context-dependent monitoring requirements. To face these demanding expectations, this article proposes a semantic-based approach to support the flexible configuration of context-aware network monitoring, where traffic sampling is used to improve efficiency. Thus, a semantic layer is proposed to provide with a standard and interoperable description of the elements, requirements and relevant features in the monitoring domain. On top of this description, semantic rules are applied to make decisions regarding monitoring and auditing policies in a proactive and context-aware manner. Use cases focusing on traffic accounting and traffic classification as monitoring tasks are also provided, demonstrating the expressiveness of the ontology and the contribution of smart SWRL rules for recommending optimised configuration profiles.

Abstract
This work studies Tor, an anonymous overlay network used to browse the Internet. Apart from its main purpose, this open-source project has gained popularity mainly because it does not hide its implementation. In this way, researchers and security experts can fully examine and confirm its security requirements. Its ease of use has attracted all kinds of people, including ordinary citizens who want to avoid being profiled for targeted advertisements or circumvent censorship, corporations who do not want to reveal information to their competitors, and government intelligence agencies who need to do operations on the Internet without being noticed. In opposition, an anonymous system like this represents a good testbed for attackers, because their actions are naturally untraceable. In this work, the characteristics of Tor traffic are studied in detail in order to devise an inspection methodology able to improve Tor detection. In particular, this methodology considers as new inputs the observer position in the network, the portion of traffic it can monitor, and particularities of the Tor browser for helping in the detection process. In addition, a set of Snort rules were developed as a proof-of-concept for the proposed Tor detection approach. © Springer Nature Switzerland AG 2020.

Abstract