Replies: 1 comment 4 replies
-
I'll absolutely look into this! I don't know almost anything about cryptography, and honestly I'm surprised that F* doesn't handle runtime dependence (I'm sure you've heard of vale? is handling side channels equivalent to ensuring input independent runtime?), but yes cryptography is absolutely intended to be a well-supported use case. If you have more resources about different ways to allow these use cases, please share them! Thank you for pointing this out! As the design and implementation progresses I'll keep this in mind :) |
Beta Was this translation helpful? Give feedback.
4 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Why cryptography is relevant for Magmide
State of formal verification in cryptography
Formal verification is mostly used in two ways, firstly it's used to show that an implementation of a cryptographic algorithm matches some specification. This is one of the main use-cases of F* in project Everest (check out Idris btw, it's very similar to F*).
Secondly it's used to prove that a cryptographic algorithm is "correct" (e.g. decrypting an encrypted message gives back the original) and that it is "secure" (for some slightly dishonest definition of secure). In order to prove "security" and often also "correctness" we have to be able to reason about probabilistic programs. This is out of scope for F* and Idris. Coq and Isabelle both have libraries for reasoning about probabilistic algorithms (FCF and CryptHOL), but these will likely never be used outside cryptography. There is also a standalone proof assistant for reasoning about cryptography, EasyCrypt, but this will also never be used outside cryptography. This is where Magmide can make a difference and provide something that is of interest to a broader community and thus has a larger ceiling on development time, library count and time spent "looking for bugs".
What Magmide can learn from cryptography
Jasmin is a c-like programming language being developed for doing cryptography. Its semantics are defined in Coq and it exports to EasyCrypt for formal verification. The compiler is verified in Coq. I think that it does a lot of the things you are interested in doing for Host Magmide, though it isn't built for uses outside cryptography.
What Magmide has to do to have first-class support for reasoning about cryptography
Most features, like asserting that a function has runtime independent of secret inputs can be added far into development, but I believe that support for reasoning about probabilistic programs has to be there from early on (before there would be resistance to changing how programs are modeled), otherwise there's the risk that the language is split into two parts, the probabilistic and the deterministic ones, with lacking compatibility.
The usual way to do this is to replace the option monad in Hoare logic with a distribution monad (this (currently incomplete) book shows some of the theory).
Beta Was this translation helpful? Give feedback.
All reactions