329 citations · 530 across the 15 of their papers we have counts for
19 papers
Learning Filter-Aware Distance Metrics for Nearest Neighbor Search with Multiple Filters
Ananya Sutradhar, Suryansh Gupta, Ravishankar Krishnaswamy +3
Filtered Approximate Nearest Neighbor (ANN) search retrieves the closest vectors for a query vector from a dataset. It enforces that a specified set of discrete labels for the…
Automatically Verifying Replication-aware Linearizability
Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi +1
Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Data Types (RDTs) have emerged as a principled app…
Enabling Memory Safety of C Programs using LLMs
Nausheen Mohammed, Akash Lal, Aseem Rastogi +2
Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such viola…
Finding Inductive Loop Invariants using Large Language Models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty +6
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become u…
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury +6
Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable…
Fixing Rust Compilation Errors using LLMs
Pantazis Deligiannis, Akash Lal, Nikita Mehrotra +1
The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alterna…
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz +3
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to bu…
SIRNN: A Math Library for Secure RNN Inference
Deevashwer Rathee, Mayank Rathee, Rahul Kranti Kiran Goli +4
Complex machine learning (ML) inference algorithms like recurrent neural networks (RNNs) use standard functions from math libraries like exponentiation, sigmoid, tanh, and reciproc…
Secure Medical Image Analysis with CrypTFlow
Javier Alvarez-Valle, Pratik Bhatu, Nishanth Chandran +6
We present CRYPTFLOW, a system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we build two compone…
CrypTFlow2: Practical 2-Party Secure Inference
Deevashwer Rathee, Mayank Rathee, Nishant Kumar +4
We present CrypTFlow2, a cryptographic framework for secure inference over realistic Deep Neural Networks (DNNs) using secure 2-party computation. CrypTFlow2 protocols are both cor…
CrypTFlow: Secure TensorFlow Inference
Nishant Kumar, Mayank Rathee, Nishanth Chandran +3
We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we…
Reliable State Machines: A Framework for Programming Reliable Cloud Services
Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj +5
Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Relia…
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
CONFLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code
Ajay Brahmakshatriya, Piyus Kedia, Derrick Paul McKee +4
We present an instrumenting compiler for enforcing data confidentiality in low-level applications (e.g. those written in C) in the presence of an active adversary. In our approach,…
WYS*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. Thi…
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu +3
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the…
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi +8
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a sm…
Dijkstra Monads for Free
Danel Ahman, Catalin Hritcu, Kenji Maillard +5
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely relate…