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
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=692972
• 关键词: 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应用程序的高级信息流问题。对于低层，我们建议研究分层抽象以提高精确度和可伸缩性，并研究可执行的反例，作为对开发人员的有用反馈。对于高层，我们建议开发一个信息流类型的系统和匹配的推理方法，以确保期望的信息流。案例研究和基准将与我们的行业合作伙伴华为技术加拿大有限公司一起开发，并将用于展示所开发方法的有效性。