Showing 1–25 of 25 results for author: Forrest, S

Concerning the Responsible Use of AI in the US Criminal Justice System

Authors: Cristopher Moore, Catherine Gill, Nadya Bliss, Kevin Butler, Stephanie Forrest, Daniel Lopresti, Mary Lou Maher, Helena Mentis, Shashi Shekhar, Amanda Stent, Matthew Turk

Abstract: Artificial intelligence (AI) is increasingly being adopted in most industries, and for applications such as note taking and checking grammar, there is typically not a cause for concern. However, when constitutional rights are involved, as in the justice system, transparency is paramount. While AI can assist in areas such as risk assessment and forensic evidence generation, its "black box" nature r… ▽ More Artificial intelligence (AI) is increasingly being adopted in most industries, and for applications such as note taking and checking grammar, there is typically not a cause for concern. However, when constitutional rights are involved, as in the justice system, transparency is paramount. While AI can assist in areas such as risk assessment and forensic evidence generation, its "black box" nature raises significant questions about how decisions are made and whether they can be contested. This paper explores the implications of AI in the justice system, emphasizing the need for transparency in AI decision-making processes to uphold constitutional rights and ensure procedural fairness. The piece advocates for clear explanations of AI's data, logic, and limitations, and calls for periodic audits to address bias and maintain accountability in AI systems. △ Less

Submitted 30 May, 2025; originally announced June 2025.

Self-Organization in Computation & Chemistry: Return to AlChemy

Authors: Cole Mathis, Devansh Patel, Westley Weimer, Stephanie Forrest

Abstract: How do complex adaptive systems, such as life, emerge from simple constituent parts? In the 1990s Walter Fontana and Leo Buss proposed a novel modeling approach to this question, based on a formal model of computation known as $λ$ calculus. The model demonstrated how simple rules, embedded in a combinatorially large space of possibilities, could yield complex, dynamically stable organizations, rem… ▽ More How do complex adaptive systems, such as life, emerge from simple constituent parts? In the 1990s Walter Fontana and Leo Buss proposed a novel modeling approach to this question, based on a formal model of computation known as $λ$ calculus. The model demonstrated how simple rules, embedded in a combinatorially large space of possibilities, could yield complex, dynamically stable organizations, reminiscent of biochemical reaction networks. Here, we revisit this classic model, called AlChemy, which has been understudied over the past thirty years. We reproduce the original results and study the robustness of those results using the greater computing resources available today. Our analysis reveals several unanticipated features of the system, demonstrating a surprising mix of dynamical robustness and fragility. Specifically, we find that complex, stable organizations emerge more frequently than previously expected, that these organizations are robust against collapse into trivial fixed-points, but that these stable organizations cannot be easily combined into higher order entities. We also study the role played by the random generators used in the model, characterizing the initial distribution of objects produced by two random expression generators, and their consequences on the results. Finally, we provide a constructive proof that shows how an extension of the model, based on typed $λ$ calculus, could simulate transitions between arbitrary states in any possible chemical reaction network, thus indicating a concrete connection between AlChemy and chemical reaction networks. We conclude with a discussion of possible applications of AlChemy to self-organization in modern programming languages and quantitative approaches to the origin of life. △ Less

Submitted 23 August, 2024; v1 submitted 22 August, 2024; originally announced August 2024.

Automated Program Repair: Emerging trends pose and expose problems for benchmarks

Authors: Joseph Renzullo, Pemma Reiter, Westley Weimer, Stephanie Forrest

Abstract: Machine learning (ML) now pervades the field of Automated Program Repair (APR). Algorithms deploy neural machine translation and large language models (LLMs) to generate software patches, among other tasks. But, there are important differences between these applications of ML and earlier work. Evaluations and comparisons must take care to ensure that results are valid and likely to generalize. A c… ▽ More Machine learning (ML) now pervades the field of Automated Program Repair (APR). Algorithms deploy neural machine translation and large language models (LLMs) to generate software patches, among other tasks. But, there are important differences between these applications of ML and earlier work. Evaluations and comparisons must take care to ensure that results are valid and likely to generalize. A challenge is that the most popular APR evaluation benchmarks were not designed with ML techniques in mind. This is especially true for LLMs, whose large and often poorly-disclosed training datasets may include problems on which they are evaluated. △ Less

Submitted 8 May, 2024; originally announced May 2024.

Comments: 16 pages, 1 table, submitted to ACM Computing Surveys

