TWC: Medium: Collaborative: Flexible and Practical Information Flow Assurance for Mobile Apps

该项目正在开发工具和技术，以经济有效地评估移动应用程序的可信度。这项工作的重点是企业场景，其中企业或政府机构的人员使用与任务相关的应用程序并访问企业网络。在这种情况下，与目前的商品应用市场相比，我们有更多的动机和资源来对信息流进行实质性的评估和控制。该项目旨在推进静态技术所需的科学，使其能够被专业开发和评估团队使用，并有助于实现显著改进的保证。该项目的目标是：(a)找到灵活而富有表现力的方法来指定应用程序的信息流需求，(b)找到有效的方法来指定对Android平台的假设，以及(c)找到实用的静态分析和验证技术来检查应用程序相对于给定策略和平台的安全性。结果包括规范技术和理论模型和算法。这些应用于项目开发的原型工具的案例研究中，以评估目标的实现程度。认证机构可以部署该项目的技术，为保证提供科学可靠的技术，从而在关键任务情况下实现高度集成的移动软件的全部好处。软件设计人员将受益于能够精确地指定端到端需求以及组件接口。软件开发人员将受益于检测设计缺陷和错误、第三方软件中的恶意软件以及暴露漏洞的意外功能的可靠方法。除了移动软件的特定目标之外，这些技术将用于其他设置，特别是web应用程序，在这些设置中，对相互不信任的各方之间大量使用回调的接口进行推理至关重要。该项目可以帮助改善政府机构和私营部门的安全，间接使国家安全和普通民众受益。

This project is developing tools and techniques for cost-effective evaluation of the trustworthiness of mobile applications (apps). The work focuses on enterprise scenarios, in which personnel at a business or government agency use mission-related apps and access enterprise networks.In such scenarios there are incentives and resources for much more substantive evaluations and controls on information flow than are currently found in commodity app marketplaces. The project aims to advance the science needed for static techniques to be usable by professional development and evaluation teams and useful for achieving dramatically improved assurance. The project's goals are to: (a) find flexible and expressive ways to specify information flow requirements for apps, (b) find effective ways to specify what is assumed about the Android platform, and (c) find practical static analysis and verification techniques to check security of apps with respect to given policies and the platform. Results include specification techniques and theory - models and algorithms. These are applied in case studies with prototype tools that the project develops, to evaluate how well the goals are achieved.The project's techniques can be deployed by certification organizations to provide scientifically sound techniques for assurance, thusenabling the full benefits of highly-integrated mobile software in mission-critical situations. Software designers will benefit from being able to precisely specify end-to-end requirements as well as component interfaces. Software developers will benefit from reliable means to detect design flaws and bugs, malware in third-party software, and unintended functionality that exposes vulnerabilities. Beyond the specific target of mobile software, the techniques will be of use in other settings, especially web applications, where it is crucial to reason about interfaces between mutually untrusting parties making heavy use of callbacks. The project could help improve security in government agencies and private sector, indirectly benefitting national security and the general population.