Abstract
The prevalence and availability of cloud infrastructures has made them the de facto solution for storing and archiving data, both for organizations and individual users. Nonetheless, the cloud's wide spread adoption is still hindered by dependability and security concerns, particularly in applications with large data collections where efficient search and retrieval services are also major requirements. This leads to an increased tension between security, efficiency, and search expressiveness, which current state of the art solutions try to balance through complex cryptographic protocols that tradeoff efficiency and expressiveness for near optimal security. In this paper we tackle this tension by proposing BISEN, a new provably-secure boolean searchable symmetric encryption scheme that improves these three complementary dimensions by exploring the design space of isolation guarantees offered by novel commodity hardware such as Intel SGX, abstracted as Isolated Execution Environments (IEEs). BISEN is the first scheme to enable highly expressive and arbitrarily complex boolean queries, with minimal information leakage regarding performed queries and accessed data, and verifiability regarding fully malicious adversaries. Furthermore, by exploiting trusted hardware and the IEE abstraction, BISEN reduces communication costs between the client and the cloud, boosting query execution performance. Experimental validation and comparison with the state of art shows that BISEN provides better performance with enriched search semantics and security properties.

Abstract
Hybrid computation harbours discrete and continuous dynamics in the form of an entangled mixture, inherently present in various natural phenomena and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only in their analysis, but also in describing them adequately in a structural, well-founded way. In order to tackle these issues and, more generally, to investigate hybridness as a dedicated computational phenomenon, we introduce a while-language for hybrid computation inspired by the fine-grain call-by-value paradigm. We equip it with operational and computationally adequate denotational semantics. The latter crucially relies on a hybrid monad supporting an (Elgot) iteration operator that we developed elsewhere. As an intermediate step, we introduce a more lightweight duration semantics furnished with analogous results and based on a new duration monad that we introduce as a lightweight counterpart to the hybrid monad.

Abstract
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions, the resulting categories of coalgebras are even complete. As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability and behaviour.

Abstract
Current Maximum Satisfiability (MaxSAT) algorithms based on successive calls to a powerful Satisfiability (SAT) solver are now able to solve real-world instances in many application domains. Moreover, replacing the SAT solver with a Satisfiability Modulo Theories (SMT) solver enables effective MaxSMT algorithms. However, MaxSMT has seldom been used in debugging multi-threaded software. Multi-threaded programs are usually non-deterministic due to the huge number of possible thread operation schedules, which makes them much harder to debug than sequential programs. A recent approach to isolate the root cause of concurrency bugs in multi-threaded software is to produce a report that shows the differences between a failing and a non-failing execution. However, since they rely solely on heuristics, these reports can be unnecessarily large. Hence, reports may contain operations that are not relevant to the bug's occurrence. This paper proposes the use of MaxSMT for the generation of minimal reports for multi-threaded software with concurrency bugs. The proposed techniques report situations that the existing techniques are not able to identify. Experimental results show that using MaxSMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs.

Abstract
Current network management systems urge for a context-aware perspective of the provided network services and the underlying infrastructure usage. This need results from the heterogeneity of services and technologies in place, and from the massive traffic volumes traversing today’s networks. To reduce complexity and improve interoperability, monitoring systems need to be flexible, context-aware, and able to self-configure measurement points (MPs) according to network monitoring tasks requirements. In addition, the use of sampling techniques in MPs to reduce the amount of traffic collected, analysed and stored has become mandatory and, currently, distinct sampling schemes are available for use in operational environments. In this context, the main objective of this paper is the ontological definition of measurement requirements and components in sampling-based monitoring environments, with the aim of supporting an expert recommendation system able to understand context and identify the appropriate configuration rules to apply to a selection of MPs. In this way, the ontology, defining management needs, network measurement topology and sampling techniques, is described and explored considering several network management activities. A use case focusing on traffic accounting as monitoring task is also provided, demonstrating the expressiveness of the ontology and the role of the recommendation system in assisting context-aware network monitoring based on traffic sampling. © Springer Nature Switzerland AG 2019.

Abstract
In this work we investigate which aspects of data protection regulation must be carefully observed when implementing Blockchain-based projects in smart cities. This technology provides interesting properties and allows governments to develop flexible and innovative data management systems. Nevertheless, realizing the benefits of using Blockchains requires understanding the government processes along with the legal framework and political setting imposed on government. Though it is a buzzword, Blockchain may not always be the best solution for data processing, and carrying out a Data Protection Impact Assessment could allow an analysis of the necessity and proportionality of the mechanism. Furthermore, principles relating to security of data remain applicable to Blockchains. We discuss points of interaction between Blockchain technology and the European Union data protection framework, and provide recommendations on how to better develop Blockchain-based projects in smart cities. The findings of the study should provide public sector actors with a guideline to assess the real necessity and better format of a Blockchain-based application.