GEVO-ML: Optimizing Machine Learning Code with Evolutionary Computation

Authors: Jhe-Yu Liou, Stephanie Forrest, Carole-Jean Wu

Abstract: Parallel accelerators, such as GPUs, are key enablers for large-scale Machine Learning (ML) applications. However, ML model developers often lack detailed knowledge of the underlying system architectures, while system programmers usually do not have a high-level understanding of the ML model that runs on the specific system. To mitigate this gap between two relevant aspects of domain knowledge, th… ▽ More Parallel accelerators, such as GPUs, are key enablers for large-scale Machine Learning (ML) applications. However, ML model developers often lack detailed knowledge of the underlying system architectures, while system programmers usually do not have a high-level understanding of the ML model that runs on the specific system. To mitigate this gap between two relevant aspects of domain knowledge, this paper proposes GEVO-ML, a tool for automatically discovering optimization opportunities and tuning the performance of ML kernels, where the model and training/prediction processes are uniformly represented in a single intermediate language, the Multiple-Layer Intermediate Representation (MLIR). GEVO-ML uses multi-objective evolutionary search to find edits (mutations) to MLIR code that ultimately runs on GPUs, improving performance on desired criteria while retaining required functionality. We demonstrate GEVO-ML on two different ML workloads for both model training and prediction. GEVO-ML finds significant Pareto improvements for these models, achieving 90.43% performance improvement when model accuracy is relaxed by 2%, from 91.2% to 89.3%. For the training workloads, GEVO-ML finds a 4.88% improvement in model accuracy, from 91% to 96%, without sacrificing training or testing speed. Our analysis of key GEVO-ML mutations reveals diverse code modifications, while might be foreign to human developers, achieving similar effects with how human developers improve model design, for example, by changing learning rates or pruning non-essential layer parameters. △ Less

Submitted 16 October, 2023; originally announced October 2023.

Understanding the Power of Evolutionary Computation for GPU Code Optimization

Authors: Jhe-Yu Liou, Muaaz Awan, Steven Hofmeyr, Stephanie Forrest, Carole-Jean Wu

Abstract: Achieving high performance for GPU codes requires developers to have significant knowledge in parallel programming and GPU architectures, and in-depth understanding of the application. This combination makes it challenging to find performance optimizations for GPU-based applications, especially in scientific computing. This paper shows that significant speedups can be achieved on two quite differe… ▽ More Achieving high performance for GPU codes requires developers to have significant knowledge in parallel programming and GPU architectures, and in-depth understanding of the application. This combination makes it challenging to find performance optimizations for GPU-based applications, especially in scientific computing. This paper shows that significant speedups can be achieved on two quite different scientific workloads using the tool, GEVO, to improve performance over human-optimized GPU code. GEVO uses evolutionary computation to find code edits that improve the runtime of a multiple sequence alignment kernel and a SARS-CoV-2 simulation by 28.9% and 29% respectively. Further, when GEVO begins with an early, unoptimized version of the sequence alignment program, it finds an impressive 30 times speedup -- a performance improvement similar to that of the hand-tuned version. This work presents an in-depth analysis of the discovered optimizations, revealing that the primary sources of improvement vary across applications; that most of the optimizations generalize across GPU architectures; and that several of the most important optimizations involve significant code interdependencies. The results showcase the potential of automated program optimization tools to help reduce the optimization burden for scientific computing developers and enhance performance portability for domain-specific accelerators. △ Less

Submitted 25 August, 2022; originally announced August 2022.

Automatically Mitigating Vulnerabilities in Binary Programs via Partially Recompilable Decompilation

Authors: Pemma Reiter, Hui Jun Tay, Westley Weimer, Adam Doupé, Ruoyu Wang, Stephanie Forrest

