Abstract
Cloud Computing services for data analytics are increasingly being sought by companies to extract value from large quantities of information. However, processing data from individuals and companies in third-party infrastructures raises several privacy concerns. To this end, different secure analytics techniques and systems have recently emerged. These initial proposals leverage specific cryptographic primitives lacking generality and thus having their application restricted to particular application scenarios. In this work, we contribute to this thriving body of knowledge by combining two complementary approaches to process sensitive data. We present SafeSpark, a secure data analytics framework that enables the combination of different cryptographic processing techniques with hardware-based protected environments for privacy-preserving data storage and processing. SafeSpark is modular and extensible therefore adapting to data analytics applications with different performance, security and functionality requirements. We have implemented a SafeSpark’s prototype based on Spark SQL and Intel SGX hardware. It has been evaluated with the TPC-DS Benchmark under three scenarios using different cryptographic primitives and secure hardware configurations. These scenarios provide a particular set of security guarantees and yield distinct performance impact, with overheads ranging from as low as 10% to an acceptable 300% when compared to an insecure vanilla deployment of Apache Spark. © IFIP International Federation for Information Processing 2020.

Abstract
Data races, a condition where two memory accesses to the same memory location occur concurrently, have been shown to be a major source of concurrency bugs in distributed systems. Unfortunately, data races are often triggered by non-deterministic event orderings that are hard to detect when testing complex distributed systems. In this paper, we propose Spider, an automated tool for identifying data races in distributed system traces. Spider encodes the causal relations between the events in the trace as a symbolic constraint model, which is then fed into an SMT solver to check for the presence of conflicting concurrent accesses. To reduce the constraint solving time, Spider employs a pruning technique aimed at removing redundant portions of the trace. Our experiments with multiple benchmarks show that Spider is effective in detecting data races in distributed executions in a practical amount of time, providing evidence of its usefulness as a testing tool. © Springer Nature Switzerland AG 2020.

Abstract
This paper introduces a synthesis procedure for the satisfiability problem of RMTL-integral formulas as SAT solving modulo theories. RMTL-integral is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL-integral with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL-integral formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.

Abstract
Online applications now routinely replicate their data at multiple sites around the world. In this paper we present ATLAS, the first state-machine replication protocol tailored for such planet-scale systems. ATLAS does not rely on a distinguished leader, so clients enjoy the same quality of service independently of their geographical locations. Furthermore, clientperceived latency improves as we add sites closer to clients. To achieve this, ATLAS minimizes the size of its quorums using an observation that concurrent data center failures are rare. It also processes a high percentage of accesses in a single round trip, even when these conflict. We experimentally demonstrate that ATLAS consistently outperforms state-of-the-art protocols in planet-scale scenarios. In particular, ATLAS is up to two times faster than Flexible Paxos with identical failure assumptions, and more than doubles the performance of Egalitarian Paxos in the YCSB benchmark.

Abstract

Abstract
AbstractThe world is suffering from a pandemic called COVID-19, caused by the SARS-CoV-2 virus. The different national governments have problems evaluating the reach of the epidemic, having limited resources and tests at their disposal. Hence, any means to evaluate the number of persons with symptoms compatible with COVID-19 with reasonable level of accuracy is useful. In this paper we present the initial results of the @CoronaSurveys project. The objective of this project is the collection and publication of data concerning the number of people that show symptoms compatible with COVID-19 in different countries using open anonymous surveys. While this data may be biased, we conjecture that it is still useful to estimate the number of infected persons with the COVID-19 virus at a given point in time in these countries, and the evolution of this number over time. We show here the initial results of the @CoronaSurveys project in Spain and Portugal.