Mobile Trust Through Joint Scalable Verification of High- and Low-Level Code

通过高级和低级代码的联合可扩展验证实现移动信任

• 批准号: 543583-2019
• 负责人: Gurfinkel, Arie
• 金额: $ 8.08万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Collaborative Research and Development Grants
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=699618
• 关键词: Mobile; Trust; Through; Joint; Scalable

Mobile device security is of critical importance. Architectural security guarantees from a Trusted Execution Environment (TEE), an operating system, and a framework like Android rely on the correctness of their code. We propose to address both low-level security concerns of TEE programs and high-level information-flow concerns of Android applications using a joint verification approach that scales to real-world applications. For the low-level, we propose to research layered abstractions for precision and scalability and executable counterexamples as a useful feedback to developers. For the high-level, we propose to develop an information flow type system and a matching inference approach to ensure desired information flow. Case studies and benchmarks will be developed together with our industrial partner Huawei Technologies Canada Ltd. and will be used to show the effectiveness of the developed approaches.

移动设备安全至关重要。可信执行环境 (TEE)、操作系统和 Android 等框架的架构安全保证依赖于其代码的正确性。我们建议使用可扩展到实际应用程序的联合验证方法来解决 TEE 程序的低级安全问题和 Android 应用程序的高级信息流问题。对于低级别，我们建议研究分层抽象以提高精度和可扩展性以及可执行的反例，作为对开发人员的有用反馈。对于高层，我们建议开发一个信息流类型系统和匹配的推理方法，以确保所需的信息流。我们将与我们的工业合作伙伴华为技术加拿大有限公司共同开发案例研究和基准，并将用于展示所开发方法的有效性。