Using Formal Methods to Eliminate Exploitable Bugs • Kathleen Fisher • YOW! 2015

This presentation was recorded at YOW! 2015. #GOTOcon #YOW https://yowcon.com Kathleen Fisher - Professor at Tufts University RESOURCES https://www.linkedin.com/in/kathleen-fisher-4000964 https://github.com/athleens ABSTRACT For decades, formal methods have offered the promise of software that doesn’t have exploitable bugs. Until recently, however, it hasn’t been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. It has been proven to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and to enforce integrity and confidentiality properties. The #CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution in the formal methods community, including increased processor speed, better infrastructure like the Isabelle/HOL and #CoqTheorem provers, specialized logics for reasoning about low-level code, increasing levels of automation afforded by tactic languages and SAT/SMT solvers, and the decision to move away from trying to verify existing artifacts and instead focus on co-developing the code and the correctness proof. In this talk, I will explore the promise and limitations of current formal methods techniques for producing useful software that probably does not contain exploitable bugs. I will discuss these issues in the context of DARPA’s HACMS program, which has as its goal the creation of high-assurance software for vehicles, including quad-copters, helicopters, and automobiles. RECOMMENDED BOOKS Aaron Parecki • OAuth 2.0 Simplified • https://amzn.to/2A3IMOf Aaron Parecki • OAuth 2.0 Servers • https://amzn.to/3ecHEsz Aaron Parecki • The Little Book of OAuth 2.0 RFCs • https://amzn.to/3i7qnlC Erdal Ozkaya • Cybersecurity: The Beginner's Guide • https://amzn.to/2T6OIj3 Richer & Sanso • OAuth 2 in Action • https://amzn.to/3hXiAH6 Wilson & Hingnikar • Demystifying OAuth 2.0, OpenID Connect, and SAML 2.0 • https://amzn.to/2U8iLY2 https://twitter.com/GOTOcon https://www.linkedin.com/company/goto- https://www.instagram.com/goto_con https://www.facebook.com/GOTOConferences #Bugs #EliminateBugs #ExploitableBugs #SoftwareEngineering #Security #Programming #KathleenFisher #YOWcon Looking for a unique learning experience? Attend the next GOTO conference near you! Get your ticket at https://gotopia.tech Sign up for updates and specials at https://gotopia.tech/newsletter SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily. https://www.youtube.com/user/GotoConferences/?sub_confirmation=1