arXiv CSopen access

Formalization of security

Chapter 19

Formalization of Security Gilles Barthe

arXiv:2607.28551v1 [cs.CR] 30 Jul 2026

Second readers: Lennart Beringer and Andreas Lochbihler

Abstract Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification. This chapter focuses on their applications to system security, language-based security, secure compilation, and cryptography.

19.1 Introduction Security is often a major consideration in the design and implementation of software systems. Because security goals can be difficult to achieve and security analyses can contain subtle flaws, proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification, e.g., Common Criteria evaluations, with mechanized proofs. In this chapter, we focus on applications of proof assistants to system security, language-based security, secure compilation, and cryptography. We briefly discuss other applications at the end of the chapter.

19.2 Information Flow A fundamental security goal is to prevent illegal information flows, including leaking secrets on public channels (confidentiality) or corrupting high-integrity data with Gilles Barthe Max Planck Institute for Security and Privacy, Bochum, Germany, and IMDEA Software Institute, Madrid, Spain, e-mail: [email protected],[email protected]

1

2

Gilles Barthe

untrusted values (integrity). This entails analyzing how information is flowing during the lifetime of a system or the execution of a program. In general, information flow security considers lattices of security levels (for confidentiality and for integrity) and controls the flow of information between distinct security levels. The simplest examples of lattices are: • Confidentiality: ({Public, Secret}, Public ≤ Secret); • Integrity: ({Trusted, Untrusted}, Trusted ≤ Untrusted). Information flow policies are typically used to (dis)allow information flows: for example, a baseline confidentiality policy is that secrets do not flow to public components, whereas a baseline integrity policy is that untrusted (i.e., potentially corrupted) components do not flow to trusted components. These two policies are instances of noninterference, an information flow policy introduced by Goguen and Meseguer [122]. In a follow-up work, Goguen and Meseguer [123] provide a powerful technique, called unwinding, that allows to reduce proofs of noninterference to simpler lemmas about one-step execution. Broadly speaking, unwinding lemmas are stated relative to an equivalence relation ∼ on states, where two states are related by ∼ if and only if they cannot be distinguished by an attacker. There are two basic unwinding lemmas: • The step-consistent lemma states that one-step execution of ∼-related states yields ∼-related states. Informally, if s1 ⇝ s′1 and s2 ⇝ s′2 , then under some additional conditions, s1 ∼ s2 implies s′1 ∼ s′2 . • The step-preserving lemma guarantees that one-step execution preserves ∼. Informally, if s ⇝ s′ , then under some additional conditions, s ∼ s′ . By combining the two lemmas, one can prove that execution traces with ∼-related initial states yield ∼-related final states.

19.2.1 Systems-Level Security Many systems-level security policies can be modeled as noninterference policies, and have been a main target of formalization. Rushby [195] used the EHDM Verification System, a predecessor of PVS, to mechanize unwinding lemmas in a more complex setting of intransitive noninterference, where information is allowed to flow through specific channels. Von Oheimb [178] formalizes a variant of Rushby’s framework in Isabelle/HOL and uses the resulting formalization to reason about the security of the Infineon SLE66 chip. More recently, Bracevac et al. [72] use Isabelle/HOL to formalize MAKS (Modular Assembly Kit of Security properties), a rich framework developed by Mantel to reason about information flow policies [157]. There is also a substantial body of work that establishes information flow properties of specific systems. Many works focus on operating systems and virtualization platforms. The seL4 project uses Isabelle/HOL to show that seL4 enforces in-

19 Formalization of Security

3

tegrity, authority confinement [199], and intransitive noninterference [165]. Barthe et al. [33, 34] use Rocq (formerly known as Coq) to prove memory isolation for a model of virtualization that includes caches and a translation lookaside buffer. They isolate a class of executions that do not leak information to an attacker executing on another partition and with control over the cache replacement policy and the scheduler. Dam et al. [98] use HOL4 to formally verify information flow security for a simple separation kernel for ARMv7. Their main result is stated as an equivalence between an ideal model in which the security requirements hold by construction with a real model that faithfully respects the system behavior. Li et al. [153] and Tao et al. [215] use Rocq to prove confidentiality and integrity guarantees for a model of the KVM hypervisor, both with respect to a sequential and to a relaxed memory model. Azevedo de Amorim et al. [25] use Rocq to model the SAFE architecture and prove that the SAFE machine enforces noninterference. A follow-up work [26] extends this approach to provide a generic framework to enforce a rich set of micro-policies, and instantiates the approach to verify several prominent examples of micro-policies. Nelson et al. [170] provides a recent overview of machinechecked proofs of noninterference for secure systems. Some works focus explicitly on web browsers. Bohannon [67] uses Rocq to define a core model of the Firefox web browser and proves reactive noninterference [68]. Jang, Tatlock, and Lerner [145] use the principles of shim verification to verify QUARK, a web browser structured similarly to Google Chrome. Kanav, Lammich, and Popescu [147] and Bauereiss, Pesenti Gritti, Popescu, and Raimondi [54] use Isabelle for developing a conference management system and a social platform with verified confidentiality guarantees. Both proofs make use of bounded deducibility [147], a framework that combines the benefits of proofs by unwinding, the precision of nondeducibility, and support for declassification. Some formalizations are specifically developed or strongly motivated by security evaluations, such as Common Criteria. The Formavie project [65] developed a formal model of the JavaCard virtual machine in Rocq. The formalization was used in an Common Criteria certification at the highest level: EAL7. Andronick, Boutali, Ly, and Paulin-Mohring [17,18] build on this model to reason about isolation properties. Hardin, Smith, and Young [136] use ACL2 for modeling the Rockwell Collins AAMP7G microprocessor in the context of a NSA certification.

19.2.2 Language-Based Security Language-based security [196] is an approach to strengthen security of applications through programming language tools. Language-based security is foundational: indeed, many language-based mechanisms come with a proof that they enforce a security property of interest. This makes language-based security a natural target for mechanization. Often, mechanizations that target language-based security leverage existing mechanizations of programming languages, compilers, and program logics, described in other chapters of the handbook.

4

Gilles Barthe

Imperative features Hrit, cu et al. [143] use Rocq to formalize a fine-grained dynamic enforcement mechanism to enforce noninterference of programs with exceptions. Silver et al. [203] develop an extension of interaction trees [226] with support for exceptions and build a Rocq library to reason about information flow properties of programs and to prove soundness of information flow type systems. In a different vein, Azevedo de Amorim, Hrit, cu, and Pierce [27] use Rocq to formalize a core programming language with manual memory management, and show that safe programs satisfy a noninterference property, namely that programs do not modify or depend on unreachable parts of the state.

19.2.2.1 Java-Like Languages Some of the earliest mechanizations of language-based security focus on sequential fragments of Java virtual machine bytecode. For instance, Barthe, Pichardie, and Rezk [48] use Rocq to formalize an information flow type system for a sequential fragment of the Java bytecode, and prove that typable programs are noninterfering. Wasserrab, Lohner, and Snelting [225] use Isabelle/HOL to formalize information flow control for program dependence graphs and instantiate their framework to derive a proof of noninterference for a sequential fragment of Java bytecode.

19.2.2.2 C-Like Languages Amtoft et al. [16] formalize an information flow analyzer for the SPARK language in Rocq. The formalization provides an operational semantics for a core fragment of the language, a relational program logic, and a proof of its soundness with respect to the operational semantics, and a checker that is proved sound with respect to the semantics and program logics. The formalization also generates correctness certificates for an external information flow analyzer. Constanzo, Shao, and Gu [93] develop a separation logic for reasoning about information flow of C-like programs in Rocq. Proofs in separation logic guarantee the existence of a suitable bisimulation between two runs of the program under verification, and thus noninterference.

19.2.2.3 Higher-Order Languages Nanevski, Banerjee, and Garg [168] introduce relational Hoare type theory, a relational extension of Hoare type theory for reasoning about information-flow properties of stateful higher-order programs. Relational Hoare type theory uses a shallow embedding of programs into Rocq. Recently, Frumin, Krebbers, and Birkedal [116] use the Iris framework to mechanize a concurrent separation logic to reason about timing-sensitive noninterference of concurrent higher-order stateful programs. In

19 Formalization of Security

5

subsequent work, Gregersen, Bay, Timany, and Birkedal [128] introduce modal weakest precondition and show how they can be used to reason modularly about the more permissive termination-sensitive noninterference.

19.2.2.4 Concurrency and Probabilistic Choice Barthe and Prensa-Nieto [47] use Isabelle/HOL to mechanize proofs of noninterference for a concurrent imperative language. Popescu, Hölzl, and Nipkow use Isabelle/HOL to mechanize proofs of noninterference for source languages with concurrency [190] and probabilistic choice [191]. Murray, Sison, Pierzchalski, and Rizkallah [166] use Isabelle/HOL to prove soundness for a value-dependent information flow analysis for a core programming language with concurrency. Motivated by proof automation, Ernst and Murray [109] develop a concurrent separation logic for reasoning about data-dependent information flow policies of C-like programs. They implement their logic into an automated prover, called SecC, and use Isabelle/ HOL to mechanize its soundness proof.

19.2.2.5 Dynamic Enforcement Most mechanizations consider static enforcement. However, there is a large body of the security literature that uses dynamic enforcement mechanisms. Beringer [59] formalizes a hybrid enforcement approach that combines static analysis and dynamic taint tracking. The approach is proved sound with respect to an operational semantics in Rocq. Recently, Xian and Chong [227] develop a coarse-grained dynamic information flow system for a Java-like language, and mechanize the soundness of a core subsystem using Rocq. Also recently, Vassena et al. [223] use Agda to establish an equivalence between two styles for dynamic enforcement of information-flow policies.

19.2.2.6 Side Channels Information flow policies have also been used to reason about side-channel leakage. In this context, policies state that leakage is independent of secrets and are defined on top of an instrumented semantics that captures leakage. One popular policy is the so-called (cryptographic) constant-time policy. It is based on a leakage model where branching statements leak their guards, memory reads and writes leak the addresses of the memory accessed, and (in some works) variable-time arithmetic instructions leak (size of) their operands [30]. Building on top of the CompCert formalization, Barthe et al. [34] define and formally verify a type system that enforces constanttime for assembly programs. Cock [90] uses a formalization of pGCL in Isabelle to obtain formally verified upper bounds on programs leakage.

6

Gilles Barthe

Resource usage (see below) is often a side channel that can be exploited by an attacker to retrieve confidential information. Such attacks can be avoided by ensuring that programs are constant-resource—i.e., their resources consumptions do not depend on secrets. The constant-resource policy can be seen as an instance of an observational information flow policy, and more specifically, a noninterference policy with respect to a resource-instrumented semantics of programs. Ngo, DehesaAzuara, Frederikson, and Hoffmann [171] define constant-resource type systems and use Agda to prove soundness of the type systems with respect to a resourceinstrumented semantics.

19.3 Resource Usage There is a large body of work that uses proof assistants for reasoning about complexity bounds of popular algorithms and implementations. The most direct approach for reasoning about the complexity of algorithms is to prove formally an upper bound on a mathematical definition of the cost function. This direct approach has been used for instance by Nipkow [175] and by Eberl, Halsbeck, and Nipkow [105] for proving upper bounds of the cost of deterministic and probabilistic algorithms. However, it is often better to formalize and instantiate generic tools, such as master theorems. For instance, Eberl [104] formalizes the Akra–Bazzi method in Isabelle, and Tassarotti and Harper formalize [216] Karp’s cookbook theorem for verifying tail bounds of randomized algorithms. Yet another approach is to build general libraries for cost. For instance, Danielsson [99] uses Agda to formalize a library for reasoning about the time complexity of purely functional data structures. Li, Xia, and Weirich [154] define a shallow embedding of the claivoyance monad in Rocq, and leverage this embedding to reason formally about the cost of lazy evaluation. A related approach is to build automated tools for reasoning about complexity of functions with respect to a cost model. Early work by Benzinger [58] uses a combination of abstract interpretation and recurrence solvers to reason about the cost of Nuprl expressions. Similar techniques can also be used to reason about implementations. Alternatively, one can formalize metatheoretical properties of static analyses, type systems and program logics for cost, and use their guarantees to reason about the cost of specific algorithms. For instance, Cachera, Jensen, Pichardie, and Schneider [79] implement a formally verified algorithm for checking that JavaCard programs do not allocate memory in loops and therefore execute in bounded memory. Aspinall et al. [22] formalize the soundness of a resource-aware program logic for a fragment of the Java virtual machine using Isabelle. Carbonneaux, Hoffmann, and Shao [84] use Rocq to verify the soundness of a program logic that supports compositional potential-based resource analyses of programs. Later, Carbonneaux, Hoffmann, Reps, and Shao [83] develop a resource bound analysis that generates Rocq certificates of their correctness for a core language; one main advantage of their analysis is that it supports polynomial bounds. Charguéraud and Pottier [86] formalize an approach based on characteristic formulas and time credits to prove the

19 Formalization of Security

7

