Research Infrastructure

Privacy is critical to freedom of creativity and innovation. Assured privacy protection offers unprecedented opportunities for industry innovation, science and engineering discovery, as well as new life enhancing experiences and opportunities.

This project is investigating the potential for language-based security techniques in the construction of low-level systems software. The specific focus is on the development of an open, capability-enhanced microkernel whose design is based on seL4, a "security enhanced" version of the L4 microkernel that was developed, by a team in Australia, as the first fully verified, general purpose operating system.

The World Wide Web and computer "clouds" have become widely used, and are interwoven into many activities of daily life, from shopping to socializing to education. But the data center servers that are the backbone of this richly connected world remain vulnerable to malicious software ("malware"). Over the past decade, attacks have increased in number and sophistication, motivated by both financial and political goals. The results include consumer concerns about identify theft and fraudulent charges, corporate concerns about millions of dollars in losses, and potential defense concerns.

The modern web experience is dynamic, providing users with a highly responsive interface through which to interact with the world. Today's mechanisms allow servers---even those which are controlled by an attacker---to download arbitrary programs into a user's browser. It is extraordinarily difficult to secure the web browser (and its user) against attack in this scenario. While tools and techniques are useful to analyze and restrict downloaded code, they are by their very nature incomplete. As a result, the security of web services relies on a series of ad hoc, service-provided techniques.

As companies collect consumer data in increasingly larger quantity and mine the data more deeply, trade-offs arise with respect to companies' practices about information privacy. A company may choose practices that augment targeted advertisements or services. However, the financial rewards associated with privacy practices are highly uncertain, since they are affected by a company's competition with rivals.