research

Differential privacy and formal verification

Decision procedures and numerical tools for checking privacy guarantees of randomized programs.

Deciding Differential Privacy of Online Algorithms with Multiple Variables

Extends DiP automata to online randomized algorithms with multiple real-valued storage variables. The paper characterizes when an automaton is Dε-differentially private for some D and every ε > 0, proves that deciding this property is PSPACE-complete, and implements an algorithm that also computes a suitable D.

Read this when: Read this when studying automated privacy verification for algorithms that process a stream of inputs, or when comparing the expressiveness and complexity of automata-based privacy analyses.

Code · Paper and citation

Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions

Introduces DipApprox for verifying differential privacy of loop-free probabilistic programs that use Gaussian and other discrete or continuous distributions. It combines numerical integration and tail bounds to approximate probabilities to arbitrary precision, with an almost-decidability result for (ε, δ)-privacy: all but a finite set of δ values are decidable under the paper’s assumptions.

Read this when: Read this when a privacy mechanism uses Gaussian noise or requires reasoning about both discrete and continuous random choices. The Sparse Vector and Noisy Max evaluations provide concrete verification examples.

Code · Paper and citation

Checking δ-Satisfiability of Reals with Integrals

Extends δ-decision procedures over the reals to constraints containing integrals of user-specified functions. The ∫dReal implementation builds on dReal and is evaluated on fairness, privacy, utility, and parameter-synthesis problems.

Read this when: Read this when a verification or synthesis task reduces to real-valued constraints involving probability integrals, including privacy-mechanism utility and algorithmic fairness.

Paper and citation

DiPAut: A Tool for Checking Differential Privacy of Online Randomized Algorithms

Provides the DiPAut software artifact for checking differential privacy of online randomized algorithms, with a versioned Zenodo record and a public implementation repository.

Read this when: Use this artifact alongside the CCS 2023 paper when looking for the implementation of automata-based privacy checking or a versioned software citation.

Code · Paper and citation

Privacy-preserving language models

Differentially private text generation, in-context learning, and optimization for language models.

Privacy Preserving In-Context-Learning Framework for Large Language Models

Presents a differentially private prediction framework that generates synthetic text by aggregating clipped per-token logits from inference over private records, without fine-tuning the underlying language model. A blending operation combines private and public inference to improve utility in the evaluated in-context-learning tasks.

Read this when: Read this when exploring how to use sensitive examples for language-model predictions or synthetic demonstrations with differential privacy, particularly when updating model weights is undesirable.

Code · Paper and citation

Inner Momentum for Differentially Private Muon

Studies how unequal per-example clipping factors can distort the singular-vector geometry used by Muon. The proposed inner-momentum method averages each sampled example’s gradients across the current and recent models before clipping. The preprint gives a distortion analysis and reports improved BLEU and ROUGE-L over DP-Muon in seed-matched private GPT-2 fine-tuning on E2E and DART at ε ∈ {1, 2, 4, 8}.

Read this when: Read this when studying differentially private optimizers, gradient-clipping geometry, or the interaction between Muon’s orthogonalization and private language-model fine-tuning.

Paper and citation

Security and privacy in practice

Strategic cyber defense, privacy communication, and verification of security-sensitive systems.

On Countering Ransomware Attacks Using Strategic Deception

Models ransomware defense as a multistage game with honeytokens, honeypots, honeyfiles, and network honeypots. The paper uses backward induction to analyze subgame-perfect Nash equilibria and evaluates the defender’s choices through a numerical healthcare case study informed by real-world data and statistics.

Read this when: Read this when analyzing how deception resources can change an attacker’s incentives across ransomware stages, or when building game-theoretic models of cyber defense.

Code · Paper and citation

Privacy Nutrition Labels: Promise, Practice, and Paradoxes in Communicating Privacy

Reviews privacy nutrition label research from 2009 to 2024 using qualitative coding of 78 papers. The study maps the communities, goals, and methods represented in the literature, identifies gaps, and provides a dataset with qualitative codes for further analysis.

Read this when: Read this when designing a study of privacy labels, reviewing how privacy practices are communicated, or looking for a starting dataset and research gaps in usable privacy.

Code · Paper and citation

Formal Verification for Blockchain-based Insurance Claims Processing

Models blockchain-based insurance claims processing and checks the underlying chaincodes using linear temporal logic and model checking. The modeled stages include issuing claims, approving or denying them, and flagging claims for fraud investigation.

Read this when: Read this when studying formal verification of blockchain workflows that coordinate multiple participants, particularly insurance claims and their transaction-processing logic.

Paper and citation