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

Project

Project FoodVibes

Reducing food waste and optimizing production Through the FoodVibes, we are addressing the global food challenge by developing and deploying affordable technology that helps reduce waste and optimize production. Starting from the farms, we focus…

Publication

A Security Study about Electron Applications and a Programming Methodology to Tame DOM Functionalities

Zihao Jin, Shuo Chen, Yang Chen, Haixin Duan, Jianjun Chen, Jianping Wu

Symposium on Network and Distributed System Security (NDSS) | March 2023

Video

ASPLOS’22 – Session 2B | Revizor: Testing Black-box CPUs against Speculation Contracts

March 2, 2023

ASPLOS’22: The 27th International Conference on Architectural Support for Programming Languages and Operating Systems Session 2B: Privacy and Software Security Session Chair: Baris Kasikci, University of Michigan Title: Revizor: Testing Black-box CPUs against Speculation Contracts…

17:16

Video

Revizor: Automatic Detection of Speculative Vulnerabilities (Lightning Talk for ASPLOS 2022)

March 2, 2023

Lightning Talk for ASPLOS 2022 Speaker: Oleksii Oleksenko Video: Neeltje Berger, Zane Colquhoun Speculative vulnerabilities such as Spectre and Meltdown can be exploited to leak information across security domains via side-channels. Revizor is a principled…

01:31

Tool

Revizor: a fuzzer to search for microarchitectural leaks in CPUs

This is Revizor, a microarchitectural fuzzer. Instead of finding bugs in programs, Revizor searches for microarchitectural vulnerabilities in CPUs. What is a microarchitectural vulnerability? In the context of Revizor, it is a violation of out expectations…

GitHub Video Video Project

Microsoft Research Blog

Research Focus: Week of February 6, 2023

February 8, 2023

Welcome to Research Focus, a new series of blog posts that highlights notable publications, events, code/datasets, new hires and other milestones from across the research community at Microsoft. In the latest episode of Behind the…

Microsoft Research Focus 09 edition, week of February 6, 2023

Publication

CHERIoT: Rethinking security for low-cost embedded systems

Saar Amar, Tony Chen, David Chisnall, Felix Domke, Nathaniel Filardo, Kunyan Liu, Robert Norton-Wright, Yucong Tao, Robert N. M. Watson, Hongyan Xia

MSR-TR-2023-6 | February 2023

Published by Microsoft

Github Github Github Project

Publication

Distribution Inference Risks: Identifying and Mitigating Sources of Leakage

Valentin Hartmann, Leo Meynent, Maxime Peyrard, Dimitrios Dimitriadis, Shruti Tople, Robert West

IEEE Conference on Secure and Trustworthy Machine Learning (SatML) | February 2023

Project Project

Tool

CherIoT-ibex: reference implementation of the ISA

cheriot-ibex is a RTL implementation of CHERI ISA based on LowRISC’s Ibex core. More specifically, cheri-ibex is a 32-bit RISC-V microcontroller which implements the CheriIoT ISA extension in addition to RV32IMCB. Same as the original…

GitHub Project

Tool

CherIoT Sail: formal specification of the ISA

This repository contains an implementation of the CHERIoT ISA in Sail. It contains an executable description of the CHERIoT instruction set that can be used to build an instruction set emulator and also prove properties…

GitHub Project

Security, privacy, and cryptography

Highlights