Security, privacy, and cryptography
Video
Incentivizing Outsourced Computation
We describe different strategies a central authority, the boss, can use to distribute computation to untrusted contractors. Our problem is inspired by volunteer distributed computing projects such as SETI@home, which outsource computation to large numbers…
Publication
Incentivizing Outsourced Computation
Video
Two-dimensional mod p Galois representations attached to modular forms
Classical newforms are cusp forms on congruence subgroups of SL(2,Z) that are eigenvectors for the Hecke operators. These modular forms give rise to two-dimensional representations of the absolute Galois group of the rational field. Conversely,…
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,…