illustration of lock, four asterisks and a shield with a fingerprint on it on a green gradient background

Security, privacy, and cryptography

Leveraging Large Language Models for Automated Proof Synthesis in Rust

photos of PhD students Anunay Kulshrestha and Karan Newatia with a photo of Senior Cryptographer Josh Benaloh in the middle with a microphone icon on a blue and purple gradient background

Intern Insights: Dr. Josh Benaloh with Anunay Kulshrestha and Karan Newatia

Bayes Security (β*, higher better) of DP-SGD against membership and attribute inference on the Adult and Purchase datasets as a function of the number of training steps. The green dashed line shows the corresponding DP budget (ε). Membership and attribute inference curves decrease monotonically as the model is trained for longer and the accuracy and DP budget grow.

Closed-Form Bounds for DP-SGD against Record-level Inference

ProvCam: A Camera Module with Self-Contained TCB for Producing Verifiable Videos

Current selections

Sort by: Most recent

Clear selections

Search within these results

Content Types

Published Date

Video

How to: Microsoft Security Risk Detection (Fuzzing)

June 28, 2019 | Ram Nagaraja

Microsoft Security Risk Detection (MSRD): How to fuzz

Video: Microsoft Security Risk Detection

0:27:38

Tool

Vale

Vale (Verified Assembly Language for Everest) is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal…

GitHub Publication Publication Publication

Tool

EverCrypt

EverCrypt (opens in new tab) is a high-performance, cross-platform, formally verified modern cryptographic provider distributed as a combined C/ASM library. EverCrypt packages cryptographic implementations from the HACL* and ValeCrypt projects, and automatically picks the fastest…

GitHub Publication Publication Publication Publication Publication

Tool

FStar

F*: Verification system for effectful programs

GitHub Publication

Video

PASTA: PASsword-based Threshold Authentication

June 24, 2019 | Peihan Miao

We introduce and formalize a new notion of password-based threshold token authentication, which protects password-based authentication against single point of failures. Specifically, we distribute the role of a single server among n servers and allow…

Peihan Miao giving a talk at Microsoft Research

0:45:41

Publication

snmalloc: A message passing Allocator

David Chisnall, Sylvan Clebsch, Sophia Drossopoulou, Juliana Vicente Franco, Paul Lietar, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger

ISSM | June 2019, pp. 122-135

Project

Video

SIKE in Hardware for IoT

June 18, 2019 | Reza Azarderakhsh

Elliptic curve groups have been a popular choice in the implementation of traditional and post-quantum cryptographic schemes, including Diffie-Hellman type key-exchange protocols and digital signature algorithms. While some of these applications require to perform multidimensional…

1:13:08

Publication

Permissions Plugins as Android Apps

Nisarg Raval, Ali Razeen, Ashwin Machanavajjhala, Landon Cox, Andrew Warfield

MobiSys | June 2019

Tool

AVML (Acquire Volatile Memory for Linux)

A portable volatile memory acquisition tool for Linux. AVML is an X86_64 userland volatile memory acquisition tool written in Rust, intended to be deployed as a static binary. AVML can be used to acquire memory…

GitHub

Video

Installing Microsoft SEAL on Windows

June 4, 2019 | Kim Laine

A tutorial on how to install Microsoft SEAL on Windows.

0:05:03

Security, privacy, and cryptography

Highlights