Abstract: Vulnerabilities are challenging to locate and repair, especially when source code is unavailable and binary patching is required. Manual methods are time-consuming, require significant expertise, and do not scale to the rate at which new vulnerabilities are discovered. Automated methods are an attractive alternative, and we propose Partially Recompilable Decompilation (PRD). PRD lifts suspect bina… ▽ More Vulnerabilities are challenging to locate and repair, especially when source code is unavailable and binary patching is required. Manual methods are time-consuming, require significant expertise, and do not scale to the rate at which new vulnerabilities are discovered. Automated methods are an attractive alternative, and we propose Partially Recompilable Decompilation (PRD). PRD lifts suspect binary functions to source, available for analysis, revision, or review, and creates a patched binary using source- and binary-level techniques. Although decompilation and recompilation do not typically work on an entire binary, our approach succeeds because it is limited to a few functions, like those identified by our binary fault localization. We evaluate these assumptions and find that, without any grammar or compilation restrictions, 70-89% of individual functions are successfully decompiled and recompiled with sufficient type recovery. In comparison, only 1.7% of the full C-binaries succeed. When decompilation succeeds, PRD produces test-equivalent binaries 92.9% of the time. In addition, we evaluate PRD in two contexts: a fully automated process incorporating source-level Automated Program Repair (APR) methods; human-edited source-level repairs. When evaluated on DARPA Cyber Grand Challenge (CGC) binaries, we find that PRD-enabled APR tools, operating only on binaries, performs as well as, and sometimes better than full-source tools, collectively mitigating 85 of the 148 scenarios, a success rate consistent with these same tools operating with access to the entire source code. PRD achieves similar success rates as the winning CGC entries, sometimes finding higher-quality mitigations than those produced by top CGC teams. For generality, our evaluation includes two independently developed APR tools and C++, Rode0day, and real-world binaries. △ Less

Submitted 12 June, 2023; v1 submitted 24 February, 2022; originally announced February 2022.

Cutting Through the Noise to Infer Autonomous System Topology

Authors: Kirtus G. Leyba, Joshua J. Daymude, Jean-Gabriel Young, M. E. J. Newman, Jennifer Rexford, Stephanie Forrest

Abstract: The Border Gateway Protocol (BGP) is a distributed protocol that manages interdomain routing without requiring a centralized record of which autonomous systems (ASes) connect to which others. Many methods have been devised to infer the AS topology from publicly available BGP data, but none provide a general way to handle the fact that the data are notoriously incomplete and subject to error. This… ▽ More The Border Gateway Protocol (BGP) is a distributed protocol that manages interdomain routing without requiring a centralized record of which autonomous systems (ASes) connect to which others. Many methods have been devised to infer the AS topology from publicly available BGP data, but none provide a general way to handle the fact that the data are notoriously incomplete and subject to error. This paper describes a method for reliably inferring AS-level connectivity in the presence of measurement error using Bayesian statistical inference acting on BGP routing tables from multiple vantage points. We employ a novel approach for counting AS adjacency observations in the AS-PATH attribute data from public route collectors, along with a Bayesian algorithm to generate a statistical estimate of the AS-level network. Our approach also gives us a way to evaluate the accuracy of existing reconstruction methods and to identify advantageous locations for new route collectors or vantage points. △ Less

Submitted 18 January, 2022; originally announced January 2022.

Comments: 10 pages, 8 figures, 1 table. To appear at IEEE INFOCOM 2022. © IEEE 2022

Journal ref: Proceedings of the IEEE Conference on Computer Communications (INFOCOM 2022), pp. 1609-1618

Challenges in cybersecurity: Lessons from biological defense systems

Authors: Edward Schrom, Ann Kinzig, Stephanie Forrest, Andrea L. Graham, Simon A. Levin, Carl T. Bergstrom, Carlos Castillo-Chavez, James P. Collins, Rob J. de Boer, Adam Doupé, Roya Ensafi, Stuart Feldman, Bryan T. Grenfell. Alex Halderman, Silvie Huijben, Carlo Maley, Melanie Mosesr, Alan S. Perelson, Charles Perrings, Joshua Plotkin, Jennifer Rexford, Mohit Tiwari

Abstract: We explore the commonalities between methods for assuring the security of computer systems (cybersecurity) and the mechanisms that have evolved through natural selection to protect vertebrates against pathogens, and how insights derived from studying the evolution of natural defenses can inform the design of more effective cybersecurity systems. More generally, security challenges are crucial for… ▽ More We explore the commonalities between methods for assuring the security of computer systems (cybersecurity) and the mechanisms that have evolved through natural selection to protect vertebrates against pathogens, and how insights derived from studying the evolution of natural defenses can inform the design of more effective cybersecurity systems. More generally, security challenges are crucial for the maintenance of a wide range of complex adaptive systems, including financial systems, and again lessons learned from the study of the evolution of natural defenses can provide guidance for the protection of such systems. △ Less

Submitted 21 July, 2021; originally announced July 2021.

Comments: 20 pages

MSC Class: A.0

Preventing Extreme Polarization of Political Attitudes

