CRII

The development of the mobile Internet economy has brought numerous benefits to people and society, with the promise of providing ubiquitous computing and communications. Mobile devices have penetrated almost every aspect of our lives and, as a result, are storing a large amount of personal data.

Recent advances of isolated execution technologies, especially the emergence of Intel Software Guard eXtension (SGX), revolutionize the model of computer security and empower programs with sensitive data and code to be shielded from untrusted operating systems. However, their security guarantees have not yet been thoroughly investigated against the notorious vector of information leakage side-channel attacks. It is conceivable that side-channel attacks with full control of the underlying operating system are more diverse, efficient and robust than those from unprivileged programs.

Technology advances have brought numerous benefits to people and society, but also heightened risks to privacy. This project will investigate mechanisms and build tools to help people make privacy-aware decisions in different online contexts. The outcomes will help people to better understand their own privacy preferences and behavior, and enable them to better manage their privacy on the Internet. The project will create designs that can be integrated into mobile app markets and web browsers. The results will also inform Internet standards and governmental policies on Internet privacy.

Many challenging real world problems, e.g., voting and blind auction, require computation over sensitive data supplied by multiple mutually-distrustful entities. Elegant cryptographic theories have been developed to solve these problems without relying on a mutually-trusted third party. Practitioners also built prototypes capable of securely computing set intersection, AES encryption, Hamming distance, etc. However, many other applications, such as data mining and running universal machines, are far more complex than what can be supported by the state-of-the-art techniques.

This project develops a comprehensive proof construction and verification framework for a well-defined class of cryptographic protocols: attribute-based cryptosystems. In particular, existing automated proof construction and verification frameworks, such as EasyCrypt and CryptoVerif, are extended to provide support for attribute-based cryptography. The extensions consist of libraries of simple transformations, algebraic manipulations, commonly used abstractions and constructs, and proof strategies, which will help in generation and verification of proofs in attribute-based cryptography.