complexity of a union–find implementation. Later, Charguéraud, and Pottier [87] and Mével, Jourdan, and Pottier [129] formalize a separation logic with time credits and negative time credits in Rocq and use their logic to prove complexity of several algorithms, including the union–find data structure. Pottier et al. [192] extend these works to support reasoning about thunks and credits and use the resulting framework to prove complexity bounds for several functional data structures. In a probabilistic setting, Hölzl and Nipkow [142] prove expected runtime of the ZeroCond protocol in Isabelle. Later, Hölzl [141] formalize in Isabelle/HOL a weakest pre-expectation calculus for expected running times based on [146]. Tassarotti and Harper [217] use the Iris framework in Rocq to formalize a concurrent separation logic for probabilistic programs and use their framework to derive complexity bounds for skiplists. Avanzini et al. [23] extend EasyCrypt with an expectation logic for probabilistic programs and use the logic to prove upper bounds for skiplists. We refer to [176] and [85, §6.2] for more detailed overviews of formally verified complexity analysis.

19.4 Access Control and Capabilities Access control is a classic mechanism to enforce security of computer systems. Access control policies are typically defined by large sets of rules. The interactions between different rules may have unintended implications or simply lead to inconsistencies, when rules disagree whether or not to grant access. Bad interactions between rules can compromise security, making it important to analyze formally the consequences and consistency of access control policies. Capretta, Stepien, Felty, and Matwin [81] verify using Rocq an algorithm for conflict detections in firewalls, and use their algorithm to detect conflicts in policies with several hundred thousands of rules. Following a similar approach, St-Martin and Felty [211] verify formally in Rocq an algorithm for detecting conflicts in eXtensible Access Control Markup Language (XACML) policies. Brucker, Brügger, and Wolff [74] use formalize in HOL firewall policies, and the HOL-TESTGEN tool to generate abstract test cases from the formal model. Sohr, Drouineaud, Ahn, and Gogolla [205] verify in Isabelle/HOL role-based access control (RBAC) policies. Their verification relies on an Isabelle/HOL formalization of first-order linear temporal logic, in which RBAC policies can be encoded. More recently, Cutler et al. [97] use Lean to formalize key properties of Cedar, an expressive authorization language used by Amazon Web Services. Cedar supports role-based, attribute-based, and relation-based access control. Capability-based systems support powerful mechanisms, such as transferring capabilities, and are able to enforce fine grained security policies in low-level systems. As such, they are an interesting and challenging target for mechanization. CHERI [1] uses unforgeable capabilities to guarantee safety and security in presence of untrusted code. The CHERI team [53, 174] has produced several mechanizations of CHERI in Isabelle/HOL. These formalizations establish monotonicity properties,

8

Gilles Barthe

ensuring for examples that capabilities cannot be increased during execution. In addition, Park, Pai, and Melham [181] and Zaliva et al. [230] provide formal models of CHERI C in Isabelle and Rocq respectively. CERISE [119,213] is a program logic for reasoning about capabilities in presence of unknown code. The soundness of the CERISE program logic is established in Rocq using logical relations.

19.5 Hyperproperties Program verification is traditionally focused on trace properties, including safety and liveness properties. However, many security properties are hyperproperties [89], i.e., sets of sets of traces, rather than properties. A special class of hyperproperties is hypersafety, which guarantees that nothing goes bad across a set of executions; for instance, noninterfence is a typical example of hypersafety. Hyperlogics [110] are temporal or program logics for verifying that programs satisfy a given hyperproperty. In their most expressive forms, hyperlogics extend usual logics by allowing for arbitrarily nested quantifications over program traces. Despite their importance in security, there are relatively few formalizations that consider hyperproperties. Antonopoulos et al. [19] introduce a relational variant of Kleene Algebra with Tests, called BiKAT, which allows reasoning about for all there exists properties. They prove the soundness of their approach using Rocq. Dardinier and Müller [100] introduce Hyper Hoare Logic, and use Isabelle to prove soundness and completeness of the proof system. Gladshtein et al. [121] introduce the Logic for Graceful Tensor Manipulation, a separation hyperlogic for reasoning about structured data. Their logic is formalized in Rocq.

19.6 Secure Compilation Secure compilation is a broad area of research that aims to guarantee that low-level programs output by compilers are secure. This entails proving that low-level programs are protected against common forms of vulnerabilities, which are typically modeled by safety policies, and verify security policies, including information flow and resource control. In principle, compilers can guarantee these protections by mitigation or by preservation. In the first case, the compiler carries analyses and passes that ensure the desired property, whereas in the second case, the compiler assumes that the source program satisfies the desired property, and ensures that the property is preserved by compilation. Unfortunately, compilers are typically not designed with security in mind, and there are documented examples of compilers that do not enforce the stated policies and do not carry security properties from source to generated programs, see for instance [102, 204]. These examples illustrate the challenges of preserving security during compilation.

19 Formalization of Security

9

19.6.1 Definitional Works and General Frameworks Defining secure compilation is nontrivial: indeed, the classic notion of refinement used in the definition of compiler correctness does not preserve security properties. Abadi [2] was among the first to popularize the idea that secure compilation could be understood through the lens of full abstraction, a notion that was originally introduced by Plotkin [189] for relating observational equivalence and denotational equality, and used by Mitchell [162] to compare notions of program equivalence. Specifically, given a notion of equivalence on a source language and a notion of program equivalence on a target language, a mapping from source to target programs is fully abstract if and only if it preserves and respects equivalence. Abadi [2] showcases the potential and obstacles of full abstraction, and suggests other alternative approaches, including preservation of security-type systems. Although full abstraction remains a desirable property for compilers, Parrow [182], Gorla and Nestmann [126], and Patrigani and Garg [183] highlight some shortcomings of this notion. In particular, Patrigani and Garg [183] show an example of a fully abstract compiler that fails to preserve confidentiality. In addition, Patrigani and Garg [183] put forward a general criterion, called trace-preserving compilation, for preserving all safety hyperproperties. The landscape of secure compilation is further explored by Abate et al. [5], and by Abate et al. [4]. These works introduce different criteria for secure compilation and compare their relative strengths. In many cases, they also provide sufficient conditions and alternative characterizations for these criteria. Their general framework and many of the notions have been formalized in Rocq and used to reason about specific compilers. Proof-carrying code [169] popularized the idea of generating machine-checked proofs that low-level programs satisfy safety and security policies. Foundational proof-carrying code [21] is a form of proof-carrying code that uses a proof assistant to minimize the trusted computing base and prove that programs satisfy the required policies relative to a machine-checked formalization of program semantics. They illustrate their approach for a small language using the Twelf prover. Syntactic foundational proof-carrying code [135] is an alternative approach that does not require building complex program semantics. In general, these approaches are focused on trace properties rather than security properties. The aforementioned works consider programs in isolation. Abate et al. [3] introduce secure compartmentalizing compilation, a relative notion which ensures that compilation does not increase the insecurity of programs with compromised components. Compartmentalizing compilation notably differs from other works of correct and secure compilation, whose guarantees are traditionally restricted to safe source programs. They use Rocq to verify secure compartmentalizing compilation from a core language with unsafe behaviors to a simple machine with built-in compartmentalization. Their work introduces new techniques, including a recomposition lemma, that allows to structure compiler correctness proofs. Later, El-Korashy et al. [106] establish a similar result for a richer language for a language with mechanisms to share and dereference safe pointers across components. Their work also introduces

10

Gilles Barthe

new simulation techniques that are used to extend the recomposition lemma to this richer setting.

19.6.2 Compiler-Based Enforcement and Mitigations The aforementioned efforts are targeted at understanding the complex landscape of secure compilation. As such, their main results are not tied to a specific compiler, nor to a specific security property. In contrast, other works formally establish mitigation or enforcement for specific settings. Jinja [148] and CertiCartes [38] are Isabelle and Rocq formalizations of sequential fragments of the Java virtual machine and include machine-checked proofs of correctness of the bytecode verifiers. SoftBound [167] is a LLVM-based transform that enforces spatial safety of C programs by inserting runtime bound checks. Its design is formalized in Rocq and validated against an operational semantics of C programs. ARMor [231] is a certifying compiler that ensures memory safety and control integrity of ARM code. ARMor uses a formally verified program logic atop a semantics of ARM instructions to discharge proof obligations within HOL. RockSalt [164] is a formally verified checker to enforce that binary programs respect Google’s Native Client (NaCl) policy. RockSalt is written in Rocq, and is formally verified against an operational semantics of x86. KCofi [96] is a system that ensures control flow integrity for commodity operating systems. Its design is formalized in Rocq and proved correct relative to an operational semantics of the KCofi virtual machine. CompCertSFI [63] is an extension of CompCert that enforces correct sandboxing; it comes with a formal proof that compiled programs verify the sandboxing policy. CertrBPF [229] uses the CompCert compiler to generate a formally verified verifier for eBPF virtual machine. Some security-enhancing transformations have complex security proofs that go beyond the typical scope of secure compilation, by requiring, e.g., probabilistic arguments. In this case, it is common to prove only correctness of the transformation. For instance, Fournet, Keller, and Laporte [114] prove correctness of a variant of CompCert with a backend to circuits used for verifiable computation. Monniaux [163] extends the CompCert compiler with support for stack canaries and pointer authentication. He then uses simulations to prove that both passes preserve the semantics of programs.

19.6.3 Information Flow and Resource Control Policies One specific line of research within secure compilation focuses on preservation of side-channel countermeasures. It is well known that mainstream compilers break constant-time by introducing branching statements, or to a lesser extent secret-

19 Formalization of Security

11

dependent memory accesses. On the other hand, preservation of side-channel countermeasures would allow developers to use existing analysis and mitigation tools, which are often developed for source programs or intermediate representations, without worrying about potential issues introduced by the compiler. A perhaps surprising outcome is that existing verified compilers mainly preserve constant-time. In particular, there are mechanized proofs that a slightly modified version of the CompCert compiler and the Jasmin compiler (Section 19.7.5.5) preserve constanttime [35, 43, 44]. Recently, Arranz-Olmos et al. [179] extend the Jasmin compiler with stack zeroization, a security of countermeasure that overwrites data before returning from a sensitive computation. Stack zeroization guarantees absence of leakage in a stronger attacker model in which an attacker sees the values of the stack upon function return. Another specific line of research within secure compilation focuses on preservation of resource consumption. The goal here is mainly to show that resource usage can be estimated (upper-bounded) correctly at source level. An alternative is to estimate directly the cost of generated code without analyzing the source code. Blazy, Maronese, and Pichardie [66] formalize a worst-case execution time (WCET) analysis on top of the CompCert compiler. Amadio et al. [14] develop an end-to-end framework to prove space and time bounds for an 8-bit CPU. The core of their framework is a formally verified compiler, which guarantees that the results of the source analysis are sound with respect to a cost model of machine code. Following a similar approach, Carbonneaux, Hoffmann, Ramananandro, and Shao [82] instrument the CompCert compiler to prove stack-space bounds for machine code. Their formalization includes a quantitative program logic to reason about stackspace bounds at source level and a certified transformer that turns the bounds obtained by source-level reasoning into valid bounds for machine code. Besson, Blazy, and Wilke [64] prove a similar result using a more precise memory model for CompCert; Wang, Wilke, and Shao [224] further refine their approach to support finegrained stack policies. Similar results have been formally verified for other certified compilers including CakeML [125] and Jasmin [9] compilers. More recently, Paraskevopoulou and Appel [180] use Rocq to prove that closure conversion is safe for space (and time) bounds. One key novelty of their work is a notion of logical relation that is compatible with garbage collection. Finally, several works consider secure compilation to capability-based machines. For instance, Georges, Trieu, and Birkedal [120] use the Iris framework for proving full abstraction for the “overlay” semantics of a capability-based language.

19.7 Cryptography Cryptography is an essential component for building secure systems, and arguably one that comes with the strongest mathematical guarantees. It is therefore highly desirable to formally verify claims of security guarantees of cryptographic designs.

12

Gilles Barthe