Authors: Robert Axelrod, Joshua J. Daymude, Stephanie Forrest

Abstract: Extreme polarization can undermine democracy by making compromise impossible and transforming politics into a zero-sum game. Ideological polarization - the extent to which political views are widely dispersed - is already strong among elites, but less so among the general public (McCarty, 2019, p. 50-68). Strong mutual distrust and hostility between Democrats and Republicans in the U.S., combined… ▽ More Extreme polarization can undermine democracy by making compromise impossible and transforming politics into a zero-sum game. Ideological polarization - the extent to which political views are widely dispersed - is already strong among elites, but less so among the general public (McCarty, 2019, p. 50-68). Strong mutual distrust and hostility between Democrats and Republicans in the U.S., combined with the elites' already strong ideological polarization, could lead to increasing ideological polarization among the public. The paper addresses two questions: (1) Is there a level of ideological polarization above which polarization feeds upon itself to become a runaway process? (2) If so, what policy interventions could prevent such dangerous positive feedback loops? To explore these questions, we present an agent-based model of ideological polarization that differentiates between the tendency for two actors to interact (exposure) and how they respond when interactions occur, positing that interaction between similar actors reduces their difference while interaction between dissimilar actors increases their difference. Our analysis explores the effects on polarization of different levels of tolerance to other views, responsiveness to other views, exposure to dissimilar actors, multiple ideological dimensions, economic self-interest, and external shocks. The results suggest strategies for preventing, or at least slowing, the development of extreme polarization. △ Less

Submitted 14 June, 2021; v1 submitted 11 March, 2021; originally announced March 2021.

Comments: 23 pages, 15 figures, 1 table

MIMOSA: Reducing Malware Analysis Overhead with Coverings

Authors: Mohsen Ahmadi, Kevin Leach, Ryan Dougherty, Stephanie Forrest, Westley Weimer

Abstract: There is a growing body of malware samples that evade automated analysis and detection tools. Malware may measure fingerprints ("artifacts") of the underlying analysis tool or environment and change their behavior when artifacts are detected. While analysis tools can mitigate artifacts to reduce exposure, such concealment is expensive. However, not every sample checks for every type of artifact-an… ▽ More There is a growing body of malware samples that evade automated analysis and detection tools. Malware may measure fingerprints ("artifacts") of the underlying analysis tool or environment and change their behavior when artifacts are detected. While analysis tools can mitigate artifacts to reduce exposure, such concealment is expensive. However, not every sample checks for every type of artifact-analysis efficiency can be improved by mitigating only those artifacts most likely to be used by a sample. Using that insight, we propose MIMOSA, a system that identifies a small set of "covering" tool configurations that collectively defeat most malware samples with increased efficiency. MIMOSA identifies a set of tool configurations that maximize analysis throughput and detection accuracy while minimizing manual effort, enabling scalable automation to analyze stealthy malware. We evaluate our approach against a benchmark of 1535 labeled stealthy malware samples. Our approach increases analysis throughput over state of the art on over 95% of these samples. We also investigate cost-benefit tradeoffs between the fraction of successfully-analyzed samples and computing resources required. MIMOSA provides a practical, tunable method for efficiently deploying analysis resources. △ Less

Submitted 18 January, 2021; originally announced January 2021.

GEVO: GPU Code Optimization using Evolutionary Computation

Authors: Jhe-Yu Liou, Xiaodong Wang, Stephanie Forrest, Carole-Jean Wu

Abstract: GPUs are a key enabler of the revolution in machine learning and high performance computing, functioning as de facto co-processors to accelerate large-scale computation. As the programming stack and tool support have matured, GPUs have also become accessible to programmers, who may lack detailed knowledge of the underlying architecture and fail to fully leverage the GPU's computation power. GEVO (… ▽ More GPUs are a key enabler of the revolution in machine learning and high performance computing, functioning as de facto co-processors to accelerate large-scale computation. As the programming stack and tool support have matured, GPUs have also become accessible to programmers, who may lack detailed knowledge of the underlying architecture and fail to fully leverage the GPU's computation power. GEVO (Gpu optimization using EVOlutionary computation) is a tool for automatically discovering optimization opportunities and tuning the performance of GPU kernels in the LLVM representation. GEVO uses population-based search to find edits to GPU code compiled to LLVM-IR and improves performance on desired criteria while retaining required functionality. We demonstrate that GEVO improves the execution time of the GPU programs in the Rodinia benchmark suite and the machine learning models, SVM and ResNet18, on NVIDIA Tesla P100. For the Rodinia benchmarks, GEVO improves GPU kernel runtime performance by an average of 49.48% and by as much as 412% over the fully compiler-optimized baseline. If kernel output accuracy is relaxed to tolerate up to 1% error, GEVO can find kernel variants that outperform the baseline version by an average of 51.08%. For the machine learning workloads, GEVO achieves kernel performance improvement for SVM on the MNIST handwriting recognition (3.24X) and the a9a income prediction (2.93X) datasets with no loss of model accuracy. GEVO achieves 1.79X kernel performance improvement on image classification using ResNet18/CIFAR-10, with less than 1% model accuracy reduction. △ Less

