Developing Systems with Secure Information Flow

开发具有安全信息流的系统

• 批准号: 183481129
• 负责人: Professor Dr. Wolfgang Reif
• 金额: --
• 依托单位: Institute for Software und Systems Engineering
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2010
• 资助国家: 德国
• 起止时间: 2009-12-31 至 2017-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/183481129?language=en
• 关键词: Developing; Systems; Secure; Information; Flow

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.

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