jm + formal-verification   2

Excellent Twitter thread from colmmacc on how s2n avoids protocol-state errors
using a linearized set of state transitions, and Cryptol and SAW to perform verification of the TLS state machine
cryptol  saw  formal-verification  twitter  threads  colmmacc  security  s2n 
29 days ago by jm
An empirical study on the correctness of formally verified distributed systems
We must recognise that even formal verification can leave gaps and hidden assumptions that need to be teased out and tested, using the full battery of testing techniques at our disposal. Building distributed systems is hard. But knowing that shouldn’t make us shy away from trying to do the right thing, instead it should make us redouble our efforts in our quest for correctness.
formal-verification  software  coding  testing  tla+  chapar  fuzzing  verdi  bugs  papers 
may 2017 by jm

Copy this bookmark:



description:


tags: