Developing Systems with Secure Information Flow

越来越多的私人数据存储在移动设备上，保护这些信息免受未经授权的访问变得越来越重要。这不仅涉及防止外部攻击者，还涉及防止应用程序和设备之间以及互联网之间的意外信息流。在本项目中，我们将重点关注第二个方面，同时也考虑外部攻击者。我们开发了一种新的方法，将正式验证的信息流控制（IFC）属性和基于语言的IFC与基于模型驱动开发的软件工程方法集成在一起。该方法从一个UML模型开始，该模型增强了特定于应用程序的信息流属性规范（例如，信用卡信息仅在确认预订后发送），这些属性可能由用户配置。模型到模型的转换生成特定于平台的Java代码以及正式的规范。为了验证程序的信息流特性，我们使用了基于语言的IFC和抽象解释的自动化技术。此分析的结果可以用作建立特定于应用程序的安全属性的关键定理。重点是Android应用和Java网络服务。

More and more private data is stored on mobile devices, and protection of this information against unauthorized access becomes more and more important. This concerns protection against outside attackers, but also protection against unintended information flows between apps and devices, and to the Internet. In this project we focus on the second aspect while also considering an external attacker. We develop a new approach that integrates formally verified information flow control (IFC) properties and language based IFC with a software engineering approach based on model-driven development. The approach starts with a UML model enhanced with application-specific specifications of information flow properties (e.g. credit card information is sent only after confirming a booking) that may be configured by the user. Model-to-model transformations generate platform-specific Java code as well as a formal specification. To verify information flow properties of programs, we use automatic techniques based on language-based IFC and abstract interpretation. The results of this analysis can be used as key theorems to establish application-specific security properties. The focus is on Android apps and Java web services.