Abstract: Applications that combine code and data from multiple sources are hard to program and even harder to get right. For example, cryptographic protocols for Secure Multi-party Computation (SMC) are known for a long time. Yet, existing SMC frameworks neither provide an easy-to-use programming model, nor allow for formal reasoning about the correctness and security of SMC applications. As another example, for web applications that host content from different origins, programmers often struggle to enforce fine-grained separation between different JavaScript components, leading to critical security vulnerabilities. In this talk, I present my work that addresses these problems.
First, I present Wys*, a new SMC domain-specific language hosted in F*, a verification-oriented programming language developed at Microsoft Research. Wys* allows programmers to program rich, reactive SMC applications as if they were regular, single-threaded F* programs, and execute them using a low-level distributed semantics. The single-threaded semantics enables programmers to seamlessly use F*'s logic for verifying the correctness and security properties of their SMC programs. We have formally proved (again, using F*) that the properties verified for the Wys* source programs carry over when the programs are run using the low-level semantics. We have programmed and verified several SMC applications in Wys*, including a novel card dealing application.
Next, I present Safe TypeScript, a sound and efficient gradual type system for TypeScript, a typed superset of JavaScript. Safe TypeScript introduces two novel ideas: differential subtyping and an erased type modality. While differential subtyping ensures that at runtime, objects are instrumented with minimum amount of runtime type information needed for type safety, the erased type modality provides safe and controlled type erasure along with fine-grained information hiding. We have empirically evaluated Safe TypeScript on 120,000 lines of existing code, including bootstrapping the Safe TypeScript compiler itself (90,000 LOC), for which we measure a 15% runtime overhead of type safety.
Bio: Aseem Rastogi is a PhD candidate in the Computer Science Department at the University of Maryland, College Park. His research applies formal methods in programming languages to design abstractions that simplify the task of programming software systems, and enable programmers to state and enforce crucial invariants such as those related to the correctness and security of the software. Before joining the University of Maryland, Aseem obtained an MS in Computer Science from the State University of New York at Stony Brook.
