Modeling and analysis of a flash filesystem

This paper describes the formal modeling and analysis of a design for a flash-based filesystem in Alloy. We model the basic operations of a filesystem as well as features that are crucial to NAND flash hardware, such as wear-leveling and erase-unit reclamation. In addition, we address the issue of fault tolerance by modeling a mechanism…

Analysis of the Android permission system

The ever increasing expansion of mobile applications into nearly every aspect of modern life, from banking to healthcare systems, is making their security more important than ever. Modern smartphone operating systems (OS) rely substantially on the permission-based security model to enforce restrictions on the operations that each application can perform. In this paper, we perform…

Alloy*: Higher-Order Extension to Alloy

The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order;…

Models of Software Systems

Scientific foundations for software engineering depend on the use of precise, abstract models and logics for characterizing and reasoning about properties of software systems. A number of basic models and logics over time have proven to be particularly important and pervasive in the development of software systems. This course is concerned with that body of…

Towards an Operational Semantics for Alloy

The Alloy modeling language has a mathematically rigorous denotational semantics based on relational algebra. Alloy specifications often represent operations on a state, suggesting a transition-system semantics. Because Alloy does not intrinsically provide a notion of state, however, this interpretation is only implicit in the relational-algebra semantics underlying the Alloy Analyzer. In this paper we demonstrate…

Alchemy: Transmuting Base Alloy Specifications into Implementations

Alloy specifications are used to define lightweight models of systems. We present Alchemy, which compiles Alloy specifications into implementations that execute against persistent databases. Alchemy translates a subset of Alloy predicates into imperative update operations, and it converts facts into database integrity constraints that it maintains automatically in the face of these imperative actions. In…

Logic for Systems

Mathematical logic provides the foundation for a rich set of tools for reasoning about systems and discovering whether their behavior meets our expectations. These tools allow us to model (e.g.) the state of buffers and caches, prove whether our protocols obey desirable properties, explore the consequences of memory-management strategies, and much more. As a Computer…

Solver-Aided Multi-Party Configuration

Configuring a service mesh often involves multiple parties, each of whom is responsible for separate portions of the overall system. This can result in miscommunication, silent and sudden errors, or a failure to meet goals. We identify two distinct modes of configuration that call for different solutions. We use synthesis algorithms to extract a set…

The Margrave Tool for Firewall Analysis

Writing and maintaining firewall configurations can be challenging, even for experienced system administrators. Tools that uncover the consequences of configurations and edits to them can help sysadmins prevent subtle yet serious errors. Our tool, Margrave, offers powerful features for firewall analysis, including enumerating consequences of configuration edits, detecting overlaps and conflicts among rules, tracing firewall…