[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[dan at geer.org]

 | Formal verification is not a panacea, will never be something we can
 | use for every program, and has serious limitations, but it is already
 | a really serious tool in the security world. A number of recent TLS
 | vulns were found via formal methods.


Two related items, possibly old news here:

1. Kathleen Fisher, Tufts, holds what I understand to be the
world heavyweight champion belt in having put together a
formally verified control system for a quad copter.

wp.doc.ic.ac.uk/riapav/wp-content/uploads/sites/28/2014/05/HACMS-Fisher.pdf

2. I see great promise in the Language Theoretic Security effort,
spearheaded by Sergey Bratus (Dartmouth) and Meredith Patterson
(Nuance Communications / Upstanding Hackers, Inc.)

langsec.org
spw16.langsec.org/workshop-program.html


--dan