Upstate
Programming Languages
Seminar

A microservice-based application is composed of self-contained components called services that collectively process a request. Controlling inter-service communications is key to enforcing safety properties in such applications. Presently, only a limited class of single-hop properties can be specified. These policies can be overly permissive because they ignore the rich service tree structure of the inter-service communications. Policies that can express the service tree structure will offer fine-grained control over communication patterns to development and security teams.

In this talk, firstly, I will present an expressive policy language to specify service tree structures. Then, I will focus on our visibly pushdown automata-based runtime monitoring technique for enforcing service tree policies. Finally, I will present our engineering solution for a distributed monitor on top of an existing microservice deployment framework.

Programs running on many cyber-physical systems, such as trains, planes, and self-driving cars, are safety-critical but difficult to reason about and design. Formal verification can provide strong safety guarantees, but most industrial controllers are too complex to verify. Safe control envelopes characterize families of safe controllers and are used to monitor untrusted controllers on verifiable abstractions of control systems that isolate the parts relevant to safety without the full complexity of a specific control implementation, at runtime. They can put complex controllers, even when machine learning based, within the reach of formal guarantees. But correct control envelopes are still hard to design because the control engineer needs to identify correct control conditions that tell the controller what to do right now to stay safe at all times in the future by anticipating the behavior of the system over complex dynamics and an uncountably infinite state space. This talk is about a control envelope synthesis. We discuss techniques to synthesize provably correct control envelopes that are as permissive as possible, and represent them such that their synthesis composes along the structure of the control problem specification.

Replicated Datatypes (RDTs) have received significant interest from both the programming languages (PL) and distributed systems (DS) communities over the past few years. Such datatypes enable strong eventual consistency, which in turn enables the creation of applications that maintain high availability and scalability. However, programming against RDTs is still a challenging task; programmers of such applications face challenges from the complexity of reasoning about different evolving states on different replicas and how to achieve consistency in the face of ever-changing states. But this does not have to be the case; programmers want to program against high-level abstractions, which, when used carefully, can witness stronger consistency models even under asynchronous, weakly consistent replication. By recognizing and replicating shared abstractions themselves, we can have the best of both worlds: a consistent, familiar programming model and fast, scalable replication.

We introduce Orthogonal Replicated Datatypes (ORDTs), a new programming abstraction that enables modular reasoning about replicated data types. We then demonstrate that ORDTs can be sequentially consistent, even when implemented atop traditional, lazy replication. The orthogonal design of ORDTs allows multiple consistency strategies to be applied uniformly over a shared semantic foundation, facilitating compositionality and extensibility. Our approach employs relational semantics over complete lattices to enable deterministic n-way merges with restriction-aware validation. We provide comprehensive formal guarantees at multiple levels: we provide merge function correctness ensuring convergence, preservation, restriction compliance, idempotence and commutativity; we show how to provide provide sequential consistency via constraint graphs; we provide policy flexibility by enabling safe transitions between conflict resolution strategies through restriction composability. To support sequential consistency, we establish a taxonomy of mutations and observations that preserves consistency under varying operational constraints.

Programmers can leverage our abstraction by invoking built-in library functions or by defining custom merge strategies and constraints, with guaranteed convergence across replicas. Our gossip-based runtime demonstrates that ORDTs can preserve both sequential consistency and availability under network partitions.

Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting.

To fill this gap, we introduce TensorRight, the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, TensorRight DSL, to represent rewrite rules using a novel axis definition, called aggregated-axis, which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of TensorRight DSL. TensorRight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate TensorRight's verification capabilities by implementing rewrite rules present in XLA's algebraic simplifier. The results demonstrate that TensorRight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic, bounded-verification system can express only 18 of these rules.

To leverage independence while reasoning about probabilistic programs, researchers have recently developed a variety of separation logics. While these systems can greatly simplify verification, they require users to construct proofs manually. We design the first fully automatic approach to verify programs using the probabilistic separation logic PSL. We design a novel collection of syntax-directed proof rules and develop algorithms for inferring the distribution of random expressions, checking entailments, and applying axioms. We implement and evaluate our method in a prototype tool.

Reverse engineering (RE) is a ubiquitous aspect of software understanding. For example, in binary reverse engineering, an expert analyst interactively discovers (``reverses'') properties of a low-level software artifact such as a Windows PE or ELF binary. Recent observational studies of RE professionals show that they employ iterated rounds of hypothesis formation and falsification, assisted via a variety of automated and ad-hoc methods. Beyond binary RE, programmers employ RE skills throughout their career, in debugging their own code, understanding their collaborators' code, or integrating with APIs and frameworks. Unfortunately, because RE tools are extremely complex software systems, they are often very brittle and do not readily facilitate ad-hoc experimentation or integration with downstream tools. This talk proposes a new methodology for reverse engineering, declarative reverse engineering, wherein the artifact under analysis is decompiled to an arbitrarily-higher-level representation via declarative rules. I describe Reversi, the first multi-target, multi-language declarative decompiler that scales to production-sized binaries. The project's goal is to leverage modern logic-programming engines to revolutionize the way we design decompilers, radically increasing efficiency, reusability, and scalability by cleanly isolating the logical specification of the decompilation task from low-level matters such as data-structure implementation, binary parsing, and parallelization.

