I am currently an engineer on the Hack team within Facebook’s Programming Languages and Runtimes group. Our mission is to make the Hack Programming Language more expressive and typesafe in order to improve the engineering efficiency of the thousands of Facebook engineers that use Hack.
In particular, I am interested in ways to automatically check correctness invariants of Hack code. My current focus in on privacy invariants. I am leading an initiative to add privacy awareness to Hack using a combination of effects and Information Flow Control.
Eliminating Bugs with Dependent Haskell
This work was published in the 13th ACM SIGPLAN International Haskell Symposium (Haskell ’20)
For five years, I worked on the Sigma project at Facebook. Sigma is a rule engine used to detect abusive content on Facebook’s family of apps (eg spam, fraud, fake accounts). To my knowledge, this is the largest scale production Haskell system in the world, handling over one million requests per second.
In my time working on Sigma, I used cutting edge software development techniques in order to ensure the correctness of my code. This mostly involved using dependent types to encode invariants at the type level.
I found that using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. My work has been shown to find and eliminate bugs in production Haskell code.
Formal Verification of System FC Using the Coq Proof Assistant
Haskell is a statically-typed functional programming language that is commonly used for the robust compile-time guarantees provided by its type system. Despite this usage, the type safety of Haskell has not been mechanically proven; it may be possible to write Haskell programs that type-check at compile-time but fall into an inconsistent state at runtime. Many safety critical systems such as flight controllers, self driving cars, and missile controllers are powered by software. If the type systems underlying this code are not verified, then the code itself is unsafe.
This work approaches this problem by verifying System FC, the formalization of the core language of the Haskell compiler. It presents a mechanized proof for a large subset of System FC using the Coq Proof Assistant. The type system of System FC is the basis for the type system of Haskell, so the results translate directly into safety guarantees at the program level.
A Zero-Knowledge Protocol for Keystroke Authentication
Research project for CIS 700: Special Topics in Cryptography.
We present a zero-knowledge protocol to authenticate users without the use of a password. Passwords have many inherent problems; several well known companies such as Dropbox and Apple have recently been targets of large scale security breaches in which passwords were compromised. Because of this risk, users are urged to use different passwords for each account. However, it is very inconvenient to create and remember enough secure passwords considering how many online accounts most people have today.
Keystroke Dynamics have successfully been used in the past to authenticate users, however previous work has not addressed how to transmit the user’s keystroke timing securely. We have built on previous work to create a zero-knowledge protocol using a fuzzy extractor.