* Black (ed.), [Dictionary of Algorithms and Data Structures](https://xlinux.nist.gov/dads/) * [Open Logic Project](https://builds.openlogicproject.org) * [ ] Abelson and Sussman (1996), *Structure and Interpretation of Computer Programs* * [ ] Bradley and Manna (2007), *The Calculus of Computation* * [ ] Delaët et al. (2022), ["Turning Catala into a Proof Platform for the Law"](https://inria.hal.science/hal-03447072/) * [ ] Fichte et al. (2023), ["The Silent (R)evolution of SAT"](https://dl.acm.org/doi/pdf/10.1145/3560469) * [ ] Lawsky (2017), ["A Logic for Statutes"](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3088206) * [ ] Kun (2021), *A Programmer's Introduction to Mathematics* * [ ] Merigoux et al. (2021), ["Catala: A Programming Language for the Law"](https://inria.hal.science/hal-03159939) * [ ] Peirce (2002), *Types and Programming Languages* * [ ] Peirce et al., [*Software Foundations*](https://softwarefoundations.cis.upenn.edu): * [ ] *Logical Foundations* * [ ] *Programming Language Foundations* * [ ] *Verified Functional Algorithms* * [ ] Ulam (1990), [*Analogies between Analogies: The Mathematical Reports of S. M. Ulam and His Los Alamos Collaborators*](https://publishing.cdlib.org/ucpressebooks/view?docId=ft9g50091s&brand=ucpress) * [ ] Wayne (2024), [*Logic for Programmers*](https://leanpub.com/logic/) ### Code correctness/compliance - [ ] Kakarla et al. (2022), ["SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers"](https://www.usenix.org/system/files/nsdi22-paper-kakarla.pdf) ## Formal modeling, verification, and analysis With blurry overlap with [[cryptography, especially end-to-end encryption]]. * ["The Science of Deep Specification: Research Overview"](https://deepspec.org/page/Research/_) * Baanen et al. (2024), [*The Hitchhiker's Guide to Logical Verification*](https://lean-forward.github.io/hitchhikers-guide/2024/) * [ ] **Barbosa et al. (2019), ["SoK: Computer-Aided Cryptography"](https://eprint.iacr.org/2019/1393.pdf)** - [ ] Bornholt et al. (2021), ["Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3"](https://dl.acm.org/doi/10.1145/3477132.3483540) - [x] Cassez (2001), ["Verification of the Incremental Merkle Tree Algorithm with Dafny"](https://franck44.github.io/publications/papers/merkle-fm-21.pdf) * [ ] Celi et al. (2022), ["A Tale of Two Models: Formal Verification of KEMTLS via Tamarin"](https://eprint.iacr.org/2023/1933.pdf) * [ ] Chlipala (2018), ["The Surprising Security Benefits of End-to-End Formal Proofs"](https://cccblog.org/2018/06/13/the-surprising-security-benefits-of-end-to-end-formal-proofs/) * [ ] Chlipala, [*Formal Reasoning about Programs*](http://adam.chlipala.net/frap/) * [ ] ["Formal Reasoning about Programs"](https://frap.csail.mit.edu/main) (MIT, spring 2023) * [ ] ["Principles of Programming Languages"](https://sites.google.com/cs.washington.edu/cse-505-18au) (University of Washington, fall 2018) * [ ] Cousot and Cousot, ["A Gentle Introduction to Formal Verification of Computer Systems by Abstract Interpretation"](https://www.di.ens.fr/~cousot/publications.www/CousotCousot-Marktoberdorf-2009.pdf) * [x] Gancher et al. (2023), ["OWL: Compositional Verification of Security Protocols via an Information-Flow Type System"](https://eprint.iacr.org/2023/473.pdf) * [x] Halevi (2005), ["A Plausible Approach to Computer-Aided Cryptographic Proofs"](https://eprint.iacr.org/2005/181.pdf) * [ ] Kobeissi et al. (2021), ["Verifpal: Cryptographic Protocol Analysis for the Real World"](https://iacr.org/submit/files/slides/2021/rwc/rwc2021/3/slides.pdf) * [ ] Larisch et al. (2024), ["Topaz: Declarative and Verifiable Authoritative DNS at CDN-Scale"](https://research.cloudflare.com/publications/Larisch2024/) * [ ] Lindell (2021), ["How To Simulate It: A Tutorial on the Simulation Proof Technique"](https://eprint.iacr.org/2016/046.pdf) - [ ] Mora et al. (2023), ["Message Chains for Distributed System Verification"](https://dl.acm.org/doi/10.1145/3622876) * [ ] Murray and van Oorschot (2018), [“BP: Formal Proofs, the Fine Print and Side Effects”](https://people.scs.carleton.ca/~paulv/papers/secdev2018.pdf”) * [ ] Nipkow and Klein (2014), *Concrete Semantics* * [ ] Newcombe et al. (2015), ["How Amazon Uses Formal Methods"](https://dl.acm.org/doi/10.1145/2699417) * [ ] Protzenko et al. (2019), ["Formally Verified Cryptographic Web Applications in WebAssembly"](https://www.computer.org/csdl/proceedings-article/sp/2019/666000b256/1dlwheTvbEI) ### Hyperproperties and observational determinism - [ ] Lamport (1980), ["'Sometimes' Is Sometimes 'Not Never'"](https://hillelwayne.com/post/hyperproperties/) - [ ] Zdancewic and Myers (2003), ["Observational Determinism for Concurrent Program Security"](https://www.cs.cornell.edu/andru/papers/csfw03.pdf) - [ ] Huisman et al. (2006), ["A Temporal Logic Characterisation of Observational Determinism"](https://ieeexplore.ieee.org/document/1648704) - [ ] Terauchi (2008), ["A Type System for Observational Determinism"](https://conferences.computer.org/sp/pdfs/csf/2008/2008-terauchi-type.pdf) - [ ] Clarkson and Schneider (2010), ["Hyperproperties"](https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf) - [ ] Clarkson (2016), ["Hyperproperties"](https://www.cs.cornell.edu/courses/cs5430/2016sp/l/27-hyperproperties/lec.pdf) - [ ] Clarkson et al. (2014), ["Temporal Logics for Hyperproperties"](https://arxiv.org/abs/1401.4492) - [ ] Karimpour et al. (2016), ["Verifying Observational Determinism"](https://inria.hal.science/hal-01345097v1/document) - [ ] Knabenhans (2018), ["Automatic Inference of Hyperproperties"](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Christian_Knabenhans_BA_report.pdf) - [ ] Patrignani (2018), ["(Hyper)Properties, Robustness, and Property-Preserving Compilers"](https://theory.stanford.edu/~mp/mp/CS350-2018_files/cs350-l3-rc.pdf) - [ ] Coenen (2019), ["Verifying Hyperliveness"](https://link.springer.com/chapter/10.1007/978-3-030-25540-4_7) - [ ] Eilers et al. (2019), ["Modular Product Programs"](https://dl.acm.org/doi/10.1145/3324783) - [x] Wayne (2020), ["Hypermodeling Hyperproperties"](https://hillelwayne.com/post/hyperproperties/) - [ ] Eilers et al. (2021), ["Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security"](https://pmpub.inf.ethz.ch/publications/EilersMeierMueller21.pdf) - [ ] Beutner and Finkbeiner (2022), ["Software Verification of Hyperproperties Beyond *k*-Safety"](https://vetss.org.uk/wp-content/uploads/sites/165/2024/05/2022_2-M-Casadio.pdf) - [ ] Pick (2022), ["Scaling Automatic Modular Verification"](https://lmpick.github.io/thesis.pdf), especially chapter 5, "Verification of Information Flow Security" - [ ] Gutsfeld et al. (2023), ["Deciding Asynchronous Hyperproperties for Recursive Programs"](https://arxiv.org/abs/2201.12859) - [x] Wayne (2024), ["Hyperproperties"](https://buttondown.com/hillelwayne/archive/hyperproperties/) - [x] Finkbeiner (2025), ["Logics and Algorithms for Hyperproperties"](https://arxiv.org/abs/2501.08063v1) ## Vulnerabilities and exploits - [ ] Bratus and Shubina (2015), "Exploitation as Code Reuse: On the Need of Formalization" - [ ] Bratus et al. (2011), "Exploit Programming: From Buffer Overflows to 'Weird Machines' and Theory of Computation" - [ ] Dullien (2017), "Weird Machines, Exploitability, and Proven Unexploitability" - [ ] Evtyushkin et al. (2021), "Computing with Time: Microarchitectural Weird Machines" - [ ] Mertens et al. (2019),"Weird Machines as Insecure Compilation" - [ ] Shacham (2007), ["The Geometry of Innocent Flesh on the Bone: Return-into-libc without Function Calls (on the x86)"](https://dl.acm.org/doi/pdf/10.1145/1315245.1315313) - [ ] Vanegue, "Adversarial Logic"