Submitted 27 April, 2020; v1 submitted 17 April, 2020; originally announced April 2020.

Risky Business: Assessing Security with External Measurements

Authors: Benjamin Edwards, Jay Jacobs, Stephanie Forrest

Abstract: Security practices in large organizations are notoriously difficult to assess. The challenge only increases when organizations turn to third parties to provide technology and business services, which typically require tight network integration and sharing of confidential data, potentially increasing the organization's attack surface. The security maturity of an organization describes how well it m… ▽ More Security practices in large organizations are notoriously difficult to assess. The challenge only increases when organizations turn to third parties to provide technology and business services, which typically require tight network integration and sharing of confidential data, potentially increasing the organization's attack surface. The security maturity of an organization describes how well it mitigates known risks and responds to new threats. Today, maturity is typically assessed with audits and questionnaires, which are difficult to quantify, lack objectivity, and may not reflect current threats. This paper demonstrates how external measurement of an organization can be used to assess the relative quality of security among organizations. Using a large dataset from BitSight(www.bitsight.com), a cybersecurity ratings company, containing 3.2 billion measurements spanning nearly 37,000 organizations collected during calendar year 2015, we show how per-organizational "risk vectors" can be constructed that may be related to an organization's overall security posture, or maturity. Using statistical analysis, we then study the correlation between the risk vectors and botnet infections. For example, we find that misconfigured TLS services, publicly available unsecured protocols, and the use of peer-to-peer file sharing correlate with organizations that have increased rates of botnet infections. We argue that the methodology used to identify these correlations can easily be applied to other data to provide a growing picture of organizational security using external measurement. △ Less

Submitted 22 May, 2019; v1 submitted 24 April, 2019; originally announced April 2019.

Comments: Updated data provider capitalization in text abstract

Using Dynamic Analysis to Generate Disjunctive Invariants

Authors: ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest

Abstract: Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra.… ▽ More Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard "max-plus" and "min-plus" algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants. △ Less

Submitted 16 April, 2019; originally announced April 2019.

Comments: appear in ICSE 2014

Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation

Authors: ThanhVu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest

Abstract: We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for t… ▽ More We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them. To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original programm. Preliminary results suggest that our approach compares favorably to other repair methods. △ Less

Submitted 27 March, 2019; originally announced March 2019.

Journal ref: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 301--318. Springer, 2017

The Surprising Creativity of Digital Evolution: A Collection of Anecdotes from the Evolutionary Computation and Artificial Life Research Communities

Authors: Joel Lehman, Jeff Clune, Dusan Misevic, Christoph Adami, Lee Altenberg, Julie Beaulieu, Peter J. Bentley, Samuel Bernard, Guillaume Beslon, David M. Bryson, Patryk Chrabaszcz, Nick Cheney, Antoine Cully, Stephane Doncieux, Fred C. Dyer, Kai Olav Ellefsen, Robert Feldt, Stephan Fischer, Stephanie Forrest, Antoine Frénoy, Christian Gagné, Leni Le Goff, Laura M. Grabowski, Babak Hodjat, Frank Hutter , et al. (28 additional authors not shown)