Type systems are light-weight yet powerful tools that provide end-to-end formal assurance while supporting modular reasoning. However, In modern systems--where third-party libraries and plugins using different compilers or even written in different languages interoperate---global properties enforced by a single type system can be easily violated. This problem is especially acute in decentralized-trust environments such as smart contracts, cloud services and WebAssembly modules, where principals inadvertantly or maliciously mislead others about types. In particular, the classic Confused Deputy Attack (CDA), long understood in traditional security settings, reemerges in Ethereum smart contracts when type confusion occurs.

To recover the end-to-end guarantees in this ""open-world"" paradigm, we formalize type confusion as a simulation relation between ill-typed and well-typed contexts of the program. Building on this, we present an information-flow typed core calculus with a runtime enforcement mechanism that preserves the security conditions enforced by the static type system.

Floating-point arithmetic enables the representation of numerical values with high precision in programs, making it essential for accurate computations in safety-critical systems. Due to the finite precision of floating-point numbers, computations are inherently approximations of real-number arithmetic, leading to rounding errors that can affect the correct functioning of a system. Existing verification methods for floating-point computations have limitations, particularly in handling programs with loops or achieving bit-precision. This paper introduces a new encoding of floating-point operations using Constrained Horn Clauses (CHCs) over the theory of bit-vectors, leveraging lazy int-blasting to reduce constraints to integer theory. The approach models floating-point arithmetic in a bit-precise way, and is able to verify safety of programs with unbounded loops that are beyond the capabilities of existing tools. We have integrated our encoding into the JayHorn model checker for Java and demonstrate its applicability across a set of benchmarks from multiple domains.

Spectacle is a novel framework for verifying relational properties of reconfigurable programs---programs whose behavior is parameterized by configurations that may evolve dynamically at runtime. Reasoning about such programs poses unique challenges: one must verify not only relations on the programs but also relations on the configurations. Existing relational struggle to reason compositionally about reconfigurable programs, relying on complex naming conventions to manage global configuration variables---to say nothing about how they are configured.

Spectacle addresses this gap by factoring relational reasoning through a different abstraction, a bidirectional lens, that maintains a relation on configuration. Rather than viewing lenses solely as a method for data synchronization, Spectacle uses them to build relational invariants that mediate behavior between reconfigurable systems. Additionally, Spectacle is equipped with a proof system that lifts lens-maintained relations on configurations to relational specifications over executions, allowing modular and compositional verification. This proof system is used to prove the equivalence of networking programs.

Computer systems are vulnerable to attacks via side channels, which leak information about the computation through the computation's secondary effects. For example, timing side channels leak sensitive information such as passwords through small differences in execution time. To prevent this, developers use static analyses to compute bounds on the amount of information a side channel can leak. To compute a correct bound, an analysis requires a model of the low-level system behavior, such as assumptions about the execution time of individual instructions. In this talk, I will present our work that leverages probabilistic models of low-level system components to analyze side-channel leakage. Our analyzer implements an abstract interpretation over a probability domain for LLVM IR, and computes a bound on the maximal leakage of the IR program. Preliminary results show that, for simple password-checking programs, our analyzer can accurately determine the amount of timing side-channel leakage.

Functional Programming languages are growing in popularity due to their strong guarantees and increased ease of proving correct. However, they are often difficult to optimize. Adjoint types provide a method of mixing substructural modes (for example linear, affine, strict, or unrestricted) in a type system while preserving the proof-theoretic and computational properties of each mode. Through this system, we can perform compiler optimizations or provide certain safety guarantees on parts of a program whose mode supports them, while not restricting the programmer’s ability to write code as they usually do. This talk will give an overview of such a type system, including an inference system for modes.

We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.

The Message Passing Interface (MPI), widely used in high performance computing, is typically implemented in imperative languages such as C, C++, or Fortran. This makes the verification of programs written in specific MPI implementations difficult. We are developing a concurrent lambda calculus to capture the message passing capabilities of MPI, which we later intend to use to verify popular algorithms used in MPI programming. We are currently focused on adding features needed for everyday MPI programming while still keeping the language slim and recognizable as a concurrent lambda calculus.

This work is in progress and we are interested in feedback both about important MPI features to capture as well as the design of the language.

Stable matching mechanisms are used in a variety of settings to match agents together, with a prominent example being the US national residency matching program. In this talk, we report ongoing work to examine stable matching mechanisms from a formal verification perspective using a form of logic programming known as answer set programming. First, we encode the stable matching problem as an answer set program and therefore, any answer set solver can produce correct stable matchings. However, modern answer set solvers are unable to handle large stable matching instances because their program grounding approach incurs enormous memory usage. To address the memory issue, we introduce an answer set solver that lazily grounds programs with modifiable solving strategies. While lazy grounding based solvers are much slower, we observe that their behavior is similar to that of stable matching mechanisms, and so provide an example of an efficient stable matching mechanism whose behavior can be realized as a choice of strategy for our solver.