19.7.1 Security Proofs in Computational Model Goldwasser and Micali [124] introduce the computational model, which underlies the overwhelming majority of modern cryptographic proofs. In this model, adversaries are probabilistic computations with oracle accesses and their interactions with cryptographic systems are also described by probabilistic computations called security experiments. Such experiments are used to measure the security of a cryptographic system; typically, one wants to show that every “resource-bounded” adversary has a “small” probability of winning the security experiment. Making this statement precise requires one to define resource-bounded adversaries, and leads to different settings. Broadly speaking, cryptographic proofs are typically carried in one of two settings: information-theoretic or computational. In the information-theoretic setting, one restricts the number of oracle queries that can be performed by the adversary, and one upper-bounds the winning probability of an adversary by an algebraic expression that depends on the number of oracle queries. In the computational setting, one additionally restricts the computational power of the adversary, and one reduces security of the cryptographic construction to the security of a problem that is assumed to be computationally hard. These reductionist statements are typically of the form: for every adversary A against the security of the cryptographic scheme S, there exists a solver B for some hard problem P such that the winning probability pA of A is upper-bounded as a function of the winning probability pB of B. Moreover, the execution time tB of B is upper-bounded by a function of the execution time tA of A . In the ideal setting, pA ≤ pB + ϵ, and tB ≤ tA + δ, with ϵ and δ being very small. In this case, the reduction is tight. However, there are sometimes multiplicative factors that make the reduction looser. Note that in general, B invokes A as a subroutine, and both δ and ϵ will depend on the number of oracle queries that can be performed by the adversaries. Further note that there may be several reductions, which for instance make different complexity trade-offs—smaller ϵ, larger δ. Moreover, the reductions can involve multiple hard problems. Finally, note that our exemplary reductionist statement above expresses concrete bounds, which may be more relevant for practical purposes. However, cryptographers also like to reason about asymptotic security, in which cases one requires that A and B execute in probabilistic polynomial-time, and prove that the winning probability of A is negligible, assuming that the winning probability of B is negligible. In all cases, the notions of polynomial-time and negligibility are set relative to a security parameter by which the experiments are (uniformly) parameterized. Reductionist proofs are complex and error-prone. To tame their the complexity, cryptographers [57, 201] have developed and adopted a code-based approach, where probabilistic experiments are written as probabilistic programs, and reductionist proofs are decomposed into a sequence of small steps. In an inspirational work, Halevi [134] suggests the possibility of mechanizing these proofs.

19 Formalization of Security

13

19.7.1.1 CertiCrypt and EasyCrypt CertiCrypt [40] is among the first and most complete formalizations of provable security in a proof assistant—see also Affeldt et al. [6] and Nowak [177] for contemporary but less developed efforts. In a nutshell, CertiCrypt is a Rocq library that formalizes many ideas and techniques of the computational model. First of all, CertiCrypt provides a deep embedding of a probabilistic language with adversarial computations, with a cost-instrumented semantics for modeling complexity. Then, CertiCrypt provides a rich set of tools for reasoning about adversarial computations. The main tool is an expressive program logic pRHL (probabilistic relational Hoare logic) for relating two programs with respect to relational pre- and postconditions, both modeled as shallow binary relations on program memories. Another tool is a nonrelational program logic for upper-bounding the probability of events in output distributions. Other tools include proof principles and program transformations based on dependence and dataflow analysis, and specific tactics for cryptography, including a tactic for interprocedural code motion of probabilistic assignments (also known as eager and lazy sampling) and conditional equivalence (also known as equivalence up to failure event). CertiCrypt has been used for verifying several classic examples from provable security, including encryption schemes, signature schemes, hash functions, and zero-knowledge proofs. One advantage of CertiCrypt is that it is developed as a Rocq library and therefore offers direct access to existing Rocq developments. For instance, Barthe et al. [42] build on Théry and Hanrot’s formalization of elliptic curves [218] to prove indifferentiability of a hash function into elliptic curves. Similarly, Almeida et al. [11] uses the CompCert compiler [152] to carry the security proof of RSA-OAEP to an assembly-level implementation. In addition, this work develops a technique to check that CompCert does not create timing side channels by introducing branching on secrets during compilation. EasyCrypt [41] is a domain-specific proof assistant that embeds many of the reasoning tools developed for CertiCrypt. One key difference is that EasyCrypt is developed as a standalone tool, rather than being embedded into an existing proof assistant. EasyCrypt combines a proof engine for higher-order logic, a backend to SMT (satisfiability modulo theories) solvers, and support for several program logics, including probabilistic Relational hoare logic, and logics to upper-bound the probability of events, including [23]. Program logics are “natively” embedded in the ambient logic: there is no formalization of program semantics, and as a consequence one cannot define the meaning of program logic judgments within the ambient logic. This pragmatic approach eases experimenting with new logics; for instance, EasyCrypt features a rich resource-aware module system [32]. EasyCrypt has been used to verify many examples from provable security, including encryption schemes, signatures schemes [111], hash functions, zero-knowledge protocols [113], cointossing protocols [112], distance bounding protocols [71], e-voting protocols [92], multi-party protocols [13,130,202,212], and universal composability [32,80]. EasyCrypt has also been used for verifying larger examples—e.g., a key protocol of AWS Key Management Service [10].

14

Gilles Barthe

19.7.1.2 Foundational Cryptography Framework Petcher and Morrisett [185] use Rocq to formalize the Foundational Cryptography Framework (FCF). In contrast to CertiCrypt, FCF provides a shallow embedding of a probabilistic programming language, letting users take advantage of the rich specification language of Rocq for writing cryptographic constructions and security definitions. The two approaches deliver different benefits in terms of expressiveness and automation and are difficult to compare. FCF has been used to mechanize a proof of security for a searchable symmetric encryption scheme [186] and for a proof of security of the HMAC message authentication code [228].

19.7.1.3 CryptHOL CryptHOL [52] is a formalization of constructive cryptography [158], a foundational paradigm for compositional, simulation-based security proofs in Isabelle/ HOL. CryptHOL stands out from prior works such as CertiCrypt and FCF, which are based on the code-based game-based approach. CryptHOL’s starting point is an encoding of probabilistic interactive systems using coinductive types, instead of the direct approach based on existential types. This encoding supports all basic operators on probabilistic interactive systems, including different forms of composition, and different notions of equivalence, that can be used to reason about the security of cryptographic protocols. CryptHOL also provides support for a relational program logic akin to probabilistic relational Hoare logic, and for reasoning principles such as optimistic sampling and up-to-bad reasoning, which are widely used in security proofs. The framework is used to verify indistinguishability of ElGamal, Hashed ElGamal, and other encryption schemes. Butler [76–78] use CryptHOL to verify Σprotocols, commitment protocols, oblivious transfer protocols, and secure two-party computations. An extension [50] of the basic framework explores the interplay between communication models and compositional security proofs. To this end, the authors introduce the key notion of Fused Resource Template (FRT). At a high-level, an FRT contains two parts: a core part and a rest part. The core part describes the common behavior across different communication models, while the rest part can interact with the core part in constrained ways. When instantiating an FRT, one must ensure that the specification is respected; the gain is that by doing so one obtains security guarantees automatically. This is guaranteed by composition theorems for FRTs. The benefits of the approach are illustrated through a running example on how to build a secure channel from a Diffie–Hellmann key exchange protocol.

19.7.1.4 SSProve SSProve [138] is a Rocq library for state-separating proofs [75]. A main idea of state-separating proofs is to structure experiments using a notion of package in-

19 Formalization of Security

15

spired from modules. The formalization provides proofs of the algebraic laws of packages, and of the soundness of a relational program logic for probabilistic computations. The framework is illustrated with ElGamal and PRF-based encryption and key encapsulation mechanisms. A recent work by Haselwarter et al. [137] establishes a formal connection between SSProve and Jasmin, and use the resulting framework for proving security of PRF-based encryption.

19.7.1.5 Computational Indistinguishability Logic Corbineau, Duclos, and Lakhnech [91] formalize Computational Indistinguishability Logic [37]; in contrast to prior works, this formalization focuses on oracle systems and their interactions with adversaries, without formalizing a programming language for describing probabilistic computations. The formalization has been used to verify an example of leakage-resilient cryptography.

19.7.1.6 Interactive Probabilistic Dependency Logic Gancher et al. [118] introduce IPDL (Interactive Probabilistic Dependency Logic), a Rocq library that formalizes an equational logic to reason about distributed probabilistic computations. In contrast to other formalizations, IPDL considers communication channels explicitly. This treatment leads to a compositional approach whereby properties of a protocol can be derived from its behavior along communication channels. IPDL has been used to verify several examples, including oblivious transfer and secure two-party computation.

19.7.1.7 Squirrel Squirrel [28] is a domain-specific proof assistant tailored toward the Bana–Comon approach [29]. The main idea of this approach is to axiomatize the adversary’s behavior in first-order logic. However, rather than formalizing the adversary’s capabilities, the approach is based on specifying what the adversary cannot do (e.g., distinguish between two ciphertexts). This leads to a notion of computationally complete symbolic attacker. Squirrel has been used to verify a representative set of primitives. 19.7.1.8 F⋆ Another alternative is to prove security of implementations using advanced program verification tools. Such tools feature an intrinsic proof mode, based on typechecking, and an extrinsic proof mode, which provides some basic functionalities for interactive proofs. The main advantage of these tools is that they integrate SMT solvers as backends, which can be used to discharge proof obligations.

16

Gilles Barthe

The Everest project uses the F⋆ language [214] to build verified implementations of cryptographic functions. F⋆ embeds a powerful refinement type system, and some basic mechanisms for interactive proofs. This approach carefully eschews probabilistic reasoning by replacing implementations of primitives by deterministic functionalities. The approach primarily focuses on trace properties, but support for relational reasoning is also considered [156].

19.7.2 Security Proofs against Quantum Adversaries All of the formalizations and tools discussed so far consider a classic execution model. However, there is an increasingly strong emphasis on post-quantum cryptography—i.e., classical cryptography that resists quantum adversaries and quantum cryptography. For instance, the National Institute of Standards and Technology (NIST) is currently supervising a competition to select and standardize a new set of cryptographic algorithms that can resist quantum adversaries. Mechanizing security proofs of these algorithms involve significant challenges, in particular adapting existing tools to the (post-)quantum setting. One early work in this direction is qRHL [221], which is implemented in Isabelle/HOL. The formalization has been used to prove security of the Fujasaki–Okamoto transform against postquantum adversaries [222]; this formalization is an important step toward mechanizing security proofs of several NIST candidates. qRHL supports reasoning about quantum programs. More recent projects focus on the more specific goal of proving security of classical constructions against quantum adversaries. This has the benefit of minimizing the gap with existing tools; currently, EasyCrypt and Squirrel offer support for post-quantum cryptography [31, 94].

19.7.3 Security Proofs in the Symbolic Model Groundbreaking work by Dolev and Yao [101] laid out the foundations for algorithmic verification of cryptographic protocols. Their work defines a symbolic model of cryptography, where cryptographic primitives (such as encryption and signatures) are idealized and modeled purely algebraically. In this model, the adversary can intercept, block, modify, or craft messages between parties. These interactions give the adversary some knowledge that they can exploit to recover cryptographic keys. Dolev and Yao show that in their model security of a cryptographic protocol can be decided in polynomial time. Following Lowe’s discovery [155] of a man-in-themiddle attack on the Needham–Schröder protocol, the Dolev–Yao model has been used extensively as a basis for formal verification of cryptographic protocols [30]. Broadly speaking, tools fall into two approaches: bounded tools, which typically consider a finite number of sessions and perform state-space exploration, and unbounded tools, which consider an infinite numbers of sessions, and use a combina-

19 Formalization of Security

17

tion of approaches, including deductive approaches. Early examples of unbounded tools include the NRL analyzer [160], ATHENA [206]. The NRL analyzer features interactive and automated modes, whereas ATHENA is based on a custom fully automated proof search procedure. Influential early works by Bolignano [69] and Paulson [184] take the alternative path to model the symbolic model in a proof assistant (Rocq and Isabelle/HOL, respectively). The crux of their approach is to model the knowledge of the adversary using an inductive relation. The security of a protocol is then established by showing that at the end of a protocol the knowledge of the adversary does not include secret values. These approaches have been used to verify security properties of real-world protocols [55, 56, 70]. Sprenger et al. [207, 208] formalize the Backes-Pfitzmann-Waidner model in Isabelle/HOL and use their formalization to prove security of classic protocols, including the (fixed) Needham-Schroeder protocol. Goubault-Larrecq [127] studies the problem of generating machine-checkable proofs from protocol verification in the Dolev–Yao model. Meier, Cremers, and Basin [161] implement proof-producing procedure atop a shallow embedding of a protocol execution model in Isabelle. Their procedure exploits protocol-independent invariants to achieve automation. Hess et al. [139] propose an automated approach for proving security of stateful cryptographic protocols in Isabelle. Their approach is based on abstract interpretation, and computes a fixpoint that soundly overapproximates protocol execution and can be checked automatically for attacks. Braje et al. [73] formalize a model of cryptographic protocols with built-in safety checks which ensure that trace properties can be verified without the need to reason about attacker behavior. Their model and the proof are formalized in Rocq. An alternative to proving cryptographic protocols directly is to build secure protocols by refinement. Sprenger and Basin [209] develop a refinement-based approach to reason about security of cryptographic protocols in Isabelle. A series of follow-up works instantiate their framework to obtain machine-checked security proofs of key agreement under different models [151, 210]. Klenze, Sprenger, and Basin [149] use a similar approach to formalize the security of forwarding protocols in Isabelle. Finally, Basin et al. [51] and Cremers et al. [95] develop extensions of the basic model to reason about the security of physical and distance bounding protocols in Isabelle.

19.7.4 Security Proofs in the Generic Group Model The generic group model [159, 200] is an idealized model which can be used to reason about cryptographic constructions or problems based on finite groups. One early application of the generic group model is to prove generic lower bounds for solving the discrete logarithm problem. The bounds hold for the restricted class of generic algorithms—i.e., algorithms that do not have access to the group representation. The crux of the generic group model is the Schwarz–Zippel lemma, which claims that the probability of sampling uniformly at random a root of a multivariate polyno-

18

Gilles Barthe

