Search papers, labs, and topics across Lattice.
This paper introduces Elton, a higher-order separation logic designed for reasoning about higher-order probabilistic programs in the presence of adversarial code. By integrating delayed samplings and a novel predicate called urn resources, Elton enables the specification of distributional properties and proves error bounds on complex security examples that surpass previous methodologies. The soundness of these extensions is validated through mechanized proofs using the Rocq proof assistant and the Iris separation logic framework, demonstrating significant advancements in the formal verification of probabilistic programs.
Elton can prove error bounds on security properties that were previously unaddressable, revolutionizing how we reason about adversarial probabilistic programs.
Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.
