Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015

Explore the revolutionary advancements in formal methods for creating software without exploitable bugs in this 47-minute conference talk from YOW! 2015. Delve into the world of verified software as Professor Kathleen Fisher from Tufts University discusses groundbreaking projects like SeL4, an open-source operating system microkernel proven to be functionally correct, and CompCert, a verifying C compiler that ensures absence of compiler-introduced bugs. Learn about the factors enabling this formal methods revolution, including improved processor speeds, advanced theorem provers, and specialized logics for low-level code reasoning. Gain insights into the promise and limitations of current formal methods techniques, with a focus on their application in DARPA's HACMS program for creating high-assurance software for vehicles. Discover how co-developing code and correctness proofs is transforming the landscape of secure software development, potentially eliminating buffer overflows, null pointer exceptions, and use-after-free errors.