mial P of total degree d over a finite field F is upper-bounded by d/|F|. Barthe, Cederquist, and Tarento [36] formalize key results of the generic group model in Rocq as well as several applications, including lower bounds for solving the discrete logarithm, and proofs of ElGamal encryption. model [117] have found many novel applications, including for zero-knowledge proofs.

19.7.5 Correctness Proofs There is a large body of work that formalizes mathematical concepts that arise in cryptography. In particular, there exists several formalizations of elliptic curves in Rocq [49, 218] and Isabelle/HOL [133]. The latter formalizes Edwards elliptic curves, which play a prominent role in recently proposed cryptographic algorithms. There are also many works that use proof assistants for proving the correctness of cryptographic implementations. 19.7.5.1 µ Cryptol Cryptol, developed by Galois, is an embedded domain-specific language for writing cryptographic algorithms. Cryptol offers support for checking that programs are safe and that generated code is equivalent to its Cryptol specification. Pike, Shields, and Matthews [187] have also developed µCryptol, a compiler from a fragment of the Cryptol language to the AAMP7 microprocessor. The compiler is formally verified in ACL2.

19.7.5.2 Fiat-Crypto Erbsen et al. [107] use Rocq as a basis for Fiat-Crypto, a compiler infrastructure to produce correct-by-construction implementations of finite field and elliptic curve cryptography. At a high level, Fiat-Crypto automatically transforms mathematical descriptions of arithmetic computations into efficient, straight-line machine code. Routines generated by FIAT Crypto have been used as drop-in replacement of several previously unverified routines in BoringSSL. Erbsen et al. [108] use Fiat-Crypto to verify a formally verified bare metal server that uses elliptic curve cryptography. Hvass, Aranha, and Spitters [144] extend Fiat-Crypto to obtain high-assurance implementations of field inversion. In a different direction, Kuepper et al. [150] combine Fiat-Crypto with superoptimization techniques show further efficiency gains for P-256 scalar multiplication. The correctness of their approach relies on verified equivalence checking, which establishes semantic equivalence between the algorithms output by Fiat-Crypto and the algorithm output by the superoptimizer.

19 Formalization of Security

19

19.7.5.3 Verified Software Toolchain The Verified Software Toolchain (VST) projects uses a combination of the CompCert verified compiler with a (formally verified) program logic for C programs to verify cryptographic implementations. More specifically, C implementations of SHA256 and HMAC are proved safe and correct using a mechanization of separation logic built on top of CompCert [20, 60, 228]; in addition to functional correctness, these works establish reductionist security through a connection between CompCert with FCF. More recently, Schwabe et al. use VST to establish the correctness of the TweetNaCl implementation of Curve 25519 [197].

19.7.5.4 CryptoLine CryptoLine is an automatic tool for verifying assembly implementations of cryptographic routines. Early work [88] uses an ad hoc combination of SMT solvers and Rocq to verify the correctness of Curve 25519. This approach is subsequently refined by Tsai, Wang, and Yang [220]. Their refined approach transforms verification tasks into modular polynomial equation entailment problems, which can then be checked by computer algebra systems. Solutions of the entailment problem are encoded into certificates that are verified automatically in Rocq using computeralgebra-system-like tactics. This line of work is further developed in [219], where Tsai et al. present COQCryptoLine, a variant of CryptoLine certified in Rocq.

19.7.5.5 Jasmin Jasmin [9, 12] is a framework that aims to deliver efficient, high-assurance cryptographic implementations. The main components of the framework are the Jasmin program verification infrastructure and the Jasmin compiler. The Jasmin compiler is formally verified in Rocq, both for safety and functional correctness. This allows to reason about Jasmin programs and obtain guarantees about assembly code. The Jasmin verification infrastructure is based on EasyCrypt, via a translation of Jasmin programs to EasyCrypt.

19.7.5.6 HACL* The F⋆ language [214] and the F⋆ /Vale framework [115] have been used to develop the HACL* and EverCrypt libraries [193, 232], which have been widely deployed in popular systems.

20

Gilles Barthe

19.7.5.7 Other Approaches Ricketts el al. [194] formally verify a SSH server in Rocq. Their formalization is based on Reflex, a deeply embedded DSL with support for automated functional correctness and noninterference proofs.

19.8 Other Applications 19.8.1 Zero-Knowledge and Electronic Voting Zero-knowledge proofs are cryptographic protocols that allow a prover P to prove knowledge of a secret to a verifier V, without revealing the secret to V. The main properties of zero-knowledge proofs are soundness, completeness, and zeroknowledge; the properties respectively (and informally) state that cheating provers cannot convince verifiers, honest verifiers will accept honestly generated proofs of valid statements, and verifiers will learn nothing about the statement except its validity. Almeida et al. [7] use Isabelle/HOL as a backend to generate soundness proofs for a subclass of zero-knowledge proofs known as Σ-protocols. Subsequent work [8] builds a similar approach for a larger class of protocols, using a Rocq formalization of proofs of knowledge of preimages under group homomorphisms [45]. In both cases, the formalizations are used as a backend by a cryptographic compiler. The resulting certifying compilers take as input a logical formula and generate a protocol together with a proof of its security properties: (special) soundness, completeness, and honest verifier zero-knowledge. Haines and collaborators [131, 132] use Rocq to reason about correctness of verifiable mix nets used in electronic elections. The proof involves reasoning about zero-knowledge arguments, which is addressed through a careful modeling that eschews probabilistic reasoning.

19.8.2 Smart Contracts Smart contracts are distributed programs that execute a protocol agreed by several parties. Simple examples of smart contracts include swaps, lotteries, payments, and other transactions. Smart contracts play an important role in decentralized finance, and flaws in smart contracts can have devastating financial consequences. It makes smart contracts, and the underlying blockchains, an important target for formal verification. Hirai [140] formalizes the operational semantics of the Ethereum VM in Rocq, HOL4, and Isabelle/HOL. Amani et al. [15] formalize a program logic for EVM bytecode in Isabelle/HOL and prove its soundness with respect to Hirai’s semantics.

19 Formalization of Security

21

In a similar vein, Bernardo et al. [62] and Bernardo et al. [61] formalize the operational semantics and a sound program logic for Tezos smart contracts in Rocq. There exists similar efforts to formalize intermediate or low-level languages for smart contracts; for instance, there exists formalized semantics of the Yul language in HOL4, Isabelle/HOL, and Lean. More recently, Avigad et al. [24] propose an alternative approach to generate proofs of correctness for algebraic programs written in the Cairo language. Specifically, they use Lean to show that Cairo programs whose algebraic intermediate representations admit a solution have correct executions. Informally, these correct executions represent complete runs of a protocol between a prover and a verifier. Their approach is deployed to carry cryptocurrency exchanges. In a different vein, Nielsen and Spitters [173] use Rocq to reason about shallow embeddings of smart contracts. A more recent work by Nielsen, Annenkov, and Spitters [172] use Rocq to reason about decentralized exchanges. Applications to smart contracts have also motivated mechanizations of consensus protocols. Pîrlea and Sergey [188] prove the correctness of consensus protocols in Rocq. More generally, formalizations of distributed protocols [198] could serve as a good starting point to reason formally about smart contracts.

19.8.3 Differential Privacy Differential privacy [103] is a quantitative, mathematically rigorous notion of privacy that quantifies the amount of information leaked by a (randomized) algorithm. Differential privacy is a relational property: informally, an algorithm is differentially private if running the algorithm on two closely related inputs yields closely related distributions. Typically, inputs are databases, and two databases are closely related (or, in differential privacy jargon, adjacent) if they differ in one element. When elements are associated with individuals, differential privacy thus guarantees that the information leaked about a single individual is small. The magic of differential privacy is to guarantee individual privacy while still allowing for the possibility of statistically meaningful computations. There are many notions of closeness for distributions; these notions yield different notions of differential privacy, including vanilla differential privacy (also known as ϵ-differential privacy), approximate differential privacy (also known as ϵ, δ-differential privacy), and more recently Rényi differential privacy, which enjoys tighter composition properties. CertiPriv [46] is a Rocq library to reason about differential privacy. CertiPriv is built on top of CertiCrypt, and features an approximate probabilistic relational Hoare logic, which is proved sound with respect to a deep embedding of probabilistic programs. Later work uses EasyCrypt in a similar style, for proving security of Sparse Vector, a challenging algorithm from differential privacy [39].

22

Gilles Barthe

References 1. CHERI project. URL www.cheri-cpu.org 2. Abadi, M.: Protection in programming-language translations. In: K.G. Larsen, S. Skyum, G. Winskel (eds.) ICALP ’98, LNCS, vol. 1443, pp. 868–883. Springer (1998). URL https://doi.org/10.1007/BFb0055109 3. Abate, C., Azevedo de Amorim, A., Blanco, R., Evans, A.N., Fachini, G., Hrit, cu, C., Laurent, T., Pierce, B.C., Stronati, M., Tolmach, A.: When good components go bad: Formally secure compilation despite dynamic compromise. In: D. Lie, M. Mannan, M. Backes, X. Wang (eds.) CCS ’18, pp. 1351–1368. ACM (2018). URL https://doi.org/10.1145/3243734.3243745 4. Abate, C., Blanco, R., Ciobâcă, Ş., Durier, A., Garg, D., Hrit, cu, C., Patrignani, M., Tanter, É., Thibault, J.: An extended account of trace-relating compiler correctness and secure compilation. ACM Trans. Program. Lang. Syst. 43(4), 14:1–14:48 (2021). URL https://doi.org/10.1145/3460860 5. Abate, C., Blanco, R., Garg, D., Hrit, cu, C., Patrignani, M., Thibault, J.: Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In: CSF 2019, pp. 256–271. IEEE (2019). URL https://doi.org/10.1109/CSF.2019.00025 6. Affeldt, R., Tanaka, M., Marti, N.: Formal proof of provable security by game-playing in a proof assistant. In: W. Susilo, J.K. Liu, Y. Mu (eds.) ProvSec 2007, LNCS, vol. 4784, pp. 151–168. Springer (2007). URL https://doi.org/10.1007/978-3-540-75670-5_10 7. Almeida, J.B., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A.R., Schneider, T.: A certifying compiler for zero-knowledge proofs of knowledge based on sigma-protocols. In: D. Gritzalis, B. Preneel, M. Theoharidou (eds.) ESORICS 2010, LNCS, vol. 6345, pp. 151–167. Springer (2010). URL https://doi.org/10.1007/978-3-642-15497-3_10 8. Almeida, J.B., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Béguelin, S.Z.: Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols. In: T. Yu, G. Danezis, V.D. Gligor (eds.) CCS ’12, pp. 488–500. ACM (2012). URL https://doi.org/10.1145/2382196.2382249 9. Almeida, J.B., Barbosa, M., Barthe, G., Blot, A., Grégoire, B., Laporte, V., Oliveira, T., Pacheco, H., Schmidt, B., Strub, P.Y.: Jasmin: High-assurance and high-speed cryptography. In: B.M. Thuraisingham, D. Evans, T. Malkin, D. Xu (eds.) CCS ’17, pp. 1807–1823. ACM (2017). URL https://doi.org/10.1145/3133956.3134078 10. Almeida, J.B., Barbosa, M., Barthe, G., Campagna, M., Cohen, E., Grégoire, B., Pereira, V., Portela, B., Strub, P.Y., Tasiran, S.: A machine-checked proof of security for AWS key management service. In: L. Cavallaro, J. Kinder, X. Wang, J. Katz (eds.) CCS ’19, pp. 63–78. ACM (2019). URL https://doi.org/10.1145/3319535.3354228 11. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations. In: A.R. Sadeghi, V.D. Gligor, M. Yung (eds.) CCS ’13, pp. 1217–1230. ACM (2013). URL https://doi.org/10.1145/2508859.2516652 12. Almeida, J.B., Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Laporte, V., Oliveira, T., Strub, P.Y.: The last mile: High-assurance and high-speed cryptographic implementations. In: SP 2020, pp. 965–982. IEEE (2020). URL https://doi.org/10.1109/SP40000.2020.00028 13. Almeida, J.B., Barbosa, M., Correia, M.L., Eldefrawy, K., Graham-Lengrand, S., Pacheco, H., Pereira, V.: Machine-checked ZKP for NP relations: Formally verified security proofs and implementations of mpc-in-the-head. In: Y. Kim, J. Kim, G. Vigna, E. Shi (eds.) CCS ’21, pp. 2587–2600. ACM (2021). URL https://doi.org/10.1145/3460120.3484771 14. Amadio, R.M., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D.P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C.S., Stark, I., Tranquilli, P.: Certified Complexity (CerCo). In: U.D. Lago, R. Peña (eds.) FOPARA 2013, LNCS, vol. 8552, pp. 1–18. Springer (2013). URL https://doi.org/10.1007/978-3-319-12466-7_1

19 Formalization of Security

23

15. Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: J. Andronick, A.P. Felty (eds.) CPP 2018, pp. 66–77. ACM (2018). URL https://doi.org/10.1145/3167084 16. Amtoft, T., Dodds, J., Zhang, Z., Appel, A.W., Beringer, L., Hatcliff, J., Ou, X., Cousino, A.: A certificate infrastructure for machine-checked proofs of conditional information flow. In: P. Degano, J.D. Guttman (eds.) POST 2012, LNCS, vol. 7215, pp. 369–389. Springer (2012). URL https://doi.org/10.1007/978-3-642-28641-4_20 17. Andronick, J., Chetali, B., Ly, O.: Using Coq to verify Java Card applet isolation properties. In: D. Basin, B. Wolff (eds.) TPHOLs 2003, LNCS, vol. 2758, pp. 335–351. Springer (2003). URL https://doi.org/10.1007/10930755_22 18. Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal verification of security properties of smart card embedded source code. In: J.S. Fitzgerald, I.J. Hayes, A. Tarlecki (eds.) FM 2005, LNCS, vol. 3582, pp. 302–317. Springer (2005). URL https://doi.org/10.1007/11526841_21 19. Antonopoulos, T., Koskinen, E., Le, T.C., Nagasamudram, R., Naumann, D.A., Ngo, M.: An algebra of alignment for relational verification. Proc. ACM Program. Lang. 7(POPL), 573–603 (2023). URL https://doi.org/10.1145/3571213 20. Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1–7:31 (2015). URL https://doi.org/10.1145/2701415 21. Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: M.N. Wegman, T.W. Reps (eds.) POPL 2000, pp. 243–253. ACM (2000). URL https://doi.org/10.1145/325694.325727 22. Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411–445 (2007). URL https://doi.org/10.1016/j.tcs.2007.09.003 23. Avanzini, M., Barthe, G., Grégoire, B., Moser, G., Vanoni, G.: Hopping proofs of expectation-based properties: Applications to skiplists and security proofs. Proc. ACM Program. Lang. 8(OOPSLA) (2024) 24. Avigad, J., Goldberg, L., Levit, D., Seginer, Y., Titelman, A.: A verified algebraic representation of Cairo program execution. In: A. Popescu, S. Zdancewic (eds.) CPP ’22, pp. 153–165. ACM (2022). URL https://doi.org/10.1145/3497775.3503675 25. Azevedo de Amorim, A., Collins, N., DeHon, A., Demange, D., Hrit, cu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. J. Comput. Secur. 24(6), 689–734 (2016). URL https://doi.org/10.3233/JCS-15784 26. Azevedo de Amorim, A., Dénès, M., Giannarakis, N., Hrit, cu, C., Pierce, B.C., Spector-Zabusky, A., Tolmach, A.: Micro-policies: Formally verified, tag-based security monitors. In: SP 2015, pp. 813–830. IEEE (2015). URL https://doi.org/10.1109/SP.2015.55 27. Azevedo de Amorim, A., Hrit, cu, C., Pierce, B.C.: The meaning of memory safety. In: L. Bauer, R. Küsters (eds.) POST 2018, LNCS, vol. 10804, pp. 79–105. Springer (2018). URL https://doi.org/10.1007/978-3-319-89722-6_4 28. Baelde, D., Delaune, S., Jacomme, C., Koutsos, A., Moreau, S.: An interactive prover for protocol verification in the computational model. In: SP 2021, pp. 537–554. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00078 29. Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: G.J. Ahn, M. Yung, N. Li (eds.) CCS ’14, pp. 609–620. ACM (2014). URL https://doi.org/10.1145/2660267.2660276 30. Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., Parno, B.: SoK: Computer-aided cryptography. In: SP 2021, pp. 777–795. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00008 31. Barbosa, M., Barthe, G., Fan, X., Grégoire, B., Hung, S.H., Katz, J., Strub, P.Y., Wu, X., Zhou, L.: EasyPQC: Verifying post-quantum cryptography. In: Y. Kim, J. Kim, G. Vigna, E. Shi (eds.) CCS ’21, pp. 2564–2586. ACM (2021). URL https://doi.org/10.1145/3460120.3484567

24

Gilles Barthe

32. Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Strub, P.Y.: Mechanized proofs of adversarial complexity and application to universal composability. In: Y. Kim, J. Kim, G. Vigna, E. Shi (eds.) CCS ’21, pp. 2541–2563. ACM (2021). URL https://doi.org/10.1145/3460120.3484548 33. Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally verifying isolation and availability in an idealized model of virtualization. In: M.J. Butler, W. Schulte (eds.) FM 2011, LNCS, vol. 6664, pp. 231–245. Springer (2011). URL https://doi.org/10.1007/978-3-642-21437-0_19 34. Barthe, G., Betarte, G., Campo, J.D., Luna, C.D., Pichardie, D.: System-level non-interference for constant-time cryptography. In: G.J. Ahn, M. Yung, N. Li (eds.) CCS ’14, pp. 1267–1279. ACM (2014). URL https://doi.org/10.1145/2660267.2660283 35. Barthe, G., Blazy, S., Grégoire, B., Hutin, R., Laporte, V., Pichardie, D., Trieu, A.: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL), 7:1–7:30 (2020). URL https://doi.org/10.1145/3371075 36. Barthe, G., Cederquist, J., Tarento, S.: A machine-checked formalization of the generic model and the random oracle model. In: D.A. Basin, M. Rusinowitch (eds.) IJCAR 2004, LNCS, vol. 3097, pp. 385–399. Springer (2004). URL https://doi.org/10.1007/978-3-540-25984-8_29 37. Barthe, G., Daubignard, M., Kapron, B.M., Lakhnech, Y.: Computational indistinguishability logic. In: E. Al-Shaer, A.D. Keromytis, V. Shmatikov (eds.) CCS ’10, pp. 375–386. ACM (2010). URL https://doi.org/10.1145/1866307.1866350 38. Barthe, G., Dufay, G.: A tool-assisted framework for certified bytecode verification. In: M. Wermelinger, T. Margaria (eds.) FASE 2004, LNCS, vol. 2984, pp. 99–113. Springer (2004). URL https://doi.org/10.1007/978-3-540-24721-0_7 39. Barthe, G., Fong, N., Gaboardi, M., Grégoire, B., Hsu, J., Strub, P.Y.: Advanced probabilistic couplings for differential privacy. In: E.R. Weippl, S. Katzenbeisser, C. Kruegel, A.C. Myers, S. Halevi (eds.) CCS ’16, pp. 55–67. ACM (2016). URL https://doi.org/10.1145/2976749.2978391 40. Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Z. Shao, B.C. Pierce (eds.) POPL 2009, pp. 90–101. ACM (2009). URL https://doi.org/10.1145/1480881.1480894 41. Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: P. Rogaway (ed.) CRYPTO 2011, LNCS, vol. 6841, pp. 71–90. Springer (2011). URL https://doi.org/10.1007/978-3-642-22792-9_5 42. Barthe, G., Grégoire, B., Heraud, S., Olmedo, F., Béguelin, S.Z.: Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21(6), 881–917 (2013). URL https://doi.org/10.3233/JCS-130476 43. Barthe, G., Grégoire, B., Laporte, V.: Secure compilation of side-channel countermeasures: The case of cryptographic “constant-time”. In: CSF 2018, pp. 328–343. IEEE (2018). URL https://doi.org/10.1109/CSF.2018.00031 44. Barthe, G., Grégoire, B., Laporte, V., Priya, S.: Structured leakage and applications to cryptographic constant-time and cost. In: Y. Kim, J. Kim, G. Vigna, E. Shi (eds.) CCS ’21, pp. 462–476. ACM (2021). URL https://doi.org/10.1145/3460120.3484761 45. Barthe, G., Hedin, D., Béguelin, S.Z., Grégoire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: CSF 2010, pp. 246–260. IEEE (2010). URL https://doi.org/10.1109/CSF.2010.24 46. Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: J. Field, M. Hicks (eds.) POPL 2012, pp. 97–110. ACM (2012). URL https://doi.org/10.1145/2103656.2103670 47. Barthe, G., Nieto, L.P.: Secure information flow for a concurrent language with scheduling. J. Comput. Sec. 15(6), 647–689 (2007). URL http://content.iospress.com/articles/journal-of-computer-security/jcs295 48. Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: R.D. Nicola (ed.) ESOP 2007, LNCS, vol. 4421, pp. 125–140. Springer (2007). URL https://doi.org/10.1007/978-3-540-71316-6_10

19 Formalization of Security

25

49. Bartzia, E.I., Strub, P.Y.: A formal library for elliptic curves in the Coq proof assistant. In: G. Klein, R. Gamboa (eds.) ITP 2014, LNCS, vol. 8558, pp. 77–92. Springer (2014). URL https://doi.org/10.1007/978-3-319-08970-6_6 50. Basin, D., Lochbihler, A., Maurer, U., Sefidgar, S.: Abstract modeling of system communication in constructive cryptography using CryptHOL. In: CSF 2021, pp. 592–607. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00047 51. Basin, D.A., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Secur. 14(2), 16:1–16:28 (2011). URL https://doi.org/10.1145/2019599.2019601 52. Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: Game-based proofs in higher-order logic. J. Cryptol. 33(2), 494–566 (2020). URL https://doi.org/10.1007/s00145-019-09341-z 53. Bauereiss, T., Campbell, B., Sewell, T., Armstrong, A., Esswood, L., Stark, I., Barnes, G., Watson, R.N.M., Sewell, P.: Verified security for the morello capability-enhanced prototype arm architecture. In: I. Sergey (ed.) ESOP 2022, LNCS, vol. 13240, pp. 174–203. Springer (2022). URL https://doi.org/10.1007/978-3-030-99336-8_7 54. Bauereiß, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: Cosmedis: A distributed social media platform with formally verified confidentiality guarantees. In: SP 2017, pp. 729–748. IEEE (2017). URL https://doi.org/10.1109/SP.2017.24 55. Bella, G.: Formal Correctness of Security Protocols. Information Security and Cryptography. Springer (2007). URL https://doi.org/10.1007/978-3-540-68136-6 56. Bella, G., Paulson, L.C., Massacci, F.: The verification of an industrial payment protocol: The SET purchase phase. In: V. Atluri (ed.) CCS ’02, pp. 12–20. ACM (2002). URL https://doi.org/10.1145/586110.586113 57. Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: S. Vaudenay (ed.) EUROCRYPT 2006, LNCS, vol. 4004, pp. 409–426. Springer (2006). URL https://doi.org/10.1007/11761679_25 58. Benzinger, R.: Automated complexity analysis of nuprl extracted programs journal of functional programming. J. Funct. Program. 11(1), 3–31 (2001). URL https://doi.org/10.1017/s0956796800003865 59. Beringer, L.: End-to-end multilevel hybrid information flow control. In: R. Jhala, A. Igarashi (eds.) APLAS 2012, LNCS, vol. 7705, pp. 50–65. Springer (2012). URL https://doi.org/10.1007/978-3-642-35182-2_5 60. Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: J. Jung, T. Holz (eds.) USENIX Security ’15, pp. 207–221. USENIX Association (2015). URL https://www.usenix.org/conference/usenixsecurity15/ technical-sessions/presentation/beringer 61. Bernardo, B., Cauderlier, R., Claret, G., Jakobsson, A., Pesin, B., Tesson, J.: Making Tezos smart contracts more reliable with Coq. In: T. Margaria, B. Steffen (eds.) ISoLA 2020, Part III, LNCS, vol. 12478, pp. 60–72. Springer (2020). URL https://doi.org/10.1007/978-3-030-61467-6_5 62. Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In: E. Sekerinski, N. Moreira, J.N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J.C. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro, D. Delmas (eds.) FM 2019, Part I, LNCS, vol. 12232, pp. 368–379. Springer (2019). URL https://doi.org/10.1007/978-3-030-54994-7_28 63. Besson, F., Blazy, S., Dang, A., Jensen, T.P., Wilke, P.: Compiling sandboxes: Formally verified software fault isolation. In: L. Caires (ed.) ESOP 2019, LNCS, vol. 11423, pp. 499–524. Springer (2019). URL https://doi.org/10.1007/978-3-030-17184-1_18 64. Besson, F., Blazy, S., Wilke, P.: CompCertS: A memory-aware verified C compiler using pointer as integer semantics. In: M. Ayala-Rincón, C.A. Muñoz (eds.) ITP 2017, LNCS, vol. 10499, pp. 81–97. Springer (2017). URL https://doi.org/10.1007/978-3-319-66107-0_6

26

Gilles Barthe

