Symmetry in integer programming causes redundant search and is often handled with symmetry breaking constraints that remove as many equivalent solutions as possible. We propose an algebraic method which allows to generate a family of random polynomial inequalities that can be used as symmetry breakers. The method requires as input an arbitrary base polynomial and a group of permutations which is specific to the integer program. The computations can be easily carried out in any major symbolic computation software. In order to test our approach, we describe a case study on near half-capacity 0-1 bin packing instances which exhibit substantial symmetries. We statically generate random quadratic breakers and add them to a baseline integer programming problem which we then solve with Gurobi. It turns out that simple symmetry breakers, especially those combining few variables and permutations, most consistently reduce work time.

Learning-augmented algorithms use machine learning predictions to boost optimization algorithms performance. The extra information incorporated into learning-augmented algorithms is, for example, the input which resembles prior instances, potentially aiding in circumventing the need to compute solutions from scratch or facilitating the utilization of existing solutions for deriving new ones.In previous works, we synthesized leasing cost optimal, subsequently named optimal, Cloud deployment plans by solving the corresponding constrained optimization problem using Satisfiability Modulo Theory (SMT) solvers and symmetry breakers. In this paper, we leverage the previously generated deployment plans to create a model of the deployed application. We employ graph neural networks (GNNs) for this purpose, encoding past deployment plans as graphs, with components and virtual machines as nodes and their interactions as edges. The GNN model trained can learn from historical data to predict optimal assignments by solving the corresponding edge classification problem. These predictions are then used as soft constraints in the exact SMT solver Z3, efficiently guiding the solver towards the optimal solution.We exemplify our approach on a Secure Web Container application.The accompanying material of this paper, as well as the application of our approach to other case studies, is publicly available at https://github.com/SAGE-Project/SAGE-GNN/tree/IJCNN2024.

Cloud computing has brought a fundamental transformation in how organizations operate their applications, enabling them to achieve affordable high availability of services. Kubernetes has emerged as the preferred choice for container orchestration and service management across many Cloud computing platforms. The scheduler in Kubernetes plays a crucial role in determining the placement of newly deployed service containers. However, the default scheduler, while fast, often lacks optimization, leading to inefficient service placement or even deployment failures.This paper introduces SAGE, a tool for optimal deployment plans in Kubernetes clusters that can also assist the Kubernetes default scheduler and any other custom scheduler in application deployment. SAGE computes an optimal deployment plan by fulfilling the constraints of the application to be deployed and by taking into consideration the available Cloud resources with the aim of minimizing the infrastructure rental cost. We show the potential benefits of using SAGE by considering test cases with various characteristics. It turns out that SAGE surpasses schedulers by comprehensively analyzing the application demand and cluster image. This ability allows it to better understand the needs of the pods, resulting in consistently optimal solutions across all test scenarios. The accompanying material of this paper is publicly available at https://github.com/SAGE-Project/SAGE-Predeployer.

We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.

Dealing with the provisioning of cloud services granted by Security SLAs is a very challenging research topic. At the state of the art, the main related issues involve: (i) representing security features so that they are understandable by both customers and providers and measurable (by means of verifiable security-related Service Level Objectives (SLOs)), (ii) automating the provisioning of security mechanisms able to grant desired security features (by means of a security-driven resource allocation process), and (iii) continuously monitoring the services in order to verify the fulfillment of specified Security SLOs (by means of cloud security monitoring solutions). We propose to face the Security SLA life cycle management with a framework able to enrich cloud applications with security features. In this paper we (i) present a novel Security SLA model and (ii) illustrate a security-driven planning process that can be adopted to determine the (optimum) deployment of security-related software components. Such process takes into account both specific implementation constraints of the security components to be deployed and customers security requirements, and enables the automatic provisioning and configuration of all needed resources. In order to demonstrate the applicability of the approach, we present and discuss a practical application of the model on a real case study.

The extensive use of cloud services by both individual users and organizations induces several security risks. The risk perception is higher when Cloud Service Providers (CSPs) do not clearly state their security policies and/or when such policies do not directly match user-defined requirements. Security-oriented Service Level Agreements (Security SLAs) represent a fundamental means to encourage the adoption of cloud services in contexts where security is mandatory. Nevertheless, despite the number of existing initiatives aimed at formalizing Security SLAs and at representing security guarantees by taking into account both customers' and providers' perspectives, they are far from being commonly adopted in practice by CSPs, due to the difficulty in automatically enforcing and monitoring the security capabilities agreed with customers. In this paper we illustrate, through a case study, a methodology to set-up a catalogue of security capabilities that can be offered as-a-service, on top of which specific guarantees can be specified through a Security SLA. Such a methodology, which explicitly takes into account the constraints behind the definition of formal guarantees related to security, is meant to serve as a guideline for providers willing to offer for their services specific security features that can be monitored and assessed by customers during operation.

We report on on-going efforts to apply real quantifier elimination to the synthesis of optimal numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound ε, find a real interval such that it contains [EQUATION] and its width is less than or equal to ε.