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

点击翻译按钮获取中文摘要

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.