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

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

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.