Proving mobile apps to be free of information flow exploits

Sunday, December 01, 2013
6:00 PM
ENS 637
Free and open to the public

Malware is a serious problem on mobile devices. Our vision is a verified app store in which each application has been formally proven to be free of (certain) defects and exploits. We have built such a system and successfully applied to dozens of challenge applications created by hostile Red Teams. This talk describes our type system for information flow, along with support for implicit invocation (intents and reflection), varieties of polymorphism, and other challenges that arose.

x x


Michael Ernst

Associate Professor
University of Washington
Michael D. Ernst is an Associate Professor in the Computer Science & Engineering department at the University of Washington. Ernst's research aims to make software more reliable, more secure, and easier (and more fun!) to produce. His primary technical interests are in software engineering, programming languages, type theory, security, program analysis, bug prediction, testing, and verification. Ernst's research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work. Dr. Ernst was previously a tenured professor at MIT, and before that a researcher at Microsoft Research.