skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Synthesizing Mutable Configurations: Setting up Systems for Success
Numerous devices, from network switches and servers to industrial control systems, can be unreliable if they are not configured properly. Even if a device’s implementation has been proven correct, it must still be configured to meet the specific functional and security requirements of its stakeholders. However, manual configuration remains labor intensive and error-prone even for experts. Automated configuration synthesis presents a promising way forward. Unfortunately, as we show, existing counterexample-guided algorithms can perform poorly if the system model allows configuration changes during execution. Yet disallowing such changes can hide significant problems, such as privilege escalation. We present a new synthesis algorithm that exploits structure inherent in state-machine models where the system configuration changes. We implement it using the Kodkod relational model finder, and show that it favorably solves a number of configuration-synthesis tasks.  more » « less
Award ID(s):
1714431
PAR ID:
10337613
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
Workshop on Software Engineering for Infrastructure and Configuration Code
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Distributed data analysis frameworks are widely used for processing large datasets generated by instruments in scientific fields such as astronomy, genomics, and particle physics. Such frameworks partition petabyte-size datasets into chunks and execute many parallel tasks to search for common patterns, locate unusual signals, or compute aggregate properties. When well-configured, such frameworks make it easy to churn through large quantities of data on large clusters. However, configuring frameworks presents a challenge for end users, who must select a variety of parameters such as the blocking of the input data, the number of tasks, the resources allocated to each task, and the size of nodes on which they run. If poorly configured, the result may perform many orders of magnitude worse than optimal, or the application may even fail to make progress at all. Even if a good configuration is found through painstaking observations, the performance may change drastically when the input data or analysis kernel changes. This paper considers the problem of automatically configuring a data analysis application for high energy physics (TopEFT) built upon standard frameworks for physics analysis (Coffea) and distributed tasking (Work Queue). We observe the inherent variability within the application, demonstrate the problems of poor configuration, and then develop several techniques for automatically sizing tasks to meet goals of resource consumption, and overall application completion. 
    more » « less
  2. Small uncrewed aerial systems (sUAS) are growing in their use for commercial, scientific, recreational, and emergency management purposes. A critical part of a successful flight is a correctly tuned controller which manages the physics of the vehicle. If improperly configured, it can lead to flight instability, deviation, or crashes. These types of misconfigurations are often within the valid ranges specified in the documentation; hence, they are hard to identify. Recent research has used fuzzing or explored only a small part of the parameter space, providing little understanding of the configuration landscape itself. In this work we leverage software product line engineering to model a subset of the parameter space of a widely used flight control software, using it to guide a systematic exploration of the controller space. Via simulation, we test over 20,000 configurations from a feature model with 50 features and 8.88 × 1034 products, covering all single parameter value changes and all pairs of changes from their default values. Our results show that only a small number of single configuration changes fail (15%), however almost 40% fail when we evaluate changes to two-parameters at a time. We explore the interactions between parameters in more detail, finding what appear to be many dependencies and interactions between parameters which are not well documented. We then explore a smaller, exhaustive product line model, with eight of the most important features (and 6,561 configurations) and uncover a complex set of interactions; over 48% of all configurations fail. 
    more » « less
  3. Deception is a crucial tool in the cyberdefence repertoire, enabling defenders to leverage their informational advantage to reduce the likelihood of successful attacks. One way deception can be employed is through obscuring, or masking, some of the information about how systems are configured, increasing attacker’s uncertainty about their tar-gets. We present a novel game-theoretic model of the resulting defender- attacker interaction, where the defender chooses a subset of attributes to mask, while the attacker responds by choosing an exploit to execute. The strategies of both players have combinatorial structure with complex informational dependencies, and therefore even representing these strategies is not trivial. First, we show that the problem of computing an equilibrium of the resulting zero-sum defender-attacker game can be represented as a linear program with a combinatorial number of system configuration variables and constraints, and develop a constraint generation approach for solving this problem. Next, we present a novel highly scalable approach for approximately solving such games by representing the strategies of both players as neural networks. The key idea is to represent the defender’s mixed strategy using a deep neural network generator, and then using alternating gradient-descent-ascent algorithm, analogous to the training of Generative Adversarial Networks. Our experiments, as well as a case study, demonstrate the efficacy of the proposed approach. 
    more » « less
  4. We investigate the problem of assembling general shapes and patterns in a model in which particles move based on uniform external forces until they encounter an obstacle. In this model, corresponding particles may bond when adjacent with one another. Succinctly, this model considers a 2D grid of “open” and “blocked” spaces, along with a set of slidable polyominoes placed at open locations on the board. The board may be tilted in any of the 4 cardinal directions, causing all slidable polyominoes to move maximally in the specified direction until blocked. By successively applying a sequence of such tilts, along with allowing different polyominoes to stick when adjacent, tilt sequences provide a method to reconfigure an initial board configuration so as to assemble a collection of previous separate polyominoes into a larger shape. While previous work within this model of assembly has focused on designing a specific board configuration for the assembly of a specific given shape, we propose the problem of designing universal configurations that are capable of constructing a large class of shapes and patterns. For these constructions, we present the notions of weak and strong universality which indicate the presence of “excess” polyominoes after the shape is constructed. In particular, for given integers h, w, we show that there exists a weakly universal configuration with O(hw) 1 × 1 slidable particles that can be reconfigured to build any h × w patterned rectangle. We then expand this result to show that there exists a weakly universal configuration that can build any h × w-bounded size connected shape. Following these results, which require an admittedly relaxed assembly definition, we go on to show the existence of a strongly universal configuration (no excess particles) which can assemble any shape within a previously studied “drop” class, while using quadratically less space than previous results. Finally, we include a study of the complexity of deciding if a particle within a configuration may be relocated to another position, and deciding if a given configuration may be transformed into a second given configuration. We show both problems to be PSPACE-complete even when no particles stick to one another and movable particles are restricted to 1 × 1 tiles and a single 2 × 2 polyomino. 
    more » « less
  5. Abstract Sulfur‐rich volcanic eruptions happen sporadically. If Stratospheric Aerosol Injection (SAI) were to be deployed, it is likely that explosive volcanic eruptions would happen during such a deployment. Here we use an ensemble of Earth System Model simulations to show how changing the injection strategy post‐eruption could be used to reduce the climate risks of a large volcanic eruption; the risks are also modified even without any change to the strategy. For a medium‐size eruption (10 Tg‐SO2) comparable to the SAI injection rate, the volcanic‐induced cooling would be reduced if it occurs under SAI, especially if artificial sulfur dioxide injections were immediately suspended. Alternatively, suspending injection only in the eruption hemisphere and continuing injection in the opposite would reduce shifts in precipitation in the tropical belt and thus mitigate eruption‐induced drought. Finally, we show that for eruptions much larger than the SAI deployment, changes in SAI strategy would have minimal effect. 
    more » « less