65. Betarte, G., Giménez, E., Loiseaux, C., Chetali, B.: FORMAVIE: Formal modelling and verification of the JavaCard 2.1.1 security architecture. In: e-Smart 2002, pp. 213–231 (2002) 66. Blazy, S., Maroneze, A.O., Pichardie, D.: Formal verification of loop bound estimation for WCET analysis. In: E. Cohen, A. Rybalchenko (eds.) VSTTE 2013, LNCS, vol. 8164, pp. 281–303. Springer (2013). URL https://doi.org/10.1007/978-3-642-54108-7_15 67. Bohannon, A.: Foundations of web script security. PhD thesis, University of Pennsylvania (2012) 68. Bohannon, A., Pierce, B.C., Sjöberg, V., Weirich, S., Zdancewic, S.: Reactive noninterference. In: E. Al-Shaer, S. Jha, A.D. Keromytis (eds.) CCS ’09, pp. 79–90. ACM (2009). URL https://doi.org/10.1145/1653662.1653673 69. Bolignano, D.: An approach to the formal verification of cryptographic protocols. In: L. Gong, J. Stearn (eds.) CCS ’96, pp. 106–118. ACM (1996). URL https://doi.org/10.1145/238168.238196 70. Bolignano, D.: Towards the formal verification of electronic commerce protocols. In: CSFW ’97, pp. 133–147. IEEE (1997). URL https://doi.org/10.1109/CSFW.1997.596802 71. Boureanu, I., Dragan, C.C., Dupressoir, F., Gérault, D., Lafourcade, P.: Mechanised models and proofs for distance-bounding. In: CSF 2021, pp. 1–16. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00049 72. Bracevac, O., Gay, R., Grewe, S., Mantel, H., Sudbrock, H., Tasch, M.: An Isabelle/HOL formalization of the modular assembly kit for security properties. Arch. Formal Proofs 2018 (2018). URL https://www.isa-afp.org/entries/Modular_Assembly_Kit_Security.html 73. Braje, T.M., Lee, A.R., Wagner, A., Kaiser, B., Park, D., Kalke, M., Cunningham, R.K., Chlipala, A.: Adversary safety by construction in a language of cryptographic protocols. In: CSF 2022, pp. 412–427. IEEE (2022). URL https://doi.org/10.1109/CSF54842.2022.9919638 74. Brucker, A.D., Brügger, L., Wolff, B.: Formal firewall conformance testing: An application of test and proof techniques. Softw. Test. Verif. Reliab. 25(1), 34–71 (2015). URL https://doi.org/10.1002/stvr.1544 75. Brzuska, C., Delignat-Lavaud, A., Fournet, C., Kohbrok, K., Kohlweiss, M.: State separation for code-based game-playing proofs. In: T. Peyrin, S.D. Galbraith (eds.) ASIACRYPT 2018, Part III, LNCS, vol. 11274, pp. 222–249. Springer (2018). URL https://doi.org/10.1007/978-3-030-03332-3_9 76. Butler, D., Aspinall, D., Gascón, A.: How to simulate it in Isabelle: Towards formal proof for secure multi-party computation. In: M. Ayala-Rincón, C.A. Muñoz (eds.) ITP 2017, LNCS, vol. 10499, pp. 114–130. Springer (2017). URL https://doi.org/10.1007/978-3-319-66107-0_8 77. Butler, D., Aspinall, D., Gascón, A.: Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. In: J. Blanchette, C. Hrit, cu (eds.) CPP 2020, pp. 229–243. ACM (2020). URL https://doi.org/10.1145/3372885.3373815 78. Butler, D., Lochbihler, A., Aspinall, D., Gascón, A.: Formalising Σ-protocols and commitment schemes using CryptHOL. J. Autom. Reason. 65(4), 521–567 (2021). URL https://doi.org/10.1007/s10817-020-09581-w 79. Cachera, D., Jensen, T.P., Pichardie, D., Schneider, G.: Certified memory usage analysis. In: J.S. Fitzgerald, I.J. Hayes, A. Tarlecki (eds.) FM 2005, LNCS, vol. 3582, pp. 91–106. Springer (2005). URL https://doi.org/10.1007/11526841_8 80. Canetti, R., Stoughton, A., Varia, M.: EasyUC: Using EasyCrypt to mechanize proofs of universally composable security. In: CSF 2019, pp. 167–183. IEEE (2019). URL https://doi.org/10.1109/CSF.2019.00019 81. Capretta, V., Stepien, B., Felty, A.P., Matwin, S.: Formal correctness of conflict detection for firewalls. In: P. Ning, V. Atluri, V.D. Gligor, H. Mantel (eds.) FMSE 2007, pp. 22–30. ACM (2007). URL https://doi.org/10.1145/1314436.1314440

19 Formalization of Security

27

82. Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: M.F.P. O’Boyle, K. Pingali (eds.) PLDI ’14, pp. 270–281. ACM (2014). URL https://doi.org/10.1145/2594291.2594301 83. Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: R. Majumdar, V. Kuncak (eds.) CAV 2017, Part II, LNCS, vol. 10427, pp. 64–85. Springer (2017). URL https://doi.org/10.1007/978-3-319-63390-9_4 84. Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: D. Grove, S.M. Blackburn (eds.) PLDI ’15, pp. 467–478. ACM (2015). URL https://doi.org/10.1145/2737924.2737955 85. Charguéraud, A.: A modern eye on separation logic for sequential programs. Habilitation thesis (2023). URL https://tel.archives-ouvertes.fr/tel-04076725 86. Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: C. Urban, X. Zhang (eds.) ITP 2015, LNCS, vol. 9236, pp. 137–153. Springer (2015). URL https://doi.org/10.1007/978-3-319-22102-1_9 87. Charguéraud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. 62(3), 331–365 (2019). URL https://doi.org/10.1007/s10817-017-9431-7 88. Chen, Y.F., Hsu, C.H., Lin, H.H., Schwabe, P., Tsai, M.H., Wang, B.Y., Yang, B.Y., Yang, S.Y.: Verifying Curve25519 software. In: G.J. Ahn, M. Yung, N. Li (eds.) CCS ’14, pp. 299–309. ACM (2014). URL https://doi.org/10.1145/2660267.2660370 89. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010). URL https://doi.org/10.3233/JCS-2009-0393 90. Cock, D.A.: Verifying probabilistic correctness in isabelle with pgcl. In: F. Cassez, R. Huuck, G. Klein, B. Schlich (eds.) SSV ’12, EPTCS, vol. 102, pp. 167–178 (2012). URL https://doi.org/10.4204/EPTCS.102.15 91. Corbineau, P., Duclos, M., Lakhnech, Y.: Certified security proofs of cryptographic protocols in the computational model: An application to intrusion resilience. In: J.P. Jouannaud, Z. Shao (eds.) CPP 2011, LNCS, vol. 7086, pp. 378–393. Springer (2011). URL https://doi.org/10.1007/978-3-642-25379-9_27 92. Cortier, V., Dragan, C.C., Dupressoir, F., Schmidt, B., Strub, P.Y., Warinschi, B.: Machine-checked proofs of privacy for electronic voting protocols. In: SP 2017, pp. 993–1008. IEEE (2017). URL https://doi.org/10.1109/SP.2017.28 93. Costanzo, D., Shao, Z., Gu, R.: End-to-end verification of information-flow security for C and assembly programs. In: C. Krintz, E.D. Berger (eds.) PLDI ’16, pp. 648–664. ACM (2016). URL https://doi.org/10.1145/2908080.2908100 94. Cremers, C., Fontaine, C., Jacomme, C.: A logic and an interactive prover for the computational post-quantum security of protocols. In: SP 2022, pp. 125–141. IEEE (2022). URL https://doi.org/10.1109/SP46214.2022.9833800 95. Cremers, C.J.F., Rasmussen, K.B., Schmidt, B., Capkun, S.: Distance hijacking attacks on distance bounding protocols. In: SP 2012, pp. 113–127. IEEE (2012). URL https://doi.org/10.1109/SP.2012.17 96. Criswell, J., Dautenhahn, N., Adve, V.S.: Kcofi: Complete control-flow integrity for commodity operating system kernels. In: SP 2014, pp. 292–307. IEEE (2014). URL https://doi.org/10.1109/SP.2014.26 97. Cutler, J.W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Ioannidis, E., Kastner, J., Mamat, A., McAdams, D., McCutchen, M., Rungta, N., Torlak, E., Wells, A.: Cedar: A new language for expressive, fast, safe, and analyzable authorization (extended version). Proc. ACM Program. Lang. 8(OOPSLA) (2024). URL https://doi.org/10.1145/3649835 98. Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple arm-based separation kernel. In: A.R. Sadeghi, V.D. Gligor, M. Yung (eds.) CCS ’13, pp. 223–234. ACM (2013). URL https://doi.org/10.1145/2508859.2516702

28

Gilles Barthe

99. Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: G.C. Necula, P. Wadler (eds.) POPL 2008, pp. 133–144. ACM (2008). URL https://doi.org/10.1145/1328438.1328457 100. Dardinier, T., Müller, P.: Hyper Hoare Logic: (Dis-)proving program hyperproperties. Proc. ACM Program. Lang. 8(PLDI) (2024). URL https://doi.org/10.48550/arXiv.2301.10037 101. Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983). URL https://doi.org/10.1109/TIT.1983.1056650 102. D’Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21-22, 2015, pp. 73–87. IEEE (2015). URL https://doi.org/10.1109/SPW.2015.33 103. Dwork, C., Roth, A.: The algorithmic foundations of differential privacy. Found. Trends Theor. Comput. Sci. 9(3–4), 211–407 (2014). URL https://doi.org/10.1561/0400000042 104. Eberl, M.: Proving divide and conquer complexities in Isabelle/HOL. J. Autom. Reason. 58(4), 483–508 (2017). URL https://doi.org/10.1007/s10817-016-9378-0 105. Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. J. Autom. Reason. 64(5), 879–910 (2020). URL https://doi.org/10.1007/s10817-020-09545-0 106. El-Korashy, A., Blanco, R., Thibault, J., Durier, A., Garg, D., Hrit, cu, C.: SecurePtrs: Proving secure compilation with data-flow back-translation and turn-taking simulation. In: CSF 2022, pp. 64–79. IEEE (2022). URL https://doi.org/10.1109/CSF54842.2022.9919680 107. Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic—with proofs, without compromises. In: SP 2019, pp. 1202–1219. IEEE (2019). URL https://doi.org/10.1109/SP.2019.00005 108. Erbsen, A., Philipoom, J., Jamner, D., Lin, A., Gruetter, S., Pit-Claudel, C., Chlipala, A.: Foundational integration verification of a cryptographic server. Proc. ACM Program. Lang. 8(PLDI), 1704–1729 (2024). URL https://doi.org/10.1145/3656446 109. Ernst, G., Murray, T.: SecCSL: Security concurrent separation logic. In: I. Dillig, S. Tasiran (eds.) CAV 2019, LNCS, vol. 11562, pp. 208–230. Springer (2019). URL https://doi.org/10.1007/978-3-030-25543-5_13 110. Finkbeiner, B.: Logics and algorithms for hyperproperties. ACM SIGLOG News 10(2), 4–23 (2023). URL https://doi.org/10.1145/3610392.3610394 111. Firsov, D., Lakk, H., Truu, A.: Verified multiple-time signature scheme from one-time signatures and timestamping. In: CSF 2021, pp. 1–13. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00051 112. Firsov, D., Unruh, D.: Reflection, rewinding, and coin-toss in EasyCrypt. In: A. Popescu, S. Zdancewic (eds.) CPP ’22, pp. 166–179. ACM (2022). URL https://doi.org/10.1145/3497775.3503693 113. Firsov, D., Unruh, D.: Zero-knowledge in EasyCrypt. In: CSF 2023, pp. 1–16. IEEE (2023). URL https://doi.org/10.1109/CSF57540.2023.00015 114. Fournet, C., Keller, C., Laporte, V.: A certified compiler for verifiable computing. In: CSF 2016, pp. 268–280. IEEE (2016). URL https://doi.org/10.1109/CSF.2016.26 115. Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. Proc. ACM Program. Lang. 3(POPL), 63:1–63:30 (2019). URL https://doi.org/10.1145/3290376 116. Frumin, D., Krebbers, R., Birkedal, L.: Compositional non-interference for fine-grained concurrent programs. In: SP 2021, pp. 1416–1433. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00003 117. Fuchsbauer, G., Kiltz, E., Loss, J.: The algebraic group model and its applications. In: H. Shacham, A. Boldyreva (eds.) CRYPTO 2018, Part II, LNCS, vol. 10992, pp. 33–62. Springer (2018). URL https://doi.org/10.1007/978-3-319-96881-0_2

19 Formalization of Security

29

