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.