Kathleen Fisher - KEYNOTE: From quadcopters to helicopters | Code Mesh LDN 18

This video was recorded at Code Mesh LDN 18 http://bit.ly/2P7SPII Get involved in Code Sync's next conference http://bit.ly/2Mcm4aS --- KEYNOTE FROM QUADCOPTERS TO HELICOPTERS: FORMAL VERIFICATION FOR SAFER VEHICLES by Kathleen Fisher THIS TALK IN THREE WORDS: IoT security vulnerabilities High-assurance software Cyber retrofit 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 Coq theorem 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 provably does not contain exploitable bugs. I will discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quad-copters, helicopters, and automobiles. Read the full abstract: http://codesync.global/speaker/kathle... --- THE KEYNOTER - KATHLEEN FISHER Founder of HACMS program, Professor and Chair of Computer Science Department Kathleen Fisher is a Professor in and the Chair of the Computer Science Department at Tufts. Previously, she was a program manager at DARPA where she started and managed the HACMS and PPAML programs, a Consulting Faculty Member in the Computer Science Department at Stanford University, and a Principal Member of the Technical Staff at AT&T Labs Research. Kathleen is an ACM Fellow. She has served as Program Chair for PLDI,OOPSLA, ICFP, CUFP, and FOOL, and as General Chair for ICFP 2015. She is a former Associate Editor for TOPLAS and a former editor of the Journal of Functional Programming. Kathleen is a past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN) and past Co-Chair of CRA's Committee on the Status of Women (CRA-W). Kathleen is a recipient of the SIGPLAN Distinguished Service Award. She is Vice Chair of DARPA's ISAT Study Group and a member of the Board of Trustees of Harvey Mudd College. More on Kathleen Fisher: http://codesync.global/speaker/kathle... --- CODE SYNC & CODE MESH LDN 18 Code Mesh LDN is powered by Code Sync. Code Mesh LDN 18 was sponsored by WhatsApp, Toyota Connected, Erlang Solutions, TEAMango, and aeternity. CODE SYNC Website: www.codesync.global Twitter: www.twitter.com/CodeMeshIO Facebook:   / codesyncglobal   LinkedIn:   / code-sync   Mail: info at codesync.global #CodeMesh #KathleenFisher #Keynote #FormalVerification #FormalMethods