@phdthesis{21401, abstract = {Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification. In this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation. The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally. }, author = {Karimi, Mahyar}, issn = {2791-4585}, keywords = {Privacy-preserving verification, Runtime verification, Monitoring, Reactive functionalities, Cryptographic protocols}, pages = {60}, publisher = {Institute of Science and Technology Austria}, title = {{Privacy-preserving runtime verification}}, doi = {10.15479/AT-ISTA-21401}, year = {2026}, } @article{22318, abstract = {Many intended uses of differential privacy involve a continual mechanism that is set up to run continuously over a long period of time, making more statistical releases as either queries come in or the dataset is updated. In this paper, we give the first general treatment of privacy against adaptive adversaries for mechanisms that support dataset updates and a variety of queries, all arbitrarily interleaved. It also models a very general notion of neighboring, that includes both event-level and user-level privacy. We prove several concurrent composition theorems for continual mechanisms, which ensure privacy even when an adversary can interleave its queries and dataset updates to the different composed mechanisms. Previous concurrent composition theorems for differential privacy were only for the case when the dataset is static, with no adaptive updates. We also give the first interactive and continual generalizations of the “parallel composition theorem” for noninteractive differential privacy. Specifically, we show that the analogue of the noninteractive parallel composition theorem holds if either there are no adaptive dataset updates or each of the composed mechanisms satisfies pure differential privacy, but it fails to hold for composing approximately differentially private mechanisms with dataset updates. Thus, we prove a tight new composition theorem for this case. In addition, we prove concurrent filter compositions theorems for the scenarios in which the privacy parameters are adaptively chosen. We extend these results to other measures of differential privacy, including Rényi DP and 𝑓 -DP. We then formalize a set of general conditions on a continual mechanism M that runs multiple continual submechanisms such that the privacy guarantees of M follow directly using the above concurrent composition theorems on the sub-mechanisms, without further privacy loss. This enables us to give a simpler and modular privacy analysis of a recent continual histogram mechanism of Henzinger, Sricharan, and Steiner. In the case of approximate DP, ours is the first proof that shows that its privacy holds against adaptive adversaries. We also provide a framework that simplifies the analysis of local differential privacy when the protocol includes multi-round server-user interactions. Using this result, we simplify the privacy analysis of the core decomposition protocol of Dhulipala, Henzinger, Li, Liu, Sricharan, and Zhu [5].}, author = {Henzinger, Monika H and Safavi Hemami, Roodabeh and Vadhan, Salil}, issn = {2836-6573}, journal = {Proceedings of the ACM on Management of Data}, keywords = {differential privacy, concurrent composition, continual release, continual observation, data streaming, continual mechanisms, concurrent parallel composition, concurrent filter composition}, number = {2}, pages = {1--26}, publisher = {Association for Computing Machinery}, title = {{Concurrent composition for differentially private continual mechanisms}}, doi = {10.1145/3801895}, volume = {4}, year = {2026}, } @inproceedings{22146, abstract = {We study differentially private model training with stochastic gradient descent under learning rate scheduling and correlated noise. Although correlated noise, in particular via matrix factorizations, has been shown to improve accuracy, prior theoretical work focused primarily on the prefix-sum workload. That workload assumes a constant learning rate, whereas in practice learning rate schedules are widely used to accelerate training and improve convergence. We close this gap by deriving general upper and lower bounds for a broad class of learning rate schedules in both single- and multi-epoch settings. Building on these results, we propose a learning-rate-aware factorization that achieves improvements over prefix-sum factorizations under both MaxSE and MeanSE error metrics. Our theoretical analysis yields memory-efficient constructions suitable for practical deployment, and experiments on CIFAR-10 and IMDB datasets confirm that schedule-aware factorizations improve accuracy in private training.}, author = {Kalinin, Nikita and Andersson, Joel D}, booktitle = {7th Symposium on Foundations of Responsible Computing}, isbn = {9783959774192}, issn = {1868-8969}, keywords = {differential privacy, machine learning, matrix factorization}, location = {Cambridge, MA; United States}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Learning rate scheduling with matrix factorization for private training}}, doi = {10.4230/LIPIcs.FORC.2026.2}, volume = {368}, year = {2026}, } @article{22102, abstract = {Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Zikelic, Dorde}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, keywords = {Static Program Analysis, Differential Privacy, Probabilistic Programming, Martingales}, number = {PLDI}, publisher = {ACM}, title = {{SuperDP: Differential privacy refutation via supermartingales}}, doi = {10.1145/3808296}, volume = {10}, year = {2026}, } @phdthesis{22857, abstract = {Artificial intelligence and machine learning have undergone an unprecedented evolution in the past decade, motivating a research effort toward a theory able to capture the qualitative behavior of large-scale neural systems. A central puzzle has been the clear benefit of scaling architecture size and overfitting the training set in supervised learning tasks. This evidence, in apparent contradiction with classical statistical learning theory, pushed researchers to develop a new theory capturing the interplay between the algorithmic and architectural bias of training and the specific target function, differently from previous methods rooted in uniform stability. This approach has enabled a grounded understanding of novel learning regimes, typically through formal limits where the number of training samples $n$, data dimensions $d$, and model parameters $p$ grow to infinity at different rates. \\ In this thesis, we follow this approach, focusing on the trustworthiness of high-dimensional models: properties that are difficult to control during training or deployment and often emerge under unpredictable or adversarial conditions. In such settings, it is crucial to formally ensure a priori the reliability of machine learning systems. First, we study data memorization, both as label fitting and as the storage of private information about training samples in trained parameters. We prove that $p = \Omega(n)$ parameters are sufficient for a deep neural network to memorize a generic set of labels, and for a model to memorize spurious features across training data. We then give evidence that $p = \Omega(dn)$ parameters are instead necessary for an adversary to reconstruct the full training set from the trained parameters. Second, we study robustness, both to adversarial perturbations and to distribution shift. We first prove that $p = \Omega(dn)$ parameters can be sufficient for a class of neural networks to overfit the training data while guaranteeing robustness to adversarial perturbations. Then, we focus on spurious correlations learning in high-dimensional regression, studying the effect of the ridge regularization parameter in the proportional regime $n = \Theta(d)$, and connecting it via an equivalence argument to the role of over-parameterization $p = \Omega(n)$ in neural networks. We also investigate the architectural bias of attention-based networks, showing that they are sensitive to the replacement of individual words in an embedded sentence, allowing them to generalize on sentences where the contextual meaning depends on one or few words. Finally, we study differentially private optimization in high-dimensional regimes. We prove that standard private gradient methods do not suffer in the over-parameterized regime $p = \Omega(n)$, challenging the current wisdom based on stability-derived generalization bounds. We then consider linear regression in the proportional regime $n = \Theta(d)$, showing that standard private gradient descent can achieve optimal rates under appropriate hyper-parameter scaling, such as sufficiently small gradient clipping constants, whose role is still debated in practice.}, author = {Bombari, Simone}, isbn = {978-3-99078-091-6}, issn = {2663-337X}, keywords = {machine learning, high-dimensional statistics, deep learning theory, privacy, memorization, robustness}, pages = {446}, publisher = {Institute of Science and Technology Austria}, title = {{Trustworthy machine learning in high dimensions}}, doi = {10.15479/AT-ISTA-22857}, year = {2026}, }