Cyber attacks abound today with weekly news of new exploits and attacks. Most attacks take advantage of badly configured, badly deployed, or upatched systems and they can be mitigated, if not solved, by the use of configration management, authentication, intrusion detection, and auditing services. The truly scary attacks are ones which completely get around security tools or protocols due to bugs in the protocol, encryption, or code itself (i.e. Heartbleed, POODLE). Such attacks may not even be detectable by the means we have available today and raise fundamental questions about whether the tools we use today work the way we think they do. One set of tools for investigating such questions are formal methods modeling tools.
Formal methods languages and tools for security verification have been around for well over 15 years and have been used to both verify protocols that we use everyday and discover bugs in implementations of well known cryptographic libraries. They have made the move from being only interesting from an academic perspective to being ready for industrial use, albeit after a steep learning curve. In this talk, I will discuss the fundamentals of how formal methods security verification languages and tools work, give some concrete examples of how they have been used in the past, and give pointers where you can learn more about them. As examples, I will discuss languages and tools such as ProVerif, Tulafale, Spin, JML, and F#.