Sep 28, 2015
Werner Dietl: Collaborative Verification of the Information Flow for a High-Assurance App Store
Malware is a serious problem on mobile devices. The vision of this session’s speakers was a verified app store in which each application has been formally proven to be free of (certain) defects and exploits. They have built such a system and successfully applied it to dozens of challenge applications created by hostile red teams. The session describes their type system for information flow along with support for implicit invocation (intents and reflection), varieties of polymorphism, and other challenges that have arisen. Based on my CCS 2014 and ASE 2015 papers.