Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU's leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants. As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs.

PLAS provides a forum for exploring and evaluating the use of programming language and program analysis techniques for promoting security in the complete range of software systems, from compilers to machine-learned models and smart contracts. The workshop encourages proposals of new, speculative ideas, evaluations of new or known techniques in practical settings, and discussions of emerging threats and problems. It also host position papers that are radical, forward-looking, and lead to lively and insightful discussions influential to the future research at the intersection of programming languages and security. This year will mark the 20th edition of PLAS, which was first held in 2007 in San Diego. The workshop will host 2 keynote talks, by Limin Jia and Jan Reineke, and 5 paper presentations.

Memory coloring is a software-based technique to ensure microarchitectural isolation between trust domains sharing a CPU. Prior coloring schemes target individual microarchitectural components and thus provide only partial solutions. In this paper, we provide theoretical foundations and practical algorithms to infer comprehensive coloring schemes for modern cloud CPUs.

We present Marghera, a system design that prevents cross-VM microarchitectural side-channel attacks in the cloud. Marghera is based on isolation contracts which, for a given CPU, describe partitions of physical threads and memory that prevent information leakage through shared microarchitectural resources.

Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.

We study satisfiability for HyperLTL with a ∀*∃* quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀*∃* HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀*∃* fragments is complemented by a new (incomplete) algorithm for ∀∃*-HyperLTL satisfiability.

We study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies $$\omega $$ -regular hyperproperties. HyperQPTL is an extension of linear-time temporal logic (LTL) with explicit trace and propositional quantification and therefore truly combines trace relations and $$\omega $$ -regularity. As such, HyperQPTL can express promptness, which states that there is a common bound on the number of steps up to which an event must have happened. We demonstrate how the HyperQPTL formulation of promptness differs from the type of promptness expressible in the logic Prompt-LTL. Furthermore, we study the realizability problem of HyperQPTL by identifying decidable fragments, where one decidable fragment contains formulas for promptness. We show that, in contrast to the satisfiability problem of HyperQPTL, propositional quantification has an immediate impact on the decidability of the realizability problem. We present a reduction to the realizability problem of HyperLTL, which immediately yields a bounded synthesis procedure. We implemented the synthesis procedure for HyperQPTL in the bounded synthesis tool BoSy. Our experimental results show that a range of arbiter satisfying promptness can be synthesized.

Hyperproperties, which generalize trace properties by relating multiple traces, are widely studied in information-flow security. Recently, a number of logics for hyperproperties have been proposed, and there is a need to understand their decidability and relative expressiveness. The new logics have been obtained from standard logics with two principal extensions: temporal logics, like LTL and CTL*, have been generalized to hyperproperties by adding variables for traces or paths. First-order and second-order logics, like monadic first-order logic of order and MSO, have been extended with the equal-level predicate. We study the impact of the two extensions across the spectrum of linear-time and branching-time logics, in particular for logics with quantification over propositions. The resulting hierarchy of hyperlogics differs significantly from the classical hierarchy, suggesting that the equal-level predicate adds more expressiveness than trace and path variables. Within the hierarchy of hyperlogics, we identify new boundaries on the decidability of the satisfiability problem. Specifically, we show that while HyperQPTL and HyperCTL* are both undecidable in general, formulas within their ∃*∀*fragments are decidable.