A discussion of next generation technologies, especially with regard to software and formal methods.
Canonical Locations for this repo are, in order:
Formal methods allow us to create High Assurance (essentially "bug-free") software assuming certain conditions are met. We'll save the list of conditions for a future update.
While these methods take more time and skill up front, they allow software to run for far longer periods between failures or security compromises. Potentially forever in a theoretical sense if the hardware could ever be reliable enough to allow that. This is a far cry from today's systems that must be rebooted frequently and patched daily in an effort to stave off attacks.
Some good intro materials for the general public and executives:
- Hacker-Proof Code Confirmed Quanta Magazine Reprint in Wired
- DARPA High Assurance Cyber Military Systems (HACMS) MH-6 Little Bird helicopter
- seL4: A high-assurance, high-performance operating system microkernel.
- CertiKOS: A novel and practical programming infrastructure for constructing large-scale certified system software.
- Ironsides: An authoritative/recursive DNS server pair that is provably invulnerable to many of the problems that plague other servers.
- Muen: An x86/64 Separation Kernel for High Assurance.
- SMACK Software Verifier and Verification Toolchain
- smackers · GitHub
- smack/projects.md at master · smackers/smack · GitHub
- GitHub - alastairreid/smack-play: Experiments in using Smack verification tool with C and Rust
- GitHub - smackers/democratizing-software-verification-workshop-2019
- LiquidHaskell (awesome repo)
- Idris (awesome repo)
- Dafny is a verification-aware programming language
- TLA+
- Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch - YouTube
- Introduction :: Learn TLA+
- TLA+ model checking made symbolic – the morning paper
- Using TLA+ to Model Cascading Failures - Marianne Bellotti - Medium
- Using TLA+ to understand Xen vchan - Thomas Leonard's blog
- Practical TLA+ Now Available • Hillel Wayne
- Isabelle
- Martin Kleppmann - Correctness proofs of distributed systems with Isabelle | Code Mesh LDN 19 - YouTube
- What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq? - Stack Overflow
- Solving a puzzle using the Isabelle proof assistant · GitHub
- "Type-Driven Program Synthesis" by Nadia Polikarpova
- Commandline Commander: Synquid (appears to have been taken offline)
- DARPA Seeks to Create Software Systems That Could Last 100 Years
- Automated Program Repair | December 2019 | Communications of the ACM
- The Origin of Quorum Systems
- Distributed Storage Systems: Data Replication using Quorums
- The load, capacity, and availability of quorum systems
- Enter the Hydra: Towards Principled Bug Bounties and Exploit-Resistant Smart Contracts - Blockchain Protocol Analysis and Security Engineering 2018 | Cyber Initiative - Good overview of N-Version computing starting at 7:24.
- Hillel Wayne - Lots of blog posts about TLA+ and Formal Methods
- awesome-provable: A curated set of links to formal methods involving provable code.
- awesome-static-analysis: Static analysis tools for all programming languages, build tools, config files and more.
- awesome-dynamic-analysis: Dynamic analysis tools for all programming languages, build tools, config files and more.
- Awesome-Fuzzing: A curated list of fuzzing resources ( Books, courses - free and paid, videos, tools, tutorials and vulnerable applications to practice on ) for learning Fuzzing and initial phases of Exploit Development like root cause analysis.
- awesome-program-synthesis: An curated list of papers on program synthesis.