Robust forecasts of future resource usage in cloud computing environments enable high efficiency in resource management solutions, such as autoscaling and overcommitment policies. Production-level systems use lightweight combinations of historical information to enable practical deployments. Recently, Machine Learning (ML) models, in particular Long Short Term Memory (LSTM) neural networks, have been proposed by various works, for their improved predictive capabilities. Following this trend, we train LSTM models and observe high levels of prediction accuracy, even on unseen data. Upon meticulous visual inspection of the results, we notice that although the predicted values seem highly accurate, they are nothing but versions of the original data shifted by one time step into the future. Yet, this clear shift seems to be enough to produce a robust forecast, because the values are highly correlated across time. We investigate time series data of various resource usage metrics (CPU, memory, network, disk I/O) across different cloud providers and levels, such as at the physical or virtual machine-level and at the application job-level. We observe that resource utilisation displays very small variations in consecutive time steps. This insight can enable very simple solutions, such as data shifts, to be used for cloud resource forecasting and deliver highly accurate predictions. This is the reason why we ask whether complex machine learning models are even necessary to use. We envision that practical resource management systems need to first identify the extent to which simple solutions can be effective, and resort to using machine learning to the extent that enables its practical use. This talk will be based on work that has been presented in the 14th edition of the annual ACM Symposium on Cloud Computing (SoCC ‘23).

In this talk, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability.

A key aspect of the adoption of blockchain technologies is their performance. Consequently, many techniques to improve the scalability of blockchains are being developed. Current blockchains require consensus algorithms to guarantee that transactions, batched as blocks, are totally ordered. Imposing a total order, although it is safe, may be unnecessary for some applications. A promising approach to improve scalability is Setchain, a distributed concurrent data type that implements Byzantine tolerant distributed grown-only sets with barriers (called epochs). Setchain relaxes the total order requirement, and thus, can achieve higher throughput and scalability. In this work in progress, we propose a family of real-world Setchain implementations built on top of the Tendermint blockchain application platform. Our main contribution is Haschain, which exploits the compression power of hash functions to reduce the communication necessary during broadcasts and consensus, communicating a fixed-sized hash instead of hundreds or thousands of elements. The prize to pay is an additional distributed algorithm to obtain the set of elements from a hash, guaranteeing tolerance against Byzantine servers.

Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. The ideal scenario for abstract interpretation is that of a complete analysis, where false alarms cannot arise. Unfortunately for any non-trivial abstract domain there is some program whose analysis is incomplete. In this talk we discuss an approach to characterizing classes of complete programs on some non-trivial abstract domains for studying their expressiveness. To this aim we present the notion of bounded domains and show the implications arising from the possibility of conducting a complete analysis on such domains. In the talk we show how to tackle the problems of deciding program termination and equivalence, and discuss applicability of our approach.

Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this talk, we will introduce LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we will introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.