Last active
October 31, 2023 07:04
-
-
Save saifnoorprottoy/7fb0fa38671e53c71d6c3957ec49a08a to your computer and use it in GitHub Desktop.
Usage of Formal Verification in Industry/ Industrial Producs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is an list of advanced PL research / FV research or the use of FV research or implementation of FV in the industry. This will be upgrated timely. | |
----------------------------------------------------------------------------------------------------------------- | |
Starter: Who is verifying their cryptographic protocols? https://galois.com/blog/2021/05/who-is-verifying-their-cryptographic-protocols/ | |
1) Static Analysis at Scale: An Instagram Story -> https://instagram-engineering.com/static-analysis-at-scale-an-instagram-story-8f498ab71a0c | |
2) Zoncolan: How Facebook uses static analysis to detect and prevent security issues -> https://engineering.fb.com/security/zoncolan/ | |
3) Proving security with automated reasoning -> https://www.allthingsdistributed.com/2019/06/proving-security-at-scale-with-automated-reasoning.html | |
4) Using EasyCrypt and Jasmin for post-quantum verification -> https://blog.cloudflare.com/post-quantum-easycrypt-jasmin/ | |
5) Design and Verification of the Arm Confidential Compute Architecture https://www.usenix.org/conference/osdi22/presentation/li | |
6) Wireguard Formal Verification https://www.wireguard.com/formal-verification/ | |
7) Avoiding Vulnerabilities in Crypto Code with SPARK https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-code-with-spark | |
8) An Analysis of Signal's PQXDH https://cryspen.com/post/pqxdh/ | |
9) Formal Verification of Ethereum 2.0 Part 1: Fixing the Array-Out-of-Bound Runtime Error https://consensys.io/blog/formal-verification-of-ethereum-2-0-part-1-fixing-the-array-out-of-bound-runtime-error | |
10) |
added two links on ARM formal verification (ARM confidential Computing ) and usage of Tamarin Prover in Wireguard
added a link on Ada Spark usage
added some other links including the latest article I found from LinkedIn
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
added an amazing article from Cloudflare engineering blog