Verification and Secure Systems

Bugs in security-critical system software already cost society billions of dollars, and the need for secure software is increasing as more devices are connected to the Internet. This session will outline the security needs of network-connected systems and explore how formal verification can help secure them.

We’ll present research on bringing high-value security to low-cost devices, particularly those powered by microcontrollers – a class of devices ill-prepared for the security challenges of Internet connectivity. We’ll also discuss advances in verification tools and techniques that lead to real, usable verified software, with an emphasis on critical systems such as distributed and operating systems, cloud infrastructure, networking protocols and cryptography. Finally, we’ll present an overview of the Azure Sphere product as part of Microsoft’s efforts to secure MCU-based devices.

Related Products: Azure Sphere

Speaker Details

SENIOR RESEARCHER Chris Hawblitzel Chris Hawblitzel is a Senior Researcher at Microsoft Research. His research focuses on using programming language techniques and formal verification to enforce the safety and security of systems software. He has worked on projects like the Singularity OS (Eurosys “Test of Time” award), the Verve verified OS (PLDI best paper award), and the Ironclad/IronFleet verified software stack. He received a Ph.D. in Computer Science from Cornell in 2000, and taught at Dartmouth College until 2004. Partner Product Architect Ed Nightingale Ed Nightingale is the Partner Product Architect for Azure Sphere where he pushes crazy ideas like designing custom silicon to secure the MCU space. Prior to Azure Sphere, Ed was a systems researcher and software engineer. Ed has authored papers in top systems conferences such as OSDI and SOSP. He has co-authored 20 conference and journal publications, has won 6 best paper awards, and even helped to set the world record in disk-to-disk sorting (http://sortbenchmark.org). He has also worked as an engineer and as an engineering manager running a large-scale distributed storage service. Ed really enjoys building operating systems and large-scale distributed systems. Adam Chlipala Researcher | MSR Nikhil Swamy Nikhil Swamy is a Researcher in the RiSE group at Microsoft Research, Redmond. Nik’s research covers various topics including type systems, program logics, functional programming, program verification, interactive theorem proving and the foundations of computer security. He works on the F* programming language and its various offshoots, and is the current chair of PL(X), the RiSE working group on programming languages.

Series: Microsoft Research Faculty Summit