# Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems

arXiv: https://arxiv.org/abs/2110.02125 · HTML: https://mlsanity.com/paper/2110.02125/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 49 references that are in the map.
- First posted on arXiv 5 Oct 2021.

## Builds on (most cited first, 13 of 13)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Evasion Attacks against Machine Learning at Test Time](https://mlsanity.com/paper/1708.06131/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Parameter Synthesis for Markov Models: Faster Than Ever](https://mlsanity.com/paper/1602.05113/) (2016)
- [Synthesis in pMDPs: A Tale of 1001 Parameters](https://mlsanity.com/paper/1803.02884/) (2018)
- [The Complexity of Reachability in Parametric Markov Decision Processes](https://mlsanity.com/paper/2009.13128/) (2020)

## Abstract (arXiv)

Probabilistic model checking is a useful technique for specifying and verifying properties of stochastic systems including randomized protocols and reinforcement learning models. Existing methods rely on the assumed structure and probabilities of certain system transitions. These assumptions may be incorrect, and may even be violated by an adversary who gains control of system components. In this paper, we develop a formal framework for adversarial robustness in systems modeled as discrete time Markov chains (DTMCs). We base our framework on existing methods for verifying probabilistic temporal logic properties and extend it to include deterministic, memoryless policies acting in Markov decision processes (MDPs). Our framework includes a flexible approach for specifying structure-preserving and non structure-preserving adversarial models. We outline a class of threat models under which adversaries can perturb system transitions, constrained by an varepsilon ball around the original transition probabilities. We define three main DTMC adversarial robustness problems: adversarial robustness verification, maximal δ synthesis, and worst case attack synthesis. We present two optimization-based solutions to these three problems, leveraging traditional and parametric probabilistic model checking techniques. We then evaluate our solutions on two stochastic protocols and a collection of Grid World case studies, which model an agent acting in an environment described as an MDP. We find that the parametric solution results in fast computation for small parameter spaces. In the case of less restrictive (stronger) adversaries, the number of parameters increases, and directly computing property satisfaction probabilities is more scalable. We demonstrate the usefulness of our definitions and solutions by comparing system outcomes over various properties, threat models, and case studies.