Formal verification redux: secure dev beyond randomized testing
What can a man do to write secure software beyond code review and rigorous testing? Write less code and more theorems! Let’s check out how HTTPS is secured at implementation level today.
It’s well known it’s hard to grok what code does if it spans more than a screenful. The solution? Restrict semantics for better composition; give a user cheap modeling huzzah; knock program analysis up to 11. This talk gives a hurricane ride of the state of the art in formal verification, including case studies of a verified OS (CertiKOS), HTTPS components powering most of the traffic on the web (Project Everest), and the Linux kernel (linux.git/*.tla; locking mechanisms models). Why? So you can write code better, of course. With the power of Computer Science