arXiv subjects

Christopher Wagner

Publications and source records attributed to Christopher Wagner.

7 recordsLinked to original sources

arXiv2022

Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)

Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, Cinnabar, to help system designers building DAB systems "fit" their intended designs into an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, Cinnabar generates sketch completions using a counterexample-guided procedure. The core technique relies on a compact encoding of a set of related counterexamples. We demonstrate Cinnabar's effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems.

cs.PL↗

arXiv2022

Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems

The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols as well as applications built on top of them. The complexity and unboundedness of such systems, however, makes their verification onerous in general, and, particularly prohibitive for full automation. An exciting, recent breakthrough reveals that, through careful modeling, it becomes possible for verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to be reduced to model checking of small, finite-state systems. It is an open question if such reductions are also possible for DAB systems that are doubly-unbounded, in particular, DAB systems that additionally have unbounded data domains. We answer this question in the affirmative in this work for models of DAB systems, thereby broadening the class of DAB systems which can be automatically verified. We present a new symmetry-based reduction and develop a tool, Venus, that can efficiently verify sophisticated DAB system models.

cs.PL↗

arXiv2020

HACCLE: Metaprogramming for Secure Multi-Party Computation -- Extended Version

Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An important class of such cryptographic techniques is known as Secure Multi-Party Computation (MPC). Developing Secure MPC applications in realistic scenarios requires extensive knowledge spanning multiple areas of cryptography and systems. And while the steps to arrive at a solution for a particular application are often straightforward, it remains difficult to make the implementation efficient, and tedious to apply those same steps to a slightly different application from scratch. Hence, it is an important problem to design platforms for implementing Secure MPC applications with minimum effort and using techniques accessible to non-experts in cryptography. In this paper, we present the HACCLE (High Assurance Compositional Cryptography: Languages and Environments) toolchain, specifically targeted to MPC applications. HACCLE contains an embedded domain-specific language Harpoon, for software developers without cryptographic expertise to write MPC-based programs, and uses Lightweight Modular Staging (LMS) for code generation. Harpoon programs are compiled into acyclic circuits represented in HACCLE's Intermediate Representation (HIR) that serves as an abstraction over different cryptographic protocols such as secret sharing, homomorphic encryption, or garbled circuits. Implementations of different cryptographic protocols serve as different backends of our toolchain. The extensible design of HIR allows cryptographic experts to plug in new primitives and protocols to realize computation. And the use of standard metaprogramming techniques lowers the development effort significantly.

cs.PL↗

arXiv2020

Parameterized Verification of Systems with Global Synchronization and Guards

Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including broadcast protocols and guarded protocols. We show that reachability properties are decidable for systems without guards, and give sufficient conditions under which they remain decidable in the presence of guards. Furthermore, we investigate cutoffs for reachability properties and provide sufficient conditions for small cutoffs in a number of cases that are inspired by our target applications.

cs.FL↗

arXiv2020

QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)

The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.

cs.PL↗

arXiv2018

Long-range entanglement near a Kondo-destruction quantum critical point

The numerical renormalization group is used to study quantum entanglement in the Kondo impurity model with a pseudogapped density of states $\rho(\varepsilon)\propto|\varepsilon|^r$ ($r>0$) that vanishes at the Fermi energy $\varepsilon=0$. The model features a Kondo-destruction quantum critical point (QCP) separating a partially screened phase (reached for impurity-band exchange couplings $J>J_c$) from a local-moment phase ($J<J_c$). The impurity contribution $S_e^{imp}$ to the entanglement entropy between a region of radius $R$ around the magnetic impurity and the rest of the host system reveals a characteristic length scale $R^*$ that distinguishes a regime $R\ll R^*$ of maximal critical entanglement from one $R\gg R^*$ of weaker entanglement. Within each phase, $S_e^{imp}$ is a universal function of $R/R^*$ with a power-law decay for $R/R^*\gg 1$. The entanglement length scale $R^*$ diverges on approach to the QCP with a critical exponent that depends only on $r$.

cond-mat.str-el↗

arXiv2015

Entanglement Entropy Near Kondo-Destruction Quantum Critical Points

We study the impurity entanglement entropy $S_e$ in quantum impurity models that feature a Kondo-destruction quantum critical point (QCP) arising from a pseudogap in the conduction-band density of states or from coupling to a bosonic bath. On the local-moment (Kondo-destroyed) side of the QCP, the entanglement entropy contains a critical component that can be related to the order parameter characterizing the quantum phase transition. In Kondo models describing a spin-$\Simp$, $S_e$ assumes its maximal value of $\ln(2\Simp+1)$ at the QCP and throughout the Kondo phase, independent of features such as particle-hole symmetry and under- or over-screening. In Anderson models, $S_e$ is nonuniversal at the QCP, and at particle-hole symmetry, rises monotonically on passage from the local-moment phase to the Kondo phase; breaking this symmetry can lead to a cusp peak in $S_e$ due to a divergent charge susceptibility at the QCP. Implications of these results for quantum critical systems and quantum dots are discussed.

cond-mat.str-el↗