3 ms·
formal verification continues to come up, but it has the issue that you can only formally verify problem domains you already expect -- and the advanced threat a
by zemnmez 6y ago
formal verification continues to come up, but it has the issue that you can only formally verify problem domains you already expect -- and the advanced threat actors for which formal verification is necessary have the toolkit to go off-script to find vulnerabilities.
I think the hype around formal verification also tends to misdirect away from the verification that strong type systems already do if used correctly, though vitally not at the protocol level.
- Klasiaster 6y agoType systems can encode invariants even on the protocol level. For example you can hand-write or generate (multi party) session types to avoid deadlocks etc. For Rust there is https://crates.io/crates/session-types https://crates.io/crates/session-types from http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf
- zemnmez 6y agothis is an interesting approach that I hope we see more of! but i specifically meant to refer to security components of a protocol: e.g. that whether a party can impersonate another with access to some information that is public or can be disclosed via some attack.
- Jhsto 6y agoAre you aware of Pi-calculus and ProVerif? ProVerif sounds to address at least some of your requirements. Links: - https://en.wikipedia.org/wiki/%CE%A0-calculus https://en.wikipedia.org/wiki/%CE%A0-calculus - https://prosecco.gforge.inria.fr/personal/bblanche/proverif/ https://prosecco.gforge.inria.fr/personal/bblanche/proverif/