Security, privacy, and cryptography
Video
Deterministic Encryption: Theory and Applications
The focus of the talk is deterministic public-key encryption schemes. Besides being interesting from theoretical and historical perspectives, the deterministic encryption primitive has applications to fast and secure search on remote data. We study several…
Publication
Refinement Types for Secure Implementations
Video
Building Secure Systems from Buggy Code with Information Flow Control
Today, computer security resembles an arms race: the bad guys constantly find new ways to break in, and being safe requires staying one step ahead of them in cutting off avenues of attack. This strategy…
Project
F7: Refinement Types for F#
F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties,…
Publication
Preventing memory error exploits with WIT
Publication