Information flow analysis

Abstract

Software systems are becoming increasingly trusted to handle sensitive information, though they have the potential to abuse this trust with serious consequences. in particular if they are connected to the internet. We allow web browsers to access our bank accounts, but also allow them to send usage reports to the browser’s developers. A mainstream smartphone application has permissions to read our digital photo albums, contact lists and calendar, while at the same time it is free to use the phone’s internet connection in every way possible. This chapter discusses how the KeY System can be used to address the increasingly important question of information flow control: does a program introduce information flows between resources in a way which is in violation of our security policy?