Abstract: Biological evolution provides a creative fount of complex and subtle adaptations, often surprising the scientists who discover them. However, because evolution is an algorithmic process that transcends the substrate in which it occurs, evolution's creativity is not limited to nature. Indeed, many researchers in the field of digital evolution have observed their evolving algorithms and organisms su… ▽ More Biological evolution provides a creative fount of complex and subtle adaptations, often surprising the scientists who discover them. However, because evolution is an algorithmic process that transcends the substrate in which it occurs, evolution's creativity is not limited to nature. Indeed, many researchers in the field of digital evolution have observed their evolving algorithms and organisms subverting their intentions, exposing unrecognized bugs in their code, producing unexpected adaptations, or exhibiting outcomes uncannily convergent with ones in nature. Such stories routinely reveal creativity by evolution in these digital worlds, but they rarely fit into the standard scientific narrative. Instead they are often treated as mere obstacles to be overcome, rather than results that warrant study in their own right. The stories themselves are traded among researchers through oral tradition, but that mode of information transmission is inefficient and prone to error and outright loss. Moreover, the fact that these stories tend to be shared only among practitioners means that many natural scientists do not realize how interesting and lifelike digital organisms are and how natural their evolution can be. To our knowledge, no collection of such anecdotes has been published before. This paper is the crowd-sourced product of researchers in the fields of artificial life and evolutionary computation who have provided first-hand accounts of such cases. It thus serves as a written, fact-checked collection of scientifically important and even entertaining stories. In doing so we also present here substantial evidence that the existence and importance of evolutionary surprises extends beyond the natural world, and may indeed be a universal property of all complex evolving systems. △ Less

Submitted 21 November, 2019; v1 submitted 9 March, 2018; originally announced March 2018.

Satisfiability Checking meets Symbolic Computation (Project Paper)

Authors: E. Abraham, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm

Abstract: Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is… ▽ More Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community. △ Less

Submitted 27 July, 2016; originally announced July 2016.

Journal ref: M. Kohlhase, M. Johansson, B. Miller, L. de Moura, F. Tompa, eds., Intelligent Computer Mathematics (Proceedings of CICM 2016), pp. 28-43, (Lecture Notes in Computer Science, 9791). Springer International Publishing, 2016

Satisfiability Checking and Symbolic Computation

Authors: E. Abraham, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm

Abstract: Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a… ▽ More Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities. △ Less

Submitted 23 July, 2016; originally announced July 2016.

Comments: 3 page Extended Abstract to accompany an ISSAC 2016 poster. Poster available at http://www.sc-square.org/SC2-AnnouncementPoster.pdf

Journal ref: ACM Communications in Computer Algebra, 50:4 (issue 198), pp. 145-147, ACM, 2016

Software Mutational Robustness

Authors: Eric Schulte, Zachary P. Fry, Ethan Fast, Westley Weimer, Stephanie Forrest

Abstract: Neutral landscapes and mutational robustness are believed to be important enablers of evolvability in biology. We apply these concepts to software, defining mutational robustness to be the fraction of random mutations that leave a program's behavior unchanged. Test cases are used to measure program behavior and mutation operators are taken from genetic programming. Although software is often viewe… ▽ More Neutral landscapes and mutational robustness are believed to be important enablers of evolvability in biology. We apply these concepts to software, defining mutational robustness to be the fraction of random mutations that leave a program's behavior unchanged. Test cases are used to measure program behavior and mutation operators are taken from genetic programming. Although software is often viewed as brittle, with small changes leading to catastrophic changes in behavior, our results show surprising robustness in the face of random software mutations. The paper describes empirical studies of the mutational robustness of 22 programs, including 14 production software projects, the Siemens benchmarks, and 4 specially constructed programs. We find that over 30% of random mutations are neutral with respect to their test suite. The results hold across all classes of programs, for mutations at both the source code and assembly instruction levels, across various programming languages, and are only weakly related to test suite coverage. We conclude that mutational robustness is an inherent property of software, and that neutral variants (i.e., those that pass the test suite) often fulfill the program's original purpose or specification. Based on these results, we conjecture that neutral mutations can be leveraged as a mechanism for generating software diversity. We demonstrate this idea by generating a population of neutral program variants and showing that the variants automatically repair unknown bugs with high probability. Neutral landscapes also provide a partial explanation for recent results that use evolutionary computation to automatically repair software bugs. △ Less

Submitted 27 June, 2013; v1 submitted 18 April, 2012; originally announced April 2012.

Modeling Internet-Scale Policies for Cleaning up Malware

Authors: Steven Hofmeyr, Tyler Moore, Stephanie Forrest, Benjamin Edwards, George Stelle

