Pith. sign in

REVIEW 2 major objections 6 minor 205 references

Formalization of security

T0 review · 2 major / 6 minor · reviewed 2026-07-31 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Proof assistants now routinely check that systems, languages, compilers, and crypto meet their security claims—and those proofs can support certification.

desk verdict Solid handbook survey that maps a mature field without claiming new theorems; useful reference, not a research advance. read the letter →

arxiv 2607.28551 v1 pith:GU63JK5C submitted 2026-07-30 cs.CR cs.LOcs.PL

Gilles Barthe This is my paper · ORCID
classification cs.CRcs.LOcs.PL
keywords proofassistantsinformationflownoninterferencesecurecompilationcryptographylanguage-basedsecurityhyperpropertiescertification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This chapter surveys how proof assistants are used to show that software and hardware designs actually enforce the security properties their designers claim. The motivation is twofold: security analyses are easy to get subtly wrong, and machine-checked proofs can feed formal certification regimes such as Common Criteria. The survey organizes a large body of work around information-flow noninterference (for systems and languages), resource bounds, access control and capabilities, hyperproperties, secure compilation, and both computational and symbolic cryptography. A sympathetic reader cares because the chapter argues that these applications have matured into a coherent, usable practice rather than isolated case studies: isolation kernels, constant-time compilers, and reductionist crypto proofs are already being machine-checked end to end.

What carries the argument

Unwinding lemmas for noninterference (step-consistency and step-preservation relative to an attacker equivalence on states), together with the parallel machinery of relational program logics (e.g., probabilistic relational Hoare logic) and secure-compilation criteria (full abstraction, hyperproperty preservation, compartmentalizing compilation). These are the devices that turn security goals into checkable proof obligations inside assistants.

What would settle it

An independent audit that finds a critical gap in a flagship cited development (for example, a broken isolation or constant-time preservation theorem in a major kernel or compiler formalization, or a flawed reduction in a widely cited crypto proof) would undercut the claim that the field is routinely reliable.

Watch

Extended reading notes

Core claim

The chapter’s central claim is that proof assistants are productively and routinely applied to validate security properties of systems, languages, compilers, and cryptographic constructions, and that the resulting mechanized proofs also support certification. It treats the surveyed formal developments—from unwinding-based noninterference through secure compilation criteria to game-based and constructive crypto proofs—as a mature, coherent field rather than scattered experiments.

Load-bearing premise

The chapter takes the theorems claimed in the cited machine-checked developments as established; if those primary proofs or their trusted bases fail, the survey’s picture of a mature field collapses.

Editorial extensions

If this is right

  • Security evaluations at high assurance levels can treat mechanized proofs of isolation, noninterference, and crypto reductions as primary evidence rather than informal arguments.
  • Compilers can be required to preserve side-channel and resource policies (constant-time, stack bounds) with machine-checked guarantees from source to assembly.
  • Cryptographic designs can be accompanied by checkable reductionist or constructive proofs before standardization or deployment.
  • Language-based enforcement (type systems, dynamic monitors, capability logics) can ship with machine-checked soundness relative to a formal semantics.
  • Hyperproperty and relational logics become standard tools for stating and verifying multi-trace security goals inside proof assistants.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The survey’s breadth implies that the bottleneck is shifting from ‘can we formalize this at all?’ to engineering reusable libraries, smaller trusted bases, and proof automation that non-experts can apply.
  • Cross-linking the crypto, compilation, and systems strands (already visible in constant-time-preserving compilers and assembly-level crypto) points toward end-to-end stacks where a single assistant carries security from high-level spec to machine code.
  • Certification regimes that still accept paper proofs may eventually require or strongly prefer the kinds of mechanized artifacts catalogued here, changing how vendors prepare evidence.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. This handbook chapter surveys the use of proof assistants to validate security properties of designs and implementations, and to support certification. It organizes a large literature under information-flow security (systems-level and language-based), resource usage, access control and capabilities, hyperproperties, secure compilation, and cryptography (computational game-based and constructive frameworks, post-quantum adversaries, symbolic/Dolev–Yao models, the generic group model, and implementation correctness), with shorter treatments of zero-knowledge/e-voting, smart contracts, and differential privacy. The load-bearing claim is descriptive and organizational: mechanized security proofs are mature and routinely applied across these areas (Abstract; §19.1), supported by an extensive citation map rather than new theorems.

