::: left till the conference

Formal verification redux: secure dev beyond randomized testing

19:35 - 20:15
30 min
Defensive Track

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

Speakers
Dmitriy “wldhx” Volkov
Share
Other Reports
Defensive Track
Company wide SAST
Web Village
JVMyachni Otake
Main Stage
LPE in Ring -3 / Intel ME
Up