Research Introduction

Securing computer systems is one of the fundamental challenges in computer science today. But what does a "secure" system mean, how does one precisely state the security requirements a system should satisfy? And how does one check that a system satisfies these stated requirements? Answering these questions is the objective of our lab's research.

Problem Areas

Our research is application-driven and aims to build verifiably secure systems. This will require innovation in system design (systems research), enforcement mechanisms (security research) and verification methods (formal methods research). Specific problem areas are given below.

Also see the publications page for more information.

Transient Execution Attacks

Public disclosure of the Spectre and Meltodown has triggered an avalanche of newly discovered transient execution attacks, as well as research into mitigations against these attacks. It turns out that mitigating these attacks is not straightforward and in fact some mitigations have been found to be incomplete. Some research goes a step further and suggests that mitigations are basically infeasible.

However, we disagree! Our work shows it is indeed feasible to provide security against transient execution vulnerabilities. But this doesn't mean the problem is solved. What we shown is a proof-of-concept for small programs. We are interested in taking the methodology further in two directions. On the computer architecture side, we would like to investigate new architectures that can provide provable security against these attacks. One the program verification side, we would like to develop program analyses to detect and fortify code vulnerable to these attacks.

Formal Methods for Hardware Security Validation

While recent years have seen enormous strides made in automated methods for finding bugs/proving correctness of programs, security validation continues to present unique challenges. Automated techniques for finding these bugs are the subject of much ongoing research. Our lab is interested in developing new algorithms for verifying security properties of systems-on-chip platforms.

We are interested in studying methods for the verification of hyperproperties in hardware designs. In particular we are interested in the secure information flow problem. Our past work has shown that secure information flow verification is closely related to taint analysis. While that work showed modest performance improvement for the verification for certain properties, our current work is taking this connection one step further to enable scalable security verification.

Trusted Hardware Platforms

A potentially promising direction for construction of secure systems are trusted hardware platforms like SGX and Keystone. These platforms can potentially be used to securely compute on private data in the presence of an untrusted software stack; a feature that is desirable in many applications, e.g., secure access to Aadhar databases and processing of health records.

While these platforms promise attractive security guarantees, ensuring these promises are kept is a challenge that our lab is addressing: we are investigating secure platform designs and security verification algorithms targeted at these platforms. For instance, our current work is investigating the use of ORAM to mitigate side-channel attacks on these platforms. This work also poses new verification questions. For instance, it turns out that verification of an ORAM implementation is not possible using existing work on secure information flow. Therefore, we are developing new verification techniques to address this problem.