Significance. As a handbook survey the contribution is organizational and bibliographic rather than theorematic, but that is appropriate and valuable. The chapter gives a coherent map of multi-community work (seL4 and related OS/hypervisor isolation, language-based IFC, CompCert/Jasmin-style secure compilation, CHERI/capabilities, and the main crypto provers CertiCrypt, EasyCrypt, FCF, CryptHOL, SSProve, Squirrel, plus implementation stacks such as Fiat-Crypto, VST, Jasmin, and HACL*). Machine-checked developments and certification-motivated formalizations are named explicitly. If accurate, the chapter is a useful reference entry point for readers who need orientation across systems, languages, compilers, and cryptography.

major comments (2)
  1. [§19.5] §19.5 (Hyperproperties) is markedly thinner than neighboring sections yet is elevated to a top-level topic. It cites only a handful of mechanizations (BiKAT, Hyper Hoare Logic, a separation hyperlogic) and does not connect them back to the noninterference, secure-compilation, and crypto material that dominate the chapter. Either expand with the main hyperproperty/hyperlogic formalization lines and their relation to §19.2 and §19.6, or fold the material into those sections so the TOC weight matches the substance.
  2. [§19.3] §19.3 (Resource usage) is only loosely tied to security for much of its length. Side-channel/constant-resource motivation appears in §19.2.2.6, but §19.3 largely surveys general complexity and cost formalizations (master theorems, time credits, expected runtime). For a chapter titled Formalization of Security, the security-relevant subset should be foregrounded and the purely algorithmic material shortened or explicitly justified as dual-use infrastructure for leakage and crypto reductions.
minor comments (6)
  1. [§19.7.4] §19.7.4 ends with a broken sentence: “...proofs of ElGamal encryption. model [117] have found many novel applications...”. Restore the intended reference to the algebraic group model (or similar) and fix grammar.
  2. [§19.2.1 and passim] Author-name and diacritic glitches appear in several places (e.g., “V on Oheimb” for von Oheimb; “Hrit,cu” / “Hrit ,cu” for Hriţcu; similar comma artifacts in other names). Sweep names and BibTeX for consistency.
  3. [§19.2.1] The text mixes “Rocq (formerly known as Coq)” with bare “Rocq” and occasional older “Coq” citations in the narrative. A one-time naming note early on, then consistent use, would help handbook readers.
  4. [§19.6.1] §19.6.1 discusses full abstraction shortcomings and trace-preserving / robust property preservation criteria; a short forward pointer from the information-flow sections to which hyperproperties are actually preserved by the cited compilers would tighten the arc between §19.2, §19.5, and §19.6.
  5. [§19.8.3] §19.8 is a catch-all; differential privacy (§19.8.3) is closer in technique to the relational crypto logics of §19.7.1 and could be cross-referenced there to avoid the appearance of an afterthought.
  6. [§19.2.1] A few citations are used for broad claims without a clause on what was machine-checked versus paper-only (e.g., overview citations in §19.2.1). Where the chapter’s theme is formalization, prefer one precise formal artifact per claim when space allows.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: handbook survey organizes external mechanized results; no derivation-from-inputs chain.

full rationale

This chapter is a literature survey (Abstract; §19.1) whose load-bearing claim is descriptive field maturity: proof assistants are routinely used to validate security properties across systems, languages, secure compilation, and cryptography, and to support certification. It does not present a first-principles derivation, fitted parameter, uniqueness theorem, or quantitative prediction that could reduce to its own inputs by construction. Cited formalizations (seL4, CompCert constant-time preservation, CertiCrypt/EasyCrypt, CryptHOL, FCF, Jasmin, etc.) are reported as established primary results, many machine-checked in independent provers; author self-citations are normal survey practice and do not force the organizing claim. There is no self-definitional loop, fitted-input-as-prediction, or ansatz smuggled via citation. Circularity score is floor.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

As a survey, the chapter inherits domain conventions of formal security rather than introducing fitted constants or new physical entities. Load-bearing background is standard: noninterference/unwinding as the information-flow yardstick, refinement/full-abstraction/hyperproperty criteria for compilers, and computational vs symbolic crypto models as used in the cited literature.

