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

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

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.