At SRI from 2017 to 2022:

High-assurance Cryptographic Protocols and Algorithms

This repository contains papers and software on computer-aided verification and automated synthesis of high-assurance cryptographic protocols and algorithms, e.g., secure multiparty computation (MPC), and zero-knowledge (ZK) via MPC-in-the-Head.

Automated-instrumentation of Legacy Insecure Cryptographic Executables (ALICE)

This repository contains papers and software exploreing feasibility of developing a toolchain for Automated-instrumentation of Legacy Insecure Cryptographic Executables (ALICE). The key features of ALICE are: (i) automatically detecting and extracting implementations of weak or broken cryptographic primitives from binaries without requiring source code or debugging symbols, (ii) identifying the context and scope in which such primitives are used, and performing program analysis to determine the effects of replacing such implementations with more secure ones, and (iii) replacing implementations of weak primitives with those of stronger or more secure ones.