assumptions (4)
  • domain assumption Noninterference (and related hyperproperties) is an appropriate baseline policy for confidentiality and integrity in the surveyed systems and languages.
    Introduced via Goguen–Meseguer and unwinding in §19.2; underpins most systems- and language-level formalizations reported.
  • domain assumption Cited machine-checked developments correctly establish the security theorems they claim relative to their stated models and trusted bases.
    The chapter catalogs results from seL4, CompCert, EasyCrypt, CryptHOL, etc., without re-executing proofs; survey validity rests on those artifacts.
  • domain assumption Computational (game-based/reductionist), symbolic (Dolev–Yao), and related idealized models are meaningful security targets for cryptographic formalization.
    §19.7 structures crypto work around these standard models from Goldwasser–Micali, Dolev–Yao, and follow-ons.
  • standard math Standard mathematics and logic of the host proof assistants (HOL, CIC, etc.) are consistent for the purposes of the cited developments.
    Implicit background for all mechanizations surveyed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formalization of security." pith.science (2026). https://pith.science/paper/GU63JK5C

@misc{pith2026260728551,
  author       = {Pith},
  title        = {Pith review of: Formalization of security},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GU63JK5C}},
  note         = {Machine review of arXiv:2607.28551}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

205 extracted references · 103 canonical work pages

  1. [1]

    URLwww.cheri-cpu.org

    CHERI project. URLwww.cheri-cpu.org

  2. [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

    work page doi:10.1007/bfb0055109 1998

  3. [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

    arXiv 2018

  4. [4]

    ACM Trans

    Abate, C., Blanco, R., Ciobâc ˘a, ¸ S., 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

    work page doi:10.1145/3460860 2021

  5. [5]

    In: CSF 2019, pp

    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). URLhttps://doi.org/10.1109/CSF.2019.00025

    arXiv 2019

  6. [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). URLhttps://doi.org/10.1007/978-3-540-75670-5_10

    work page doi:10.1007/978-3-540-75670-5_10 2007

  7. [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). URLhttps://doi.org/10.1007/978-3-642-15497-3_10

    work page doi:10.1007/978-3-642-15497-3_10 2010

  8. [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

    arXiv 2012

Show all 205 references
  1. [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...

    2013

  2. [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...

    2013 doi

  3. [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). URLhttps://doi.org/10.1145/3167084

    2018 doi

  4. [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). ...

    2012 doi

  5. [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). URLhttps://doi.org/10.1007/10930755_22

    2003 doi

  6. [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

    2005 doi

  7. [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). URLhttps://doi.org/10.1145/3571213

    2023 doi

  8. [20]

    ACM Trans

    Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst.37(2), 7:1–7:31 (2015). URLhttps://doi.org/10.1145/2701415

    2015 doi

  9. [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). URLhttps://doi.org/10.1145/325694.325727

    2000

  10. [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

    2007 doi

  11. [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)

    2024

  12. [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). URLhttps://doi.org/10.3233/JCS-15784

    2016 doi

  13. [26]

    In: SP 2015, pp

    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

    2015 doi

  14. [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). URLhttps://doi.org/10.1007/978-3-319-89722-6_4

    2018 doi

  15. [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

    2021

  16. [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

    2011 doi

  17. [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). URLhttps://doi.org/10.1145/2660267.2660283

    2014

  18. [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). URLhttps://doi.org/10.1145/3371075

    2020 doi

  19. [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

    2004 doi

  20. [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). URLhttps://doi.org/10.1007/978-3-540-24721-0_7

    2004 doi

  21. [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

    2016

  22. [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

    2009

  23. [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). URLhttps://doi.org/10.1007/978-3-642-22792-9_5

    2011 doi

  24. [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

    2013 doi

  25. [43]

    constant-time

    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

    2018

  26. [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). URLhttps://doi.org/10.1145/3460120.3484761

    2021

  27. [45]

    In: CSF 2010, pp

    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

    2010 doi

  28. [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). URLhttps://doi.org/10.1145/2103656.2103670

    2012

  29. [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

    2007

  30. [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). URLhttps://doi.org/10.1007/978-3-540-71316-6_10 19 Formalization of Security 25

    2007 doi

  31. [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

    2014 doi

  32. [51]

    ACM Trans

    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). URLhttps://doi.org/10.1145/2019599.2019601

    2011

  33. [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

    2020 doi

  34. [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...

    2022 doi

  35. [54]

    In: SP 2017, pp

    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). URLhttps://doi.org/10.1109/SP.2017.24

    2017 doi

  36. [55]

    Springer (2007)

    Bella, G.: Formal Correctness of Security Protocols.Information Security and Cryptography. Springer (2007). URLhttps://doi.org/10.1007/978-3-540-68136-6

    2007 doi

  37. [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

    2002

  38. [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). URLhttps://doi.org/10.1007/11761679_25

    2006 doi

  39. [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

    2001 doi

  40. [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

    2012 doi

  41. [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). URLhttps://www.usenix.org/conference/usenixsecurity15/ technical-sessions/presentation/beringer

    2015

  42. [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

    2020 doi

  43. [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...

    2019 doi

  44. [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). URLhttps://doi.org/10.1007/978-3-030-17184-1_18

    2019 doi

  45. [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

    2017 doi

  46. [65]

    In: e-Smart 2002, pp

    Betarte, G., Giménez, E., Loiseaux, C., Chetali, B.: FORMA VIE: Formal modelling and verification of the JavaCard 2.1.1 security architecture. In: e-Smart 2002, pp. 213–231 (2002)

    2002

  47. [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). URLhttps://doi.org/10.1007/978-3-642-54108-7_15

    2013 doi

  48. [67]

    PhD thesis, University of Pennsylvania (2012)

    Bohannon, A.: Foundations of web script security. PhD thesis, University of Pennsylvania (2012)

    2012

  49. [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). URLhttps://doi.org/10.1145/1653662.1653673

    2009

  50. [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

    1996

  51. [70]

    In: CSFW ’97, pp

    Bolignano, D.: Towards the formal verification of electronic commerce protocols. In: CSFW ’97, pp. 133–147. IEEE (1997). URLhttps://doi.org/10.1109/CSFW.1997.596802

    1997

  52. [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

    2018

  53. [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

    2015 doi

  54. [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

    2018 doi

  55. [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

    2017 doi

  56. [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). URLhttps://doi.org/10.1145/3372885.3373815

    2020

  57. [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

    2021 doi

  58. [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). URLhttps://doi.org/10.1007/11526841_8

    2005 doi

  59. [80]

    In: CSF 2019, pp

    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

    2019

  60. [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). URLhttps://doi.org/10.1145/1314436.1314440 19 Formalization of Security 27

    2007

  61. [83]

    Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: R. Majumdar, V . Kuncak (eds.) CA V 2017, Part II,LNCS, vol. 10427, pp. 64–85. Springer (2017). URLhttps://doi.org/10.1007/978-3-319-63390-9_4

    2017 doi

  62. [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

    2015

  63. [85]

    Habilitation thesis (2023)

    Charguéraud, A.: A modern eye on separation logic for sequential programs. Habilitation thesis (2023). URLhttps://tel.archives-ouvertes.fr/tel-04076725

    2023

  64. [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

    2015 doi

  65. [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). URLhttps://doi.org/10.1007/s10817-017-9431-7

    2019 doi

  66. [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). URLhttps://doi.org/10.1145/2660267.2660370

    2014

  67. [89]

    Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur.18(6), 1157–1210 (2010). URLhttps://doi.org/10.3233/JCS-2009-0393

    2010 doi

  68. [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

    2012 doi

  69. [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....

    2011 doi

  70. [92]

    In: SP 2017, pp

    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). URLhttps://doi.org/10.1109/SP.2017.28

    2017 doi

  71. [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). URLhttps://doi.org/10.1145/2908080.2908100

    2016

  72. [94]

    In: SP 2022, pp

    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). URLhttps://doi.org/10.1109/SP46214.2022.9833800

    2022

  73. [95]

    In: SP 2012, pp

    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

    2012 doi

  74. [96]

    In: SP 2014, pp

    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

    2014 doi

  75. [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 ...

    2024 doi

  76. [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.251670...

    2013

  77. [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). URLhttps://doi.org/10.1145/1328438.1328457

    2008

  78. [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

    2024 doi arXiv

  79. [101]

    IEEE Trans

    Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983). URLhttps://doi.org/10.1109/TIT.1983.1056650

    1983

  80. [102]

    In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21-22, 2015, pp

    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

    2015 doi

  81. [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

    2014 doi

  82. [104]

    Eberl, M.: Proving divide and conquer complexities in Isabelle/HOL. J. Autom. Reason. 58(4), 483–508 (2017). URLhttps://doi.org/10.1007/s10817-016-9378-0

    2017 doi

  83. [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

    2020 doi

  84. [107]

    In: SP 2019, pp

    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). URLhttps://doi.org/10.1109/SP.2019.00005

    2019

  85. [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). URLhttps://doi.org/10.1145/3656446

    2024 doi

  86. [109]

    Ernst, G., Murray, T.: SecCSL: Security concurrent separation logic. In: I. Dillig, S. Tasiran (eds.) CA V 2019,LNCS, vol. 11562, pp. 208–230. Springer (2019). URL https://doi.org/10.1007/978-3-030-25543-5_13

    2019 doi

  87. [110]

    ACM SIGLOG News10(2), 4–23 (2023)

    Finkbeiner, B.: Logics and algorithms for hyperproperties. ACM SIGLOG News10(2), 4–23 (2023). URLhttps://doi.org/10.1145/3610392.3610394

    2023

  88. [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

    2022

  89. [114]

    In: CSF 2016, pp

    Fournet, C., Keller, C., Laporte, V .: A certified compiler for verifiable computing. In: CSF 2016, pp. 268–280. IEEE (2016). URLhttps://doi.org/10.1109/CSF.2016.26

    2016 doi

  90. [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). URLhttps://doi.org/10.1145/3290376

    2019 doi

  91. [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). URLhttps://doi.org/10.1007/978-3-319-96881-0_2 19 Formalization of Security 29

    2018 doi

  92. [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). URLhttps://doi.org/10.1145/3571223

    2023 doi

  93. [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

    2021 doi

  94. [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). URLhttps://doi.org/10.1145/3527318

    2022 doi

  95. [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

    2024 arXiv

  96. [122]

    In: SP ’82, pp

    Goguen, J.A., Meseguer, J.: Security policies and security models. In: SP ’82, pp. 11–20. IEEE (1982). URLhttps://doi.org/10.1109/SP.1982.10014

    1982

  97. [123]

    In: SP ’84, pp

    Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: SP ’84, pp. 75–87. IEEE (1984). URLhttps://doi.org/10.1109/SP.1984.10019

    1984

  98. [124]

    Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci.28(2), 270–299 (1984). URLhttps://doi.org/10.1016/0022-0000(84)90070-9

    1984 doi

  99. [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

    2020 doi

  100. [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

    2016 doi

  101. [127]

    In: CSF 2008, pp

    Goubault-Larrecq, J.: Towards producing formally checkable security proofs, automatically. In: CSF 2008, pp. 224–238. IEEE (2008). URLhttps://doi.org/10.1109/CSF.2008.21

    2008 doi

  102. [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). URLhttps://doi.org/10.1145/3434291

    2021 doi

  103. [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

    2018 doi

  104. [130]

    In: CSF 2018, pp

    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). URLhttps://doi.org/10.1109/CSF.2018.00016

    2018

  105. [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

    2019

  106. [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). URLhttps://doi.org/10.1007/978-3-030-51054-1_15

    2020 doi

  107. [134]

    IACR Cryptol

    Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch.2005(181) (2005). URLhttp://eprint.iacr.org/2005/181

    2005

  108. [135]

    In: LICS 2002, pp

    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

    2002 arXiv

  109. [138]

    ACM Trans

    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). URLhttps://doi...

    2023 doi

  110. [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). URLhtt...

    2017 doi

  111. [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). URLhttps://doi.org/10.1007/978-3-319-43144-4_30

    2016 doi

  112. [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). URLhttps://doi.org/10.4204/EPTCS.103.2

    2012 doi

  113. [143]

    In: SP 2013, pp

    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

    2013 doi

  114. [144]

    In: CSF 2023, pp

    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

    2023

  115. [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). URLhttps://www.usenix.org/conference/usenixsecurity12/ technical-sessions/presentation/jang

    2012

  116. [146]

    Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM65(5), 30:1–30:68 (2018). URL https://doi.org/10.1145/3208102

    2018 doi

  117. [147]

    Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: A. Biere, R. Bloem (eds.) CA V 2014,LNCS, vol. 8559, pp. 167–183. Springer (2014). URLhttps://doi.org/10.1007/978-3-319-08867-9_11

    2014 doi

  118. [148]

    Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comput. Sci.298(3), 583–626 (2003). URLhttps://doi.org/10.1016/S0304-3975(02)00869-1

    2003 doi

  119. [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–...

    2023 doi

  120. [151]

    In: EuroS&P 2017, pp

    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

    2017 doi

  121. [152]

    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM52(7), 107–115 (2009). URLhttps://doi.org/10.1145/1538788.1538814

    2009

  122. [154]

    Li, Y ., yao Xia, L., Weirich, S.: Reasoning about the garden of forking paths. Proc. ACM Program. Lang.5(ICFP), 1–28 (2021). URLhttps://doi.org/10.1145/3473585

    2021 doi

  123. [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

    1995 doi

  124. [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

    2020 doi

  125. [157]

    PhD thesis, Saarland University (2003)

    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

    2003

  126. [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). URLhttps://doi.org/10.1007/978-3-642-27375-9_3

    2011 doi

  127. [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

    2005 doi

  128. [160]

    Meadows, C.: The NRL Protocol Analyzer: An overview. J. Log. Program.26(2), 113–131 (1996). URLhttps://doi.org/10.1016/0743-1066(95)00095-X

    1996 doi

  129. [161]

    In: CSF 2010, pp

    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

    2010 doi

  130. [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

    1993 doi

  131. [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). URLhttps://doi.org/10.1145/3636501.3636952

    2024

  132. [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). URLhttps://doi.org/10.1145/2254064.2254111

    2012

  133. [165]

    In: SP 2013, pp

    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). URLhttps://doi.org/10.1109/SP.2013.35

    2013 doi

  134. [166]

    In: CSF 2016, pp

    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). URLhttps://doi.org/10.1109/CSF.2016.36

    2016 doi

  135. [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). URLhttps://doi.org/10.1145/1542476.1542504

    2009

  136. [168]

    In: SP 2011, pp

    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

    2011 doi

  137. [169]

    Necula, G.C.: Proof-carrying code. In: P. Lee, F. Henglein, N.D. Jones (eds.) POPL ’97, pp. 106–119. ACM (1997). URLhttps://doi.org/10.1145/263699.263712

    1997

  138. [170]

    ACM SIGOPS Oper

    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). URLhttps://doi.org/10.1145/3421473.3421478

    2020

  139. [171]

    In: SP 2017, pp

    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). URLhttps://doi.org/10.1109/SP.2017.53

    2017 doi

  140. [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). URLhttps://doi.org/10.1145/3573105.3575685 32 Gilles Barthe

    2023

  141. [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 (...

    2019 doi

  142. [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

    2015 doi

  143. [176]

    Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms: A biased survey. In: D.V . Hung, O. Sokolsky (eds.) ATV A 2020,LNCS, vol. 12302, pp. 25–53. Springer (2020). URLhttps://doi.org/10.1007/978-3-030-59152-6_2

    2020 doi

  144. [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

    2007 doi

  145. [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

    2004 doi

  146. [179]

    IACR Trans

    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). URLhttps://doi.org/10.46586/tches.v2024.i1.375-397

    2024 doi

  147. [180]

    Paraskevopoulou, Z., Appel, A.W.: Closure conversion is safe for space. Proc. ACM Program. Lang.3(ICFP), 83:1–83:29 (2019). URLhttps://doi.org/10.1145/3341687

    2019 doi

  148. [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). URLhttps://doi.org/10.1007/978-3-031-30823-9_28

    2021 doi

  149. [182]

    Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci.26(4), 655–657 (2016). URLhttps://doi.org/10.1017/S0960129514000280

    2016 doi

  150. [183]

    In: CSF 2017, pp

    Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: CSF 2017, pp. 392–404. IEEE (2017). URLhttps://doi.org/10.1109/CSF.2017.13

    2017 doi

  151. [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

    1998

  152. [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

    2015 doi

  153. [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). URLhttps://doi.org/10.1109/CSF.2015.36

    2015 doi

  154. [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

    2006

  155. [188]

    Pîrlea, G., Sergey, I.: Mechanising blockchain consensus. In: J. Andronick, A.P. Felty (eds.) CPP 2018, pp. 78–90. ACM (2018). URLhttps://doi.org/10.1145/3167086

    2018 doi

  156. [189]

    Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci.5(3), 223–255 (1977). URLhttps://doi.org/10.1016/0304-3975(77)90044-5

    1977 doi

  157. [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

    2012 doi

  158. [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). URLhttps://doi.org/10.1007/978-3-319-03545-1_17

    2013 doi

  159. [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

    2024 doi

  160. [193]

    In: SP 2020, pp

    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-pl...

    2020

  161. [194]

    In: M.F.P

    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). URLhttps://doi.org/10.1145/2594291.2594338

    2014

  162. [195]

    Rushby, J.: Noninterference, transitivity and channel-control security policies. Tech. rep., SRI International (1992)

    1992

  163. [196]

    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun.21(1), 5–19 (2003). URLhttps://doi.org/10.1109/JSAC.2002.806121

    2003

  164. [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

    2018 doi

  165. [199]

    In: M.C.J.D

    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

    2011 doi

  166. [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

    1997 doi

  167. [201]

    IACR Cryptol

    Shoup, V .: Sequences of games: A tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch.2004(332) (2004). URLhttp://eprint.iacr.org/2004/332

    2004

  168. [202]

    In: CSF 2021, pp

    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

    2021

  169. [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...

    2023 doi

  170. [204]

    In: EuroS&P 2018, pp

    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

    2018

  171. [205]

    IEEE Trans

    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

    2008 doi

  172. [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

    2001 doi

  173. [207]

    In: CSFW ’06, pp

    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

    2006 doi

  174. [208]

    In: CSF 2008, pp

    Sprenger, C., Basin, D.A.: Cryptographically-sound protocol-model abstractions. In: CSF 2008, pp. 115–129. IEEE (2008). URLhttps://doi.org/10.1109/CSF.2008.19 34 Gilles Barthe

    2008 doi

  175. [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

    2010

  176. [210]

    Sprenger, C., Basin, D.A.: Refining key establishment. In: S. Chong (ed.) CSF 2012, pp. 230–246. IEEE (2012). URLhttps://doi.org/10.1109/CSF.2012.21

    2012 doi

  177. [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

    2016

  178. [212]

    In: CSF 2017, pp

    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). URLhttps://doi.org/10.1109/CSF.2017.36

    2017 doi

  179. [213]

    In: CSF 2022, pp

    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/CSF54...

    2022

  180. [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–27...

    2016

  181. [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

    2021

  182. [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

    2018 doi

  183. [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

    2019 doi

  184. [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

    2007 doi

  185. [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.) CA V 2023, Part II,LNCS, vol. 13965, pp. 227–240. Springer (2023). URL https://doi.org/10.1007/978-3-031-37703-7_11

    2023 doi

  186. [221]

    Unruh, D.: Quantum relational Hoare logic. Proc. ACM Program. Lang.3(POPL), 33:1–33:31 (2019). URLhttps://doi.org/10.1145/3290346

    2019 doi

  187. [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

    2020 doi

  188. [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). URLhttps://doi.org/10.1145/3290389

    2019 doi

  189. [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). URLhttps://doi.org/10.1145/3290375

    2019 doi

  190. [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

    2009

  191. [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). URLhttps://doi.org/10.1145/3371119

    2020 doi

  192. [227]

    In: SP 2021, pp

    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

    2021

  193. [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

    2007

  194. [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.) CA V 2022, Part II,LNCS, vol. 13372, pp. 293–316. Springer (2022). URL https://doi.org/10.1007...

    2022 doi

  195. [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. Musu...

    2024

  196. [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). URLhttps://doi.org/10.1145/2038642.2038687

    2011

  197. [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

    2017

Pith tools

Reviewed July 31, 2026 · model on record in the stance chip above.