118. Gancher, J., Sojakova, K., Fan, X., Shi, E., Morrisett, G.: A core calculus for equational proofs of cryptographic protocols. Proc. ACM Program. Lang. 7(POPL), 866–892 (2023). URL https://doi.org/10.1145/3571223 119. Georges, A.L., Guéneau, A., Strydonck, T.V., Timany, A., Trieu, A., Huyghebaert, S., Devriese, D., Birkedal, L.: Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5(POPL), 1–30 (2021). URL https://doi.org/10.1145/3434287 120. Georges, A.L., Trieu, A., Birkedal, L.: Le temps des cerises: Efficient temporal stack safety on capability machines using directed capabilities. Proc. ACM Program. Lang. 6(OOPSLA), 1–30 (2022). URL https://doi.org/10.1145/3527318 121. Gladshtein, V., Zhao, Q., Ahrens, W., Amarasinghe, S., Sergey, I.: Mechanised hypersafety proofs about structured data. Proc. ACM Program. Lang. 8(PLDI) (2024). URL https://arxiv.org/abs/2404.06477 122. Goguen, J.A., Meseguer, J.: Security policies and security models. In: SP ’82, pp. 11–20. IEEE (1982). URL https://doi.org/10.1109/SP.1982.10014 123. Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: SP ’84, pp. 75–87. IEEE (1984). URL https://doi.org/10.1109/SP.1984.10019 124. Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984). URL https://doi.org/10.1016/0022-0000(84)90070-9 125. Gómez-Londoño, A., Pohjola, J.Å., Syeda, H.T., Myreen, M.O., Tan, Y.K.: Do you have space for dessert? A verified space cost semantics for CakeML programs. Proc. ACM Program. Lang. 4(OOPSLA), 204:1–204:29 (2020). URL https://doi.org/10.1145/3428272 126. Gorla, D., Nestmann, U.: Full abstraction for expressiveness: History, myths and facts. Math. Struct. Comput. Sci. 26(4), 639–654 (2016). URL https://doi.org/10.1017/S0960129514000279 127. Goubault-Larrecq, J.: Towards producing formally checkable security proofs, automatically. In: CSF 2008, pp. 224–238. IEEE (2008). URL https://doi.org/10.1109/CSF.2008.21 128. Gregersen, S.O., Bay, J., Timany, A., Birkedal, L.: Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang. 5(POPL), 1–29 (2021). URL https://doi.org/10.1145/3434291 129. Guéneau, A., Charguéraud, A., Pottier, F.: A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In: A. Ahmed (ed.) ESOP 2018, LNCS, vol. 10801, pp. 533–560. Springer (2018). URL https://doi.org/10.1007/978-3-319-89884-1_19 130. Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., Strub, P.Y.: Computer-aided proofs for multiparty computation with active security. In: CSF 2018, pp. 119–131. IEEE (2018). URL https://doi.org/10.1109/CSF.2018.00016 131. Haines, T., Goré, R., Sharma, B.: Did you mix me? Formally verifying verifiable mix nets in electronic voting. In: SP 2021, pp. 1748–1765. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00033 132. Haines, T., Goré, R., Tiwari, M.: Verified verifiers for verifying elections. In: L. Cavallaro, J. Kinder, X. Wang, J. Katz (eds.) CCS ’19, pp. 685–702. ACM (2019). URL https://doi.org/10.1145/3319535.3354247 133. Hales, T.C., Raya, R.: Formal proof of the group law for Edwards elliptic curves. In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part II, LNCS, vol. 12167, pp. 254–269. Springer (2020). URL https://doi.org/10.1007/978-3-030-51054-1_15 134. Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch. 2005(181) (2005). URL http://eprint.iacr.org/2005/181 135. Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: LICS 2002, pp. 89–100. IEEE (2002). URL https://doi.org/10.1109/LICS.2002.1029819 136. Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: P. Manolios, M. Wilding (eds.) ACL2 2006, pp. 11–20. ACM (2006). URL https://doi.org/10.1145/1217975.1217978

30

Gilles Barthe

137. Haselwarter, P.G., Hvass, B.S., Hansen, L.L., Winterhalter, T., Hrit, cu, C., Spitters, B.: The last yard: Foundational end-to-end verification of high-speed cryptography. In: A. Timany, D. Traytel, B. Pientka, S. Blazy (eds.) CPP 2024, pp. 30–44. ACM (2024). URL https://doi.org/10.1145/3636501.3636961 138. Haselwarter, P.G., Rivas, E., Muylder, A.V., Winterhalter, T., Abate, C., Sidorenco, N., Hrit, cu, C., Maillard, K., Spitters, B.: SSProve: A foundational framework for modular cryptographic proofs in Coq. ACM Trans. Program. Lang. Syst. 45(3), 15:1–15:61 (2023). URL https://doi.org/10.1145/3594735 139. Hess, A.V., Mödersheim, S., Brucker, A.D., Schlichtkrull, A.: Performing security proofs of stateful protocols. In: CSF 2021, pp. 1–16. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00006 140. Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: M. Brenner, K. Rohloff, J. Bonneau, A. Miller, P.Y.A. Ryan, V. Teague, A. Bracciali, M. Sala, F. Pintore, M. Jakobsson (eds.) FC 2017, LNCS, vol. 10323, pp. 520–535. Springer (2017). URL https://doi.org/10.1007/978-3-319-70278-0_33 141. Hölzl, J.: Formalising semantics for expected running time of probabilistic programs. In: J.C. Blanchette, S. Merz (eds.) ITP 2016, LNCS, vol. 9807, pp. 475–482. Springer (2016). URL https://doi.org/10.1007/978-3-319-43144-4_30 142. Hölzl, J., Nipkow, T.: Interactive verification of Markov chains: Two distributed protocol case studies. In: U. Fahrenberg, A. Legay, C.R. Thrane (eds.) QFM 2012, EPTCS, vol. 103, pp. 17–31 (2012). URL https://doi.org/10.4204/EPTCS.103.2 143. Hrit, cu, C., Greenberg, M., Karel, B., Pierce, B.C., Morrisett, G.: All your IFCException are belong to us. In: SP 2013, pp. 3–17. IEEE (2013). URL https://doi.org/10.1109/SP.2013.10 144. Hvass, B.S., Aranha, D.F., Spitters, B.: High-assurance field inversion for curve-based cryptography. In: CSF 2023, pp. 552–567. IEEE (2023). URL https://doi.org/10.1109/CSF57540.2023.00008 145. Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: T. Kohno (ed.) USENIX Security ’12, pp. 113–128. USENIX Association (2012). URL https://www.usenix.org/conference/usenixsecurity12/ technical-sessions/presentation/jang 146. Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1–30:68 (2018). URL https://doi.org/10.1145/3208102 147. Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: A. Biere, R. Bloem (eds.) CAV 2014, LNCS, vol. 8559, pp. 167–183. Springer (2014). URL https://doi.org/10.1007/978-3-319-08867-9_11 148. Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comput. Sci. 298(3), 583–626 (2003). URL https://doi.org/10.1016/S0304-3975(02)00869-1 149. Klenze, T., Sprenger, C., Basin, D.A.: Formal verification of secure forwarding protocols. In: CSF 2021, pp. 1–16. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00018 150. Kuepper, J., Erbsen, A., Gross, J., Conoly, O., Sun, C., Tian, S., Wu, D., Chlipala, A., Chuengsatiansup, C., Genkin, D., Wagner, M., Yarom, Y.: CryptOpt: Verified compilation with randomized program search for cryptographic primitives. Proc. ACM Program. Lang. 7(PLDI), 1268–1292 (2023). URL https://doi.org/10.1145/3591272 151. Lallemand, J., Basin, D.A., Sprenger, C.: Refining authenticated key agreement with strong adversaries. In: EuroS&P 2017, pp. 92–107. IEEE (2017). URL https://doi.org/10.1109/EuroSP.2017.22 152. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). URL https://doi.org/10.1145/1538788.1538814 153. Li, S.W., Li, X., Gu, R., Nieh, J., Hui, J.Z.: A secure and formally verified Linux KVM hypervisor. In: SP 2021, pp. 1782–1799. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00049

19 Formalization of Security

31

154. Li, Y., yao Xia, L., Weirich, S.: Reasoning about the garden of forking paths. Proc. ACM Program. Lang. 5(ICFP), 1–28 (2021). URL https://doi.org/10.1145/3473585 155. Lowe, G.: An attack on the Needham–Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995). URL https://doi.org/10.1016/0020-0190(95)00144-2 156. Maillard, K., Hrit, cu, C., Rivas, E., Muylder, A.V.: The next 700 relational program logics. Proc. ACM Program. Lang. 4(POPL), 4:1–4:33 (2020). URL https://doi.org/10.1145/3371072 157. Mantel, H.: A uniform framework for the formal specification and verification of information flow security. PhD thesis, Saarland University (2003). URL http://scidok.sulb.uni-saarland.de/volltexte/2004/202/index.html 158. Maurer, U.: Constructive cryptography—a new paradigm for security definitions and proofs. In: S. Mödersheim, C. Palamidessi (eds.) TOSCA 2011, LNCS, vol. 6993, pp. 33–56. Springer (2011). URL https://doi.org/10.1007/978-3-642-27375-9_3 159. Maurer, U.M.: Abstract models of computation in cryptography. In: N.P. Smart (ed.) Cryptography and Coding 2005, LNCS, vol. 3796, pp. 1–12. Springer (2005). URL https://doi.org/10.1007/11586821_1 160. Meadows, C.: The NRL Protocol Analyzer: An overview. J. Log. Program. 26(2), 113–131 (1996). URL https://doi.org/10.1016/0743-1066(95)00095-X 161. Meier, S., Cremers, C., Basin, D.A.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: CSF 2010, pp. 231–245. IEEE (2010). URL https://doi.org/10.1109/CSF.2010.23 162. Mitchell, J.C.: On abstraction and the expressive power of programming languages. Sci. Comput. Program. 21(2), 141–163 (1993). URL https://doi.org/10.1016/0167-6423(93)90004-9 163. Monniaux, D.: Memory simulations, security and optimization in a verified compiler. In: A. Timany, D. Traytel, B. Pientka, S. Blazy (eds.) CPP 2024, pp. 103–117. ACM (2024). URL https://doi.org/10.1145/3636501.3636952 164. Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: RockSalt: Better, faster, stronger SFI for the x86. In: J. Vitek, H. Lin, F. Tip (eds.) PLDI ’12, pp. 395–404. ACM (2012). URL https://doi.org/10.1145/2254064.2254111 165. Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: SP 2013, pp. 415–429. IEEE (2013). URL https://doi.org/10.1109/SP.2013.35 166. Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF 2016, pp. 417–431. IEEE (2016). URL https://doi.org/10.1109/CSF.2016.36 167. Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: SoftBound: Highly compatible and complete spatial memory safety for C. In: M. Hind, A. Diwan (eds.) PLDI ’09, pp. 245–258. ACM (2009). URL https://doi.org/10.1145/1542476.1542504 168. Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: SP 2011, pp. 165–179. IEEE (2011). URL https://doi.org/10.1109/SP.2011.12 169. Necula, G.C.: Proof-carrying code. In: P. Lee, F. Henglein, N.D. Jones (eds.) POPL ’97, pp. 106–119. ACM (1997). URL https://doi.org/10.1145/263699.263712 170. Nelson, L., Bornholt, J., Krishnamurthy, A., Torlak, E., Wang, X.: Noninterference specifications for secure systems. ACM SIGOPS Oper. Syst. Rev. 54(1), 31–39 (2020). URL https://doi.org/10.1145/3421473.3421478 171. Ngo, V.C., Dehesa-Azuara, M., Fredrikson, M., Hoffmann, J.: Verifying and synthesizing constant-resource implementations with types. In: SP 2017, pp. 710–728. IEEE (2017). URL https://doi.org/10.1109/SP.2017.53 172. Nielsen, E.H., Annenkov, D., Spitters, B.: Formalising decentralised exchanges in Coq. In: R. Krebbers, D. Traytel, B. Pientka, S. Zdancewic (eds.) CPP 2023, pp. 290–302. ACM (2023). URL https://doi.org/10.1145/3573105.3575685

32

Gilles Barthe