Abstract: An emerging consensus among policy makers is that interventions undertaken by Internet Service Providers are the best way to counter the rising incidence of malware. However, assessing the suitability of countermeasures at this scale is hard. In this paper, we use an agent-based model, called ASIM, to investigate the impact of policy interventions at the Autonomous System level of the Internet. Fo… ▽ More An emerging consensus among policy makers is that interventions undertaken by Internet Service Providers are the best way to counter the rising incidence of malware. However, assessing the suitability of countermeasures at this scale is hard. In this paper, we use an agent-based model, called ASIM, to investigate the impact of policy interventions at the Autonomous System level of the Internet. For instance, we find that coordinated intervention by the 0.2%-biggest ASes is more effective than uncoordinated efforts adopted by 30% of all ASes. Furthermore, countermeasures that block malicious transit traffic appear more effective than ones that block outgoing traffic. The model allows us to quantify and compare positive externalities created by different countermeasures. Our results give an initial indication of the types and levels of intervention that are most cost-effective at large scale. △ Less

Submitted 17 February, 2012; originally announced February 2012.

Comments: 22 pages, 9 Figures, Presented at the Tenth Workshop on the Economics of Information Security, Jun 2011

ACM Class: K.5.5; K.6.m; C.2.0

Internet Topology over Time

Authors: Benjamin Edwards, Steven Hofmeyr, George Stelle, Stephanie Forrest

Abstract: There are few studies that look closely at how the topology of the Internet evolves over time; most focus on snapshots taken at a particular point in time. In this paper, we investigate the evolution of the topology of the Autonomous Systems graph of the Internet, examining how eight commonly-used topological measures change from January 2002 to January 2010. We find that the distributions of most… ▽ More There are few studies that look closely at how the topology of the Internet evolves over time; most focus on snapshots taken at a particular point in time. In this paper, we investigate the evolution of the topology of the Autonomous Systems graph of the Internet, examining how eight commonly-used topological measures change from January 2002 to January 2010. We find that the distributions of most of the measures remain unchanged, except for average path length and clustering coefficient. The average path length has slowly and steadily increased since 2005 and the average clustering coefficient has steadily declined. We hypothesize that these changes are due to changes in peering policies as the Internet evolves. We also investigate a surprising feature, namely that the maximum degree has changed little, an aspect that cannot be captured without modeling link deletion. Our results suggest that evaluating models of the Internet graph by comparing steady-state generated topologies to snapshots of the real data is reasonable for many measures. However, accurately matching time-variant properties is more difficult, as we demonstrate by evaluating ten well-known models against the 2010 data. △ Less

Submitted 17 February, 2012; originally announced February 2012.

Comments: 6 pages, 5 figures

ACM Class: C.2.5; H.3.4

Beyond the Blacklist: Modeling Malware Spread and the Effect of Interventions

Authors: Benjamin Edwards, Tyler Moore, George Stelle, Steven Hofmeyr, Stephanie Forrest

Abstract: Malware spread among websites and between websites and clients is an increasing problem. Search engines play an important role in directing users to websites and are a natural control point for intervening, using mechanisms such as blacklisting. The paper presents a simple Markov model of malware spread through large populations of websites and studies the effect of two interventions that might be… ▽ More Malware spread among websites and between websites and clients is an increasing problem. Search engines play an important role in directing users to websites and are a natural control point for intervening, using mechanisms such as blacklisting. The paper presents a simple Markov model of malware spread through large populations of websites and studies the effect of two interventions that might be deployed by a search provider: blacklisting infected web pages by removing them from search results entirely and a generalization of blacklisting, called depreferencing, in which a website's ranking is decreased by a fixed percentage each time period the site remains infected. We analyze and study the trade-offs between infection exposure and traffic loss due to false positives (the cost to a website that is incorrectly blacklisted) for different interventions. As expected, we find that interventions are most effective when websites are slow to remove infections. Surprisingly, we also find that low infection or recovery rates can increase traffic loss due to false positives. Our analysis also shows that heavy-tailed distributions of website popularity, as documented in many studies, leads to high sample variance of all measured outcomes. These result implies that it will be difficult to determine empirically whether certain website interventions are effective, and it suggests that theoretical models such as the one described in this paper have an important role to play in improving web security. △ Less

Submitted 17 February, 2012; originally announced February 2012.

Comments: 13 pages, 11 figures

ACM Class: K.6.5; K.6.m

Nation-State Routing: Censorship, Wiretapping, and BGP

Authors: Josh Karlin, Stephanie Forrest, Jennifer Rexford

