Building Secure Smartphone Applications

K. Bhargavan and G. Steel

With the emergence of application markets for smartphones, hundreds of third-party applications now use cryptography to protect sensitive user data before storing it on disk or sending it out on the network. For example, applications like Google Wallet use a combination of software and hardware cryptographic APIs to protect credit-card information as it travels from the phone to a merchant’s terminal. However, using cryptographic mechanisms correctly is challenging and error-prone, even for experts. Our goal is to build tools that application developers can use to verify the security of their code.

We focus on smartphone applications written for the Android platform. Previous security analyses for these applications[Enck et al., 2010, Chin et al., 2011] have focused on information leakage and permission violations, but do not account for applications that use cryptography. Moreover, recent Android phones have an embedded “secure element”: a hardware security module that enables new kinds of security applications that are only now beginning to appear. Our aim is to verify or find vulnerabilities in such applications

In previous work, we have used cryptographic provers, such as ProVerif, and security type systems, such as F7, to verify ML programs that use software cryptography [Bhargavan et al., 2008, Bhargavan et al., 2010]. Independently, we have used a formal testing framework, Tookan, to analyze and find vulnerabilities in hardware security APIs [Bortolozzo et al., 2010]. To verify cryptographic applications written for the Android platform, we will use a combination of these techniques.

Internship.

The precise topic will be decided after discussion with the student, but during the course of the internship, the student will learn to do the following:

Some prior knowledge of cryptography, verification tools, functional programming, and type systems will be an advantage, but is not mandatory.

The internship will be located at INRIA in Paris. The dates of the internship and its duration are flexible and students of any nationality may apply. Masters students who are thinking of doing a Ph.D. are encouraged to apply for a six-month internship (i.e. a French M1/M2 stage). Ph.D. students and advanced undergraduate students (with adequate background) may apply for a three-month summer internship. We expect the research carried out during the internship will form the major part of a Masters-level thesis and lead to a conference publication. All interns are funded under the ERC grant CRYSP and successful internships are expected to lead to funded Ph.D. studentships.

Application Details.

To apply, send an email describing your research interests, and including your CV and the names and email addresses of one or two referees (professors or prior employers), to karthikeyan DOT bhargavan AT inria DOT fr. The deadline for applications is January 5, 2012. Positions will be kept open until filled.

The intern will have the opportunity to work closely with a team of researchers from INRIA and MSR-INRIA, including B. Blanchet , C. Fournet, A. Pironti, and P-Y. Strub.

Related Proposals.

References

Bhargavan et al. [2008]
K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In 15th ACM conference on Computer and Communications Security (CCS’08), pages 459–468. ACM, 2008. PDF.
Bhargavan et al. [2010]
K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In ACM Symposium on Principles of Programming Languages (POPL’10), pages 445–456, 2010. PDF.
Bortolozzo et al. [2010]
M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel. Attacking and fixing pkcs#11 security tokens. In ACM Conference on Computer and Communications Security, pages 260–269, 2010. .
Chin et al. [2011]
E. Chin, A. P. Felt, K. Greenwood, and D. Wagner. Analyzing inter-application communication in android. In MobiSys, pages 239–252, 2011.
Enck et al. [2010]
W. Enck, P. Gilbert, B.-G. Chun, L. P. Cox, J. Jung, P. McDaniel, and A. N. Sheth. Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In Proceedings of the 9th USENIX conference on Operating systems design and implementation, OSDI’10, pages 1–6, Berkeley, CA, USA, 2010. USENIX Association.

This document was translated from LATEX by HEVEA.