173. Nielsen, J.B., Spitters, B.: Smart contract interactions in Coq. In: E. Sekerinski, N. Moreira, J.N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J.C. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro, D. Delmas (eds.) FM 2019, Part I, LNCS, vol. 12232, pp. 380–391. Springer (2019). URL https://doi.org/10.1007/978-3-030-54994-7_29 174. Nienhuis, K., Joannou, A., Bauereiss, T., Fox, A.C.J., Roe, M., Campbell, B., Naylor, M., Norton, R.M., Moore, S.W., Neumann, P.G., Stark, I., Watson, R.N.M., Sewell, P.: Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In: SP 2020, pp. 1003–1020. IEEE (2020). URL https://doi.org/10.1109/SP40000.2020.00055 175. Nipkow, T.: Amortized complexity verified. In: C. Urban, X. Zhang (eds.) ITP 2015, LNCS, vol. 9236, pp. 310–324. Springer (2015). URL https://doi.org/10.1007/978-3-319-22102-1_21 176. Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms: A biased survey. In: D.V. Hung, O. Sokolsky (eds.) ATVA 2020, LNCS, vol. 12302, pp. 25–53. Springer (2020). URL https://doi.org/10.1007/978-3-030-59152-6_2 177. Nowak, D.: A framework for game-based security proofs. In: S. Qing, H. Imai, G. Wang (eds.) ICICS 2007, LNCS, vol. 4861, pp. 319–333. Springer (2007). URL https://doi.org/10.1007/978-3-540-77048-0_25 178. von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: P. Samarati, P.Y.A. Ryan, D. Gollmann, R. Molva (eds.) ESORICS 2004, LNCS, vol. 3193, pp. 225–243. Springer (2004). URL https://doi.org/10.1007/978-3-540-30108-0_14 179. Olmos, S.A., Barthe, G., Gonzalez, R., Grégoire, B., Laporte, V., Léchenet, J.C., Oliveira, T., Schwabe, P.: High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024(1), 375–397 (2024). URL https://doi.org/10.46586/tches.v2024.i1.375-397 180. Paraskevopoulou, Z., Appel, A.W.: Closure conversion is safe for space. Proc. ACM Program. Lang. 3(ICFP), 83:1–83:29 (2019). URL https://doi.org/10.1145/3341687 181. Park, S.H., Pai, R.R., Melham, T.: A formal CHERI-C semantics for verification. In: S. Sankaranarayanan, N. Sharygina (eds.) TACAS 2021, Part I, LNCS, vol. 13993, pp. 549–568. Springer (2023). URL https://doi.org/10.1007/978-3-031-30823-9_28 182. Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci. 26(4), 655–657 (2016). URL https://doi.org/10.1017/S0960129514000280 183. Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: CSF 2017, pp. 392–404. IEEE (2017). URL https://doi.org/10.1109/CSF.2017.13 184. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Sec. 6(1–2), 85–128 (1998). URL http://content.iospress.com/articles/journal-of-computer-security/jcs102 185. Petcher, A., Morrisett, G.: The foundational cryptography framework. In: R. Focardi, A.C. Myers (eds.) POST 2015, LNCS, vol. 9036, pp. 53–72. Springer (2015). URL https://doi.org/10.1007/978-3-662-46666-7_4 186. Petcher, A., Morrisett, G.: A mechanized proof of security for searchable symmetric encryption. In: C. Fournet, M.W. Hicks, L. Viganò (eds.) CSF 2015, pp. 481–494. IEEE (2015). URL https://doi.org/10.1109/CSF.2015.36 187. Pike, L., Shields, M., Matthews, J.: A verifying core for a cryptographic language compiler. In: P. Manolios, M. Wilding (eds.) ACL2 2006, pp. 1–10. ACM (2006). URL https://doi.org/10.1145/1217975.1217977 188. Pîrlea, G., Sergey, I.: Mechanising blockchain consensus. In: J. Andronick, A.P. Felty (eds.) CPP 2018, pp. 78–90. ACM (2018). URL https://doi.org/10.1145/3167086 189. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977). URL https://doi.org/10.1016/0304-3975(77)90044-5 190. Popescu, A., Hölzl, J., Nipkow, T.: Proving concurrent noninterference. In: C. Hawblitzel, D. Miller (eds.) CPP 2012, LNCS, vol. 7679, pp. 109–125. Springer (2012). URL https://doi.org/10.1007/978-3-642-35308-6_11

19 Formalization of Security

33

191. Popescu, A., Hölzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: G. Gonthier, M. Norrish (eds.) CPP 2013, LNCS, vol. 8307, pp. 259–275. Springer (2013). URL https://doi.org/10.1007/978-3-319-03545-1_17 192. Pottier, F., Guéneau, A., Jourdan, J.H., Mével, G.: Thunks and debits in separation logic with time credits. Proc. ACM Program. Lang. 8(POPL), 1482–1508 (2024). URL https://doi.org/10.1145/3632892 193. Protzenko, J., Parno, B., Fromherz, A., Hawblitzel, C., Polubelova, M., Bhargavan, K., Beurdouche, B., Choi, J., Delignat-Lavaud, A., Fournet, C., Kulatova, N., Ramananandro, T., Rastogi, A., Swamy, N., Wintersteiger, C.M., Béguelin, S.Z.: EverCrypt: A fast, verified, cross-platform cryptographic provider. In: SP 2020, pp. 983–1002. IEEE (2020). URL https://doi.org/10.1109/SP40000.2020.00114 194. Ricketts, D., Robert, V., Jang, D., Tatlock, Z., Lerner, S.: Automating formal proofs for reactive systems. In: M.F.P. O’Boyle, K. Pingali (eds.) PLDI ’14, pp. 452–462. ACM (2014). URL https://doi.org/10.1145/2594291.2594338 195. Rushby, J.: Noninterference, transitivity and channel-control security policies. Tech. rep., SRI International (1992) 196. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003). URL https://doi.org/10.1109/JSAC.2002.806121 197. Schwabe, P., Viguier, B., Weerwag, T., Wiedijk, F.: A Coq proof of the correctness of X25519 in TweetNaCl. In: CSF 2021, pp. 1–16. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00023 198. Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 28:1–28:30 (2018). URL https://doi.org/10.1145/3158116 199. Sewell, T., Winwood, S., Gammie, P., Murray, T.C., Andronick, J., Klein, G.: seL4 enforces integrity. In: M.C.J.D. van Eekelen, H. Geuvers, J. Schmaltz, F. Wiedijk (eds.) ITP 2011, LNCS, vol. 6898, pp. 325–340. Springer (2011). URL https://doi.org/10.1007/978-3-642-22863-6_24 200. Shoup, V.: Lower bounds for discrete logarithms and related problems. In: W. Fumy (ed.) EUROCRYPT ’97, LNCS, vol. 1233, pp. 256–266. Springer (1997). URL https://doi.org/10.1007/3-540-69053-0_18 201. Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch. 2004(332) (2004). URL http://eprint.iacr.org/2004/332 202. Sidorenco, N., Oechsner, S., Spitters, B.: Formal security analysis of MPC-in-the-head zero-knowledge protocols. In: CSF 2021, pp. 1–14. IEEE (2021). URL https://doi.org/10.1109/CSF51468.2021.00050 203. Silver, L., He, P., Cecchetti, E., Hirsch, A.K., Zdancewic, S.: Semantics for noninterference with interaction trees. In: K. Ali, G. Salvaneschi (eds.) ECOOP 2023, LIPIcs, vol. 263, pp. 29:1–29:29. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023). URL https://doi.org/10.4230/LIPIcs.ECOOP.2023.29 204. Simon, L., Chisnall, D., Anderson, R.J.: What you get is what you C: Controlling side effects in mainstream C compilers. In: EuroS&P 2018, pp. 1–15. IEEE (2018). URL https://doi.org/10.1109/EuroSP.2018.00009 205. Sohr, K., Drouineaud, M., Ahn, G.J., Gogolla, M.: Analyzing and managing role-based access control policies. IEEE Trans. Knowl. Data Eng. 20(7), 924–939 (2008). URL https://doi.org/10.1109/TKDE.2008.28 206. Song, D.X., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 9(1/2), 47–74 (2001). URL https://doi.org/10.3233/jcs-2001-91-203 207. Sprenger, C., Backes, M., Basin, D.A., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW ’06, pp. 153–166. IEEE (2006). URL https://doi.org/10.1109/CSFW.2006.10 208. Sprenger, C., Basin, D.A.: Cryptographically-sound protocol-model abstractions. In: CSF 2008, pp. 115–129. IEEE (2008). URL https://doi.org/10.1109/CSF.2008.19

34

Gilles Barthe

209. Sprenger, C., Basin, D.A.: Developing security protocols by refinement. In: E. Al-Shaer, A.D. Keromytis, V. Shmatikov (eds.) CCS ’10, pp. 361–374. ACM (2010). URL https://doi.org/10.1145/1866307.1866349 210. Sprenger, C., Basin, D.A.: Refining key establishment. In: S. Chong (ed.) CSF 2012, pp. 230–246. IEEE (2012). URL https://doi.org/10.1109/CSF.2012.21 211. St-Martin, M., Felty, A.P.: A verified algorithm for detecting conflicts in XACML access control rules. In: J. Avigad, A. Chlipala (eds.) CPP 2016, pp. 166–175. ACM (2016). URL https://doi.org/10.1145/2854065.2854079 212. Stoughton, A., Varia, M.: Mechanizing the proof of adaptive, information-theoretic security of cryptographic protocols in the random oracle model. In: CSF 2017, pp. 83–99. IEEE (2017). URL https://doi.org/10.1109/CSF.2017.36 213. Strydonck, T.V., Georges, A.L., Guéneau, A., Trieu, A., Timany, A., Piessens, F., Birkedal, L., Devriese, D.: Proving full-system security properties under multiple attacker models on capability machines. In: CSF 2022, pp. 80–95. IEEE (2022). URL https://doi.org/10.1109/CSF54842.2022.9919645 214. Swamy, N., Hrit, cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Béguelin, S.Z.: Dependent types and multi-monadic effects in F. In: R. Bodík, R. Majumdar (eds.) POPL 2016, pp. 256–270. ACM (2016). URL https://doi.org/10.1145/2837614.2837655 215. Tao, R., Yao, J., Li, X., Li, S.W., Nieh, J., Gu, R.: Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware. In: R. van Renesse, N. Zeldovich (eds.) SOSP ’21, pp. 866–881. ACM (2021). URL https://doi.org/10.1145/3477132.3483560 216. Tassarotti, J., Harper, R.: Verified tail bounds for randomized programs. In: J. Avigad, A. Mahboubi (eds.) ITP 2018, LNCS, vol. 10895, pp. 560–578. Springer (2018). URL https://doi.org/10.1007/978-3-319-94821-8_33 217. Tassarotti, J., Harper, R.: A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL), 64:1–64:30 (2019). URL https://doi.org/10.1145/3290377 218. Théry, L., Hanrot, G.: Primality proving with elliptic curves. In: K. Schneider, J. Brandt (eds.) TPHOLs 2007, LNCS, vol. 4732, pp. 319–333. Springer (2007). URL https://doi.org/10.1007/978-3-540-74591-4_24 219. Tsai, M.H., Fu, Y.F., Liu, J., Shi, X., Wang, B.Y., Yang, B.Y.: CoqCryptoLine: A verified model checker with certified results. In: C. Enea, A. Lal (eds.) CAV 2023, Part II, LNCS, vol. 13965, pp. 227–240. Springer (2023). URL https://doi.org/10.1007/978-3-031-37703-7_11 220. Tsai, M.H., Wang, B.Y., Yang, B.Y.: Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs. In: B.M. Thuraisingham, D. Evans, T. Malkin, D. Xu (eds.) CCS ’17, pp. 1973–1987. ACM (2017). URL https://doi.org/10.1145/3133956.3134076 221. Unruh, D.: Quantum relational Hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1–33:31 (2019). URL https://doi.org/10.1145/3290346 222. Unruh, D.: Post-quantum verification of Fujisaki-Okamoto. In: S. Moriai, H. Wang (eds.) ASIACRYPT 2020, Part I, LNCS, vol. 12491, pp. 321–352. Springer (2020). URL https://doi.org/10.1007/978-3-030-64837-4_11 223. Vassena, M., Russo, A., Garg, D., Rajani, V., Stefan, D.: From fine- to coarse-grained dynamic information flow control and back. Proc. ACM Program. Lang. 3(POPL), 76:1–76:31 (2019). URL https://doi.org/10.1145/3290389 224. Wang, Y., Wilke, P., Shao, Z.: An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang. 3(POPL), 62:1–62:30 (2019). URL https://doi.org/10.1145/3290375 225. Wasserrab, D., Lohner, D., Snelting, G.: On PDG-based noninterference and its modular proof. In: S. Chong, D.A. Naumann (eds.) PLAS 2009, pp. 31–44. ACM (2009). URL https://doi.org/10.1145/1554339.1554345

19 Formalization of Security

35

226. Xia, L., Zakowski, Y., He, P., Hur, C.K., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction trees: Representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL), 51:1–51:32 (2020). URL https://doi.org/10.1145/3371119 227. Xiang, J., Chong, S.: Co-inflow: Coarse-grained information flow control for Java-like languages. In: SP 2021, pp. 18–35. IEEE (2021). URL https://doi.org/10.1109/SP40001.2021.00002 228. Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: B.M. Thuraisingham, D. Evans, T. Malkin, D. Xu (eds.) CCS ’17, pp. 2007–2020. ACM (2017). URL https://doi.org/10.1145/3133956.3133974 229. Yuan, S., Besson, F., Talpin, J.P., Hym, S., Zandberg, K., Baccelli, E.: End-to-end mechanized proof of an eBPF virtual machine for micro-controllers. In: S. Shoham, Y. Vizel (eds.) CAV 2022, Part II, LNCS, vol. 13372, pp. 293–316. Springer (2022). URL https://doi.org/10.1007/978-3-031-13188-2_15 230. Zaliva, V., Memarian, K., Almeida, R., Clarke, J., Davis, B., Richardson, A., Chisnall, D., Campbell, B., Stark, I., Watson, R.N.M., Sewell, P.: Formal mechanised semantics of CHERI C: Capabilities, undefined behaviour, and provenance. In: R. Gupta, N.B. Abu-Ghazaleh, M. Musuvathi, D. Tsafrir (eds.) ASPLOS 2024, pp. 181–196. ACM (2024). URL https://doi.org/10.1145/3617232.3624859 231. Zhao, L., Li, G., Sutter, B.D., Regehr, J.: ARMor: Fully verified software fault isolation. In: S. Chakraborty, A. Jerraya, S.K. Baruah, S. Fischmeister (eds.) EMSOFT 2011, pp. 289–298. ACM (2011). URL https://doi.org/10.1145/2038642.2038687 232. Zinzindohoué, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: A verified modern cryptographic library. In: B.M. Thuraisingham, D. Evans, T. Malkin, D. Xu (eds.) CCS ’17, pp. 1789–1806. ACM (2017). URL https://doi.org/10.1145/3133956.3134043