Abstract: The treatment of Internet traffic is increasingly affected by national policies that require the ISPs in a country to adopt common protocols or practices. Examples include government enforced censorship, wiretapping, and protocol deployment mandates for IPv6 and DNSSEC. If an entire nation's worth of ISPs apply common policies to Internet traffic, the global implications could be significant. Fo… ▽ More The treatment of Internet traffic is increasingly affected by national policies that require the ISPs in a country to adopt common protocols or practices. Examples include government enforced censorship, wiretapping, and protocol deployment mandates for IPv6 and DNSSEC. If an entire nation's worth of ISPs apply common policies to Internet traffic, the global implications could be significant. For instance, how many countries rely on China or Great Britain (known traffic censors) to transit their traffic? These kinds of questions are surprisingly difficult to answer, as they require combining information collected at the prefix, Autonomous System, and country level, and grappling with incomplete knowledge about the AS-level topology and routing policies. In this paper we develop the first framework for country-level routing analysis, which allows us to answer questions about the influence of each country on the flow of international traffic. Our results show that some countries known for their national policies, such as Iran and China, have relatively little effect on interdomain routing, while three countries (the United States, Great Britain, and Germany) are central to international reachability, and their policies thus have huge potential impact. △ Less

Submitted 18 March, 2009; originally announced March 2009.

An integrated model of traffic, geography and economy in the Internet

Authors: Petter Holme, Josh Karlin, Stephanie Forrest

Abstract: Modeling Internet growth is important both for understanding the current network and to predict and improve its future. To date, Internet models have typically attempted to explain a subset of the following characteristics: network structure, traffic flow, geography, and economy. In this paper we present a discrete, agent-based model, that integrates all of them. We show that the model generates… ▽ More Modeling Internet growth is important both for understanding the current network and to predict and improve its future. To date, Internet models have typically attempted to explain a subset of the following characteristics: network structure, traffic flow, geography, and economy. In this paper we present a discrete, agent-based model, that integrates all of them. We show that the model generates networks with topologies, dynamics, and (more speculatively) spatial distributions that are similar to the Internet. △ Less

Submitted 22 February, 2008; originally announced February 2008.

Journal ref: ACM SIGCOMM Computer Communication Review 38, 7-15 (2008)

Radial Structure of the Internet

Authors: Petter Holme, Josh Karlin, Stephanie Forrest

Abstract: The structure of the Internet at the Autonomous System (AS) level has been studied by both the Physics and Computer Science communities. We extend this work to include features of the core and the periphery, taking a radial perspective on AS network structure. New methods for plotting AS data are described, and they are used to analyze data sets that have been extended to contain edges missing f… ▽ More The structure of the Internet at the Autonomous System (AS) level has been studied by both the Physics and Computer Science communities. We extend this work to include features of the core and the periphery, taking a radial perspective on AS network structure. New methods for plotting AS data are described, and they are used to analyze data sets that have been extended to contain edges missing from earlier collections. In particular, the average distance from one vertex to the rest of the network is used as the baseline metric for investigating radial structure. Common vertex-specific quantities are plotted against this metric to reveal distinctive characteristics of central and peripheral vertices. Two data sets are analyzed using these measures as well as two common generative models (Barabasi-Albert and Inet). We find a clear distinction between the highly connected core and a sparse periphery. We also find that the periphery has a more complex structure than that predicted by degree distribution or the two generative models. △ Less

Submitted 22 August, 2006; originally announced August 2006.

Journal ref: Proc. R. Soc. A 463, (2007) 1231-1246

Technological networks and the spread of computer viruses

Authors: Justin Balthrop, Stephanie Forrest, M. E. J. Newman, Matthew M. Williamson

Abstract: Computer infections such as viruses and worms spread over networks of contacts between computers, with different types of networks being exploited by different types of infections. Here we analyze the structures of several of these networks, exploring their implications for modes of spread and the control of infection. We argue that vaccination strategies that focus on a limited number of networ… ▽ More Computer infections such as viruses and worms spread over networks of contacts between computers, with different types of networks being exploited by different types of infections. Here we analyze the structures of several of these networks, exploring their implications for modes of spread and the control of infection. We argue that vaccination strategies that focus on a limited number of network nodes, whether targeted or randomly chosen, are in many cases unlikely to be effective. An alternative dynamic mechanism for the control of contagion, called throttling, is introduced and argued to be effective under a range of conditions. △ Less

Submitted 19 July, 2004; originally announced July 2004.

Comments: 9 pages, 1 figure

Journal ref: Science 304, 527-529 (2004)