* 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* * [ ] 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) * [ ] Chulipala (2022), *Certified Programming with Dependent Types* * [ ] 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) * [x] Floyd (1967), "Assigning Meanings to Programs" * [x] Hoare (1969), "An Axiomatic Basis for Computer Programming" * [ ] 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* * [ ] Scott and Strachey (1971), ["Towards a Mathematical Semantics for Computer Languages"](https://www.cs.cmu.edu/~crary/819-f09/Scott71.pdf) * [ ] Stonebreaker and Hellerstein (2005), ["What Goes Around Comes Around"](https://people.cs.umass.edu/~yanlei/courses/CS691LL-f06/papers/SH05.pdf) * [ ] 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) * [ ] Van Horn and Might (2010), ["Abstracting Abstract Machines"](https://dl.acm.org/doi/10.1145/1863543.1863553) * [ ] 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) ## Data - [ ] Shneiderman (1996), ["The Eyes Have It: A Task by Data Type Taxonomy for Information Visualizations"](https://www.cs.umd.edu/~ben/papers/Shneiderman1996eyes.pdf) - [ ] Wickham (2014), ["Tidy Data"](https://www.jstatsoft.org/article/view/v059i10/) ## Formal modeling, verification, and analysis With blurry overlap with [[cryptography, especially end-to-end encryption]]. - Spin, Simple Protocol Interpreter, Protocol Meta Language * ["The Science of Deep Specification: Research Overview"](https://deepspec.org/page/Research/_) * [ ] Appel (2015), ["Verification of a Cryptographic Primitive: SHA-256"](https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf) * [x] Arquint et al. (2022), ["Sound Verification of Security Protocols: From Design to Interoperable Implementations"](https://arxiv.org/pdf/2212.04171) * [ ] 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)** * [ ] Basin and Cremers (2014), ["Know Your Enemy: Compromising Adversaries in Protocol Analysis"](https://dl.acm.org/doi/abs/10.1145/2658996) * [ ] Basin et al. (2016), ["Modeling Human Errors in Security Protocols"](https://ieeexplore.ieee.org/document/7536385) - [ ] 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 et al. (2015), ["Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant"](https://dl.acm.org/doi/10.1145/2775051.2677006) * [ ] 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/) * [ ] 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) * [ ] Cremers et al. (2025), ["A Ladder of Cryptographic Problems to Illustrate Formal Verification"](https://github.com/charlie-j/fm-crypto-lib/blob/9c6c23045f1f16f2f0253c9a16aac83d9f427865/Notes/main.pdf) * [ ] Davis et al. (2020), ["eXtreme Modelling in Practice"](https://arxiv.org/abs/2006.00915) * [ ] Denning (1976), ["A Lattice Model of Secure Information Flow"](https://dl.acm.org/doi/10.1145/360051.360056) * [ ] Durgin et al. (2004), ["Multiset Rewriting and the Complexity of Bounded Security Protocols"](https://dl.acm.org/doi/10.5555/1017273.1017276) * [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) * [x] Jenny (2023), ["Verifying Go's Standard Library"](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Adrian_Jenny_PW_Report.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) * [ ] Le Blanc and Lam (2024), ["Surveying the Rust Verification Landscape"](https://arxiv.org/abs/2410.01981) * [ ] Larisch et al. (2024), ["Topaz: Declarative and Verifiable Authoritative DNS at CDN-Scale"](https://research.cloudflare.com/publications/Larisch2024/) * [ ] Lattuada et al. (2024), ["Verus: A Practical Foundation for Systems Verification"](https://dl.acm.org/doi/10.1145/3694715.3695952) * [ ] Lindell (2021), ["How To Simulate It: A Tutorial on the Simulation Proof Technique"](https://eprint.iacr.org/2016/046.pdf) * [x] Ma et al. (2025), ["SpecGen: Automated Generation of Formal Program Specifications via Large Language Models"](https://arxiv.org/abs/2401.08807) - [ ] 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) * [ ] Sergey et al. (2017), ["Programming and Proving with Distributed Protocols"](https://dl.acm.org/doi/abs/10.1145/3158116) * [ ] Singh et al. (2025), ["OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries"](https://eprint.iacr.org/2025/1092.pdf) * [ ] Sprenger et al. (2020), ["Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifcation"](https://dl.acm.org/doi/pdf/10.1145/3428220) * [ ] Weisner (2022), ["Automated Translation of Tamarin Theories into I/O Specifications for Igloo"](https://www.research-collection.ethz.ch/entities/publication/70b92112-ca4a-4fba-9984-b6da72075e9d) * [ ] Wilcox et al. (2015), ["Verdi: A Framework for Implementing and Formally Verifying Distributed Systems"](https://dl.acm.org/doi/10.1145/2737924.2737958) * [ ] Wilcox et al. (2017), ["Programming Language Abstractions for Modularly Verified Distributed Systems"](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.19) ### Hyperproperties and observational determinism For some reason, sorted by publication date rather than by author: - [ ] 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) - [ ] Barthe et al. (2004), ["Secure Information Flow by Self-Composition"](https://www.computer.org/csdl/proceedings-article/csfw/2004/21690100/12OmNxdm4uz) - [ ] Terauchi and Aiken (2005), ["Secure Information Flow as a Safety Problem"](https://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf) - [ ] Huisman et al. (2006), ["A Temporal Logic Characterisation of Observational Determinism"](https://ieeexplore.ieee.org/document/1648704) - [ ] Smith (2007), ["Principles of Secure Information Flow Analysis"](https://www.cs.cornell.edu/courses/cs5430/2013sp/paper.smithInfoFlow.pdf) - [ ] 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) - [ ] Sheff (2013), ["Secure Information Flow by Self-Composition"](https://www.cs.cornell.edu/courses/cs6113/2013fa/notes/Self_Composition.pdf) - [ ] Clarkson et al. (2014), ["Temporal Logics for Hyperproperties"](https://arxiv.org/abs/1401.4492) - [ ] Basin et al. (2015), ["Automated Symbolic Proofs of Observational Equivalence"](https://infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2015/ASPObsEq.pdf) - [ ] Karimpour et al. (2016), ["Verifying Observational Determinism"](https://inria.hal.science/hal-01345097v1/document) - [ ] Cheval et al. (2018), “DEEPSEC: Deciding Equivalence Properties in Security Protocols—Theory and Practice" - [ ] Cheval et al. (2018), ["The DEEPSEC Prover"](https://link.springer.com/chapter/10.1007/978-3-319-96142-2_4) - [ ] Cheval et al. (2019), [“Exploiting Symmetries When Proving Equivalence Properties for Security Protocols"](https://chevalvi.gitlabpages.inria.fr/chevalvi/files/CKR-ccs19.pdf) - [ ] 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) - [ ] Babel et al. (2020), “On the Semantics of Communications When Verifying Equivalence Properties" - [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) ## Logic(s) - ["Linear Logic"](https://plato.stanford.edu/entries/logic-linear/), *Stanford Encyclopedia of Philosophy* - [ ] Basin and Constable (1991), ["Metalogical Frameworks"](https://ecommons.cornell.edu/server/api/core/bitstreams/a27793f9-009b-4251-bd1f-674d7d4de215/content) - [ ] Basin et al. (1996), "A Topography of Labelled Modal Logics", in *Frontiers of Combining Systems: First International Workshop, Munich, March 1996* - [ ] Basin et al. (1997), ["Labelled Propositional Modal Logics: Theory and Practice"](https://ieeexplore.ieee.org/abstract/document/8344126) - [ ] Basin et al. (1998), ["Natural Deduction for Non-Classical Logics"](https://link.springer.com/article/10.1023/A:1005003904639) - [ ] Basin et al. (2000), ["Rewriting Logic as as Metalogical Framework"](https://link.springer.com/chapter/10.1007/3-540-44450-5_4) - [ ] Basin and Matthews (2002), ["Logical Frameworks"](https://link.springer.com/chapter/10.1007/978-94-017-0464-9_2), in Gabbay and Guenthner (eds.), *Handbook of Philosophical Logic* ## 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"