Fine-Grained, Language-Based Access Control for Database-Backed Applications

• Thesis

• Extended Abstract

• GitHub

Database-backed applications often run queries with more authority than necessary. Since programs can access more data than they legitimately need, flaws in security checks at the application level can enable malicious or buggy code to view or modify data in violation of intended access control policies. Although database management systems provide tools for controlling access to data, these tools are not well-suited for modern web applications which often have many users and consist of many different software components. First, databases are unaware of application users, and creating a new database user for each application user is impractical for applications with many users. Second, different components of the same application require different levels of database access, which would require creating different database users for different software components. Thus, it is difficult to properly limit the authority an application has when executing queries.

I propose ShillDB, a language for writing secure, database-backed applications. ShillDB enables reasoning about database access at the language level through capabilities, which limit what database tables a program can access, and contracts, which limit what operations a program can perform on those tables. ShillDB contracts are expressed as part of function interfaces, making it easy to specify different access control policies for different components of an application. These contracts act as executable security documentation for consumers of ShillDB programs and are enforced by the language runtime. Further, ShillDB provides database access control guarantees independent of the security mechanisms of the underlying database management system.

Reaper: Synthesizing SQL Data Modification Queries from Input-Output Examples

• Read the Paper

• GitHub

A final project for Advanced Topics in Programming Languages at Harvard.

Users of relational databases often have trouble constructing SQL queries to perform their desired tasks. However, users are often able to provide input-output examples that provide a partial specification for their desired outcome. Accordingly, prior work has developed programming-by-example systems to help users craft database SELECT queries. A natural and useful extension of this technique is to automatically synthesize queries that modify data (that is, UPDATE and DELETE queries), as even users who are proficient in writing SELECT queries may struggle to write these modification queries.

In this paper, we present the first system for synthesizing SQL data modification queries from input-output examples. Our key insight is that it is possible to solve SQL data modification query synthesis problems by issuing multiple, independent calls to an existing SELECT synthesizer, which we can treat as a black box. This results in a simple synthesis algorithm that will benefit from future advances in SELECT synthesis technology. We have implemented our algorithm in a new tool called REAPER which can solve a variety of interesting update problems in a few seconds.

Verifying Security of Enclave-Aware Calculi

• Read the Paper

• GitHub

A final project for Projects and Close Readings in Software Systems: Verified Systems at Harvard.

We model in Coq a security-typed calculus that includes an abstract model of Intel SGX-like enclaves, and show that the calculus provides meaningful security guarantees, even in the face of low-level attackers. We also model a translation scheme from an enclave-agnostic calculus to an enclave-aware calculus and show that the scheme ensures that enclaves are correctly placed, so that a translation of a well-typed program in the enclave-agnostic calculus results in a well-typed program in the enclave-aware calculus.

Accelerating Good (and Evil): Using Accelerometer Data to Catch Spam (and Spy on People)

• Read the Paper

• GitHub

A final project for System Security at Harvard.

To prevent automated systems from accessing certain webpages, website developers often wish to verify that a user is a human. This generally involves asking a user to perform tasks that are relatively easy for humans but difficult for automated systems. One of the most popular such methods is CAPTCHA. However, these tasks can still be difficult or unpleasant to complete for humans. In general, they can reduce the quality of user experience, which may make a user frustrated when interacting with a system, particularly for those with disabilities.

To address these issues, we explore a replacement for CAPTCHA that uses a mobile client’s accelerometer data to determine whether the client is an automated system. We also examine the privacy implications of websites clandestinely collecting accelerometer data.