Pith. sign in

REVIEW 1 major objections 7 minor 24 references

Privacy-Preserving Robustness Verification for Neural Networks

T0 review · 1 major / 7 minor · reviewed 2026-07-07 · glm-5.2

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read SecureCROWN verifies neural network robustness without exposing model or data

desk verdict First 2PC protocol for neural network robustness verification; soundness gap from stability constant is real but bounded and acknowledged. read the letter →

arxiv 2607.05251 v1 pith:3S6BRMFI submitted 2026-07-06 cs.CR cs.AIcs.LGcs.LO

Nianyun Song , Xiaokun Luan , Yu Guo , Rongfang Bie , Meng Sun , Xiyue Zhang This is my paper
classification cs.CRcs.AIcs.LGcs.LO
keywords verificationdatamodelneuralrobustnessnetworkprivacy-preservingbranching
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

SecureCROWN is a protocol that lets two parties jointly verify the robustness of a neural network without either party revealing their private data. A model owner holds proprietary network parameters; a data owner holds sensitive input data. Using secure two-party computation (2PC), the protocol computes the same certified robustness bounds that a standard plaintext verifier would produce, revealing only the final yes-or-no-no result. The central technical obstacle is that robustness verification via Linear Bound Propagation requires data-dependent conditional branches (to determine ReLU activation states and coefficient signs), which are expensive or incompatible with secure computation protocols. SecureCROWN eliminates all such branching by reformulating every piecewise conditional as a unified arithmetic expression built from ReLU operations, which can be efficiently evaluated under secret sharing using function secret sharing (FSS) primitives. A Newton–Raphson refinement step is added to maintain numerical precision during secure division, since fixed-point rounding errors accumulate through the deep backward recursion that verification requires. The paper provides formal semi-honest security guarantees and shows experimentally that the protocol matches plaintext verification decisions with 100% consistency across eight network architectures, with runtimes ranging from 0.1 to 200 seconds.

What carries the argument

Secure two-party computation (2PC) with additive secret sharing; function secret sharing (FSS) for efficient secure ReLU and comparison operations; branch-free reformulation of CROWN's Linear Bound Propagation; Newton–Raphson refinement for secure reciprocal computation; semi-honest security model with trusted dealer for offline preprocessing

What would settle it

A network and input where the certified margin lies within O(epsilon_s) of zero, causing SecureCROWN to return a different verification decision than plaintext CROWN.

Watch

Extended reading notes

Core claim

The key discovery is that the conditional logic inherent in CROWN-style neural network robustness verification—specifically, the piecewise definitions of ReLU relaxation slopes and the sign-dependent intercept accumulation in backward bound propagation—can be completely eliminated by reformulating conditionals as continuous arithmetic expressions using ReLU itself as a selector. This reformulation makes the entire verification circuit branch-free, enabling efficient vectorized execution under secure two-party computation. Combined with a Newton–Raphson-based reciprocal refinement to control division precision in fixed-point arithmetic, this yields a protocol that provably protects both model

Load-bearing premise

The stability constant epsilon_s is added to the denominator of the slope computation to prevent division by zero, but it perturbs the relaxation away from its ideal form. The paper acknowledges that if this perturbation shifts a certified margin across zero, the verification outcome could change, and a full slope–intercept co-adjustment restoring provable soundness is left for future work.

Editorial extensions

If this is right

  • Privacy-preserving robustness verification becomes feasible in regulated domains (healthcare, finance) where model parameters are proprietary and input data is protected by law, removing the requirement that a single party hold both model and data in plaintext.
  • The branch elimination technique—reformulating piecewise conditionals as ReLU-based arithmetic—may transfer to other verification methods beyond CROWN that also rely on data-dependent branching, potentially enabling a broader class of privacy-preserving formal verification tools.
  • The error analysis showing depth-dependent error growth in fixed-point secure computation identifies a structural tension between verification depth and cryptographic precision, motivating future work on adaptive precision or soundness-preserving perturbation bounds.
  • The protocol's compatibility with batch preprocessing (generating correlated randomness offline for multiple queries) suggests a practical deployment model where a model owner pre-generates verification capacity amortized across many client queries.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the branch-free reformulation strategy generalizes, it could enable privacy-preserving versions of complete verifiers (e.g., branch-and-bound methods) that use conditional logic more extensively than CROWN's incomplete verification, though at higher computational cost.
  • The 100% verification consistency observed empirically, combined with the acknowledged theoretical gap around the stability constant's effect on soundness, suggests that the practical soundness boundary depends on the distribution of certified margins near zero—an empirical property of trained networks rather than a worst-case guarantee.
  • The communication cost scaling as O(L²d²) for L-layer networks of width d implies a practical depth limit beyond which online verification becomes prohibitively expensive, potentially constraining applicability to moderately deep fully-connected networks unless convolution-specific optimizations are developed.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

1 major / 7 minor

Summary. The paper presents SecureCROWN, the first framework for privacy-preserving neural network robustness verification using 2PC. The framework enables a model owner and a data owner to jointly compute certified robustness bounds via Linear Bound Propagation (LBP) under the semi-honest security model. The key technical contribution is a branch-free reformulation of the conditional logic in CROWN's ReLU relaxation, replacing data-dependent branching with continuous arithmetic operations (Eqs. 12-14) that can be efficiently evaluated using FSS-based primitives. A Newton-Raphson refinement is introduced for secure reciprocal computation. The paper provides a security proof via a standard hybrid argument (Theorem 6.1), complexity analysis, depth-dependent error bounds (Theorems B.1, B.2), and experiments across 8 architectures on MNIST and CIFAR-10 demonstrating 100% verification consistency with plaintext CROWN.

Significance. The paper addresses a genuine gap at the intersection of formal verification and cryptography: no prior work combines robustness verification with privacy guarantees. The branch-free reformulation of CROWN's piecewise relaxation logic into ReLU-based arithmetic (Eqs. 12-14) is an elegant and correct observation that enables efficient vectorized secure computation. The security proof follows the standard hybrid approach appropriate for the semi-honest model. The error analysis (Theorems B.1, B.2, Corollary B.3) provides depth-dependent bounds with three regimes (stable, unit-norm, unstable). The experimental evaluation is thorough, covering multiple architectures, network conditions (LAN/WAN), and near-boundary verification cases. The replication package is publicly available. The discussion of extensions to other architectures (Appendix D) and malicious security (Appendix C) is informative for future work.

major comments (1)
  1. §5.3, Eq. (12) and Remark 1 (Appendix B.3): The stability constant ε_s introduces a soundness gap that is load-bearing for the paper's central claim of faithful verification semantics. For an unstable neuron with bounds [z̲, z̄], the ideal CROWN slope is α* = z̄/(z̄ - z̲). With ε_s > 0, the perturbed slope is α' = z̄/(z̄ - z̲ + ε_s) < α*. The perturbed upper bound uses the same intercept formula β̄ = -α'·z̲, giving the line α'(z - z̲). At z = z̄, this evaluates to z̄(z̄ - z̲)/(z̄ - z̲ + ε_s) < z̄ = ReLU(z̄). Thus the perturbed upper relaxation lies below the ReLU activation at z = z̄, meaning it is not a valid upper bound. This breaks the soundness of the certified upper bound on the network output: the margin f_{y,j} could appear positive when the true worst-case margin is negative, yielding false robustness certifications. The authors acknowledge this in Remark 1 ('a verification could
minor comments (7)
  1. Table 1: The MRE values for the 'Unknown' category on MNIST 7×[256] (1.32×10⁻²) and the 'Robust' category on CIFAR-10 10×[200] (1.73×10⁻³) are notably larger than other entries. The paper should discuss whether these reflect specific numerical instability patterns and whether they approach the threshold where verification consistency could break.
  2. §7.1: The baseline plaintext CROWN is implemented in Python (single-threaded) while SecureCROWN is in C++ (4 threads). While the comparison is for correctness (not speed), clarifying this implementation difference would help readers interpret the MRE values.
  3. Table 4: The sensitivity analysis only covers MNIST 5×[256]. Given that deeper networks (7×[256], 10×[200]) show higher MRE, a sensitivity analysis on at least one deeper architecture would strengthen the claim that ε_s robustness holds across network depths.
  4. Appendix B.2, Table 5: The SecARS communication is listed as 'k+2(66)' which appears to be a specific instantiation for k=64. Clarifying the general formula would improve readability.
  5. §3.1: The notation for lower and upper bounds uses z̲ and z̄, but in some places (e.g., Eq. 2) the subscript formatting is inconsistent. Standardizing throughout would improve clarity.
  6. Appendix C: The malicious security cost comparison (3.2× online time, 8.7× communication) is informative but the MP-SPDZ baseline uses spdz2k while the paper's implementation uses FSS-based protocols. The comparison is between different protocol families, which should be noted.
  7. References: The citation for ObliviGate [Song et al., 2026] has a future publication year; this should be verified.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful and constructive review. The referee correctly identifies a soundness gap introduced by the stability constant ε_s in the slope computation (Eq. 12). We fully accept this criticism and will revise the manuscript to fix the issue. Below we address the major comment point by point.

read point-by-point responses

  1. Referee: §5.3, Eq. (12) and Remark 1 (Appendix B.3): The stability constant ε_s introduces a soundness gap. The perturbed slope α' = z̄/(z̄ - z̲ + ε_s) < α* yields an upper relaxation line that lies below ReLU(z̄) at z = z̄, meaning it is not a valid upper bound. This breaks soundness of the certified upper bound and could yield false robustness certifications.

    Authors: The referee's analysis is correct. We have verified the argument: with ε_s > 0, the perturbed slope α' = z̄/(z̄ − z̲ + ε_s) is strictly less than the optimal chord slope α* = z̄/(z̄ − z̲) for unstable neurons. Using the same intercept formula β̄ = −α'·z̲, the perturbed upper relaxation line evaluated at z = z̄ gives α'(z̄ − z̲) = z̄(z̄ − z̲)/(z̄ − z̲ + ε_s) < z̄ = ReLU(z̄). Thus the perturbed upper bound is not a valid relaxation of the ReLU activation, and the certified upper bound on the network output is not guaranteed to be sound. This is a genuine flaw in the current formulation, and we appreciate the referee identifying it precisely. revision: yes

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derivation maps plaintext CROWN to 2PC using standard cryptographic primitives without self-referential dependency.

full rationale

The paper's core derivation chain is self-contained. Eq. (12) reformulates the piecewise CROWN slope (Eq. 2) into a branch-free arithmetic expression using ReLU operations, which is a direct algebraic identity for the three cases (inactive, active, unstable). Eqs. (13)-(14) similarly reformulate the conditional intercept accumulation into ReLU-based matrix products, again by direct algebraic substitution. These reformulations are verified against the plaintext CROWN algorithm (Table 1, 100% consistency) as an external benchmark. The cryptographic primitives (Beaver triples, FSS, DCF) are cited to external work (Boyle et al. 2015, Gupta et al. 2025) and used as standard building blocks. The Newton-Raphson refinement for SecRecip is a standard numerical method. The security proof (Theorem 6.1, Appendix B.1) reduces to FSS and ASS security via a hybrid argument. The error analysis (Theorems B.1-B.2) derives depth-dependent bounds from stated assumptions (range safety, quantization error model) without invoking the target result. The epsilon_s stability constant (Eq. 12) introduces a soundness gap (Remark 1), but this is a correctness concern, not circularity: the paper does not claim epsilon_s restores soundness and explicitly defers a formal fix. No 'prediction' reduces to a fitted parameter, no self-citation is load-bearing for the central claim, and no result is defined in terms of itself.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new physical entities or mathematical objects. It uses standard cryptographic primitives (Beaver triples, FSS, DCF) and standard neural network verification concepts (CROWN, LBP). The free parameters are implementation choices for the fixed-point protocol, not fundamental theoretical constructs.

free parameters (3)
  • epsilon_s (stability constant) = 1e-4
    Introduced in Eq. (12) to prevent division-by-zero in secure slope computation. Chosen empirically; sensitivity analysis in Table 4 shows robustness to this choice.
  • n_f (fractional bits) = 26
    Fixed-point precision parameter. Set to balance accuracy and efficiency.
  • n_iter (Newton-Raphson iterations) = 1
    Number of refinement iterations for secure reciprocal computation. Chosen to double precision from the FSS seed.
assumptions (4)
  • domain assumption Semi-honest adversary model: both parties follow the protocol specification but may attempt to infer the other party's private input from their view.
    Stated in Section 4 (Threat Model). This is a standard cryptographic assumption but limits the threat model; a pathway to malicious security is discussed in Appendix C.
  • domain assumption Trusted dealer D for preprocessing: distributes correlated randomness offline without colluding with parties.
    Stated in Section 4 (Threat Model). The paper notes D can be instantiated via trusted hardware or two-party preprocessing, but the current protocol relies on this assumption.
  • domain assumption Range safety: during execution, every intermediate integer value remains within the representable range of the fixed-point format (no overflow).
    Assumption 1 in Appendix B.3. Required for the error analysis to hold.
  • standard math Quantization error model: each call to ARS introduces additive error bounded by epsilon_q = 2^-n_f.
    Assumption 2 in Appendix B.3. Standard fixed-point arithmetic assumption.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Privacy-Preserving Robustness Verification for Neural Networks." pith.science (2026). https://pith.science/paper/3S6BRMFI

@misc{pith2026260705251,
  author       = {Pith},
  title        = {Pith review of: Privacy-Preserving Robustness Verification for Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3S6BRMFI}},
  note         = {Machine review of arXiv:2607.05251}
}
read the original abstract

Neural network verification and data privacy are inherently in tension: verification demands full access to model parameters and input data, yet both are increasingly restricted by privacy regulations and intellectual property constraints. This tension has left robustness verification impractical in privacy-sensitive domains. In this work, we address this gap with SecureCROWN, the first framework for privacy-preserving neural network robustness verification. Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds -- revealing only the final result while provably protecting both parties' private data under the semi-honest security model. A key challenge is securely computing the conditional operations in Linear Bound Propagation, where the data-dependent branching is incompatible with standard secure computation protocols. We eliminate branching by formulating conditional logic as continuous arithmetic operations. Additionally, we introduce a Newton--Raphson refinement method to improve numerical stability. Extensive analysis and experiments show that SecureCROWN strictly matches plaintext verification results, while completing in 0.1--200s across varied model sizes and communication settings (LAN/WAN), demonstrating the feasibility of privacy-preserving neural network verification.

Figures

Figures reproduced from arXiv: 2607.05251 by the authors.

Figure 1
Figure 1. Online latency breakdown across network conditions and model architectures. [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Function se- cret sharing

    Elette Boyle, Niv Gilboa, and Yuval Ishai. Function se- cret sharing. InAdvances in Cryptology, EUROCRYPT 2015, volume 9057 ofLecture Notes in Computer Science, pages 337–367. Springer,

    work page 2015

  2. [2]

    Hai Duong, Linhan Li, ThanhVu Nguyen, and Matthew B. Dwyer. A DPLL(T) framework for verifying deep neural networks.CoRR, abs/2307.10266,

    work page Pith review arXiv

  3. [3]

    Hai Duong, ThanhVu Nguyen, and Matthew B. Dwyer. Neu- ralSAT: A high-performance verification tool for deep neural networks. InComputer Aided Verification, CAV 2025, volume 15932 ofLecture Notes in Computer Sci- ence, pages 409–423. Springer,

    work page 2025

  4. [4]

    Goldreich, S

    O. Goldreich, S. Micali, and A. Wigderson. How to play ANY mental game. InProceedings of the Annual ACM Symposium on Theory of Computing, STOC 1987, pages 218–229. ACM,

    work page 1987

  5. [5]

    Goodfellow, Jonathon Shlens, and Christian Szegedy

    Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. InInter- national Conference on Learning Representations, ICLR 2015,

    work page 2015

  6. [6]

    SHARK: actively secure in- ference using function secret sharing

    Kanav Gupta, Nishanth Chandran, Divya Gupta, Jonathan Katz, and Rahul Sharma. SHARK: actively secure in- ference using function secret sharing. InIEEE Sympo- sium on Security and Privacy, SP 2025, pages 2472–2490. IEEE,

    work page 2025

  7. [7]

    Dietterich

    Dan Hendrycks and Thomas G. Dietterich. Benchmarking neural network robustness to common corruptions and perturbations. InInternational Conference on Learning Representations, ICLR 2019,

    work page 2019

  8. [8]

    Dill, Kyle Julian, and Mykel J

    Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. InComputer Aided Verification, CAV 2017, volume 10426 ofLec- ture Notes in Computer Science, pages 97–117. Springer,

    work page 2017

Show all 24 references
  1. [9]

    Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shan- tanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L

    Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shan- tanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The Marabou framework for verification and analysis of deep neural ...

    2019

  2. [10]

    Learning multiple layers of features from tiny images

    Alex Krizhevsky. Learning multiple layers of features from tiny images. Technical Report TR-2009, Department of Computer Science, University of Toronto,

    2009

  3. [11]

    CrypTFlow: Secure TensorFlow inference

    Nishant Kumar, Mayank Rathee, Nishanth Chandran, Divya Gupta, Aseem Rastogi, and Rahul Sharma. CrypTFlow: Secure TensorFlow inference. InIEEE Symposium on Security and Privacy, SP 2020, pages 336–353. IEEE,

    2020

  4. [12]

    Low-complexity deep convolutional neural networks on fully homomorphic encryption using multiplexed parallel convolutions

    Eunsang Lee, Joon-Woo Lee, Junghyun Lee, Young-Sik Kim, Yongjune Kim, Jong-Seon No, and Woosuk Choi. Low-complexity deep convolutional neural networks on fully homomorphic encryption using multiplexed parallel convolutions. InInternational Conference on Machine Learning, ICML ...

    2022

  5. [13]

    HEMET: A homomorphic- encryption-friendly privacy-preserving mobile neural net- work architecture

    Qian Lou and Lei Jiang. HEMET: A homomorphic- encryption-friendly privacy-preserving mobile neural net- work architecture. InInternational Conference on Ma- chine Learning, ICML 2021, volume 139 ofProceedings of Machine Learning Research, pages 7102–7110. PMLR,

    2021

  6. [14]

    TeleSparse: Practical privacy-preserving veri- fication of deep neural networks.Proc

    Mohammad Mahdi Maheri, Hamed Haddadi, and Alex Davidson. TeleSparse: Practical privacy-preserving veri- fication of deep neural networks.Proc. Priv. Enhancing Technol., 2025(4):861–880,

    2025

  7. [15]

    ABY3: A mixed pro- tocol framework for machine learning

    Payman Mohassel and Peter Rindal. ABY3: A mixed pro- tocol framework for machine learning. InProceedings of the ACM SIGSAC Conference on Computer and Com- munications Security, CCS 2018, pages 35–52. ACM,

    2018

  8. [16]

    Neural network verification with branch-and-bound for general nonlinearities

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, volume 15696 ofLecture Notes in Comp...

    2025

  9. [17]

    Goodfellow, and Rob Fer- gus

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fer- gus. Intriguing properties of neural networks. InInter- national Conference on Learning Representations, ICLR 2014,

    2014

  10. [18]

    Sijun Tan, Brian Knott, Yuan Tian, and David J. Wu. Crypt- GPU: Fast privacy-preserving machine learning on the GPU. InIEEE Symposium on Security and Privacy, SP 2021, pages 1021–1038. IEEE,

    2021

  11. [19]

    Se- cureNN: 3-party secure computation for neural network training.Proc

    Sameer Wagh, Divya Gupta, and Nishanth Chandran. Se- cureNN: 3-party secure computation for neural network training.Proc. Priv. Enhancing Technol., 2019(3):26–49,

    2019

  12. [20]

    Falcon: Honest-majority maliciously secure framework for pri- vate deep learning.Proc

    Sameer Wagh, Shruti Tople, Fabrice Benhamouda, Eyal Kushilevitz, Prateek Mittal, and Tal Rabin. Falcon: Honest-majority maliciously secure framework for pri- vate deep learning.Proc. Priv. Enhancing Technol., 2021 (1):188–208,

    2021

  13. [21]

    Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W

    Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tago- mori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A versatile formal an...

    2024

  14. [22]

    Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. InInterna- tional Conference on Learning Representations, ICLR 2021,

    2021

  15. [23]

    Protocols for secure computations

    Andrew C Yao. Protocols for secure computations. In Proceedings of the Annual Symposium on Foundations of Computer Science, FOCS 1982, pages 160–164. IEEE,

    1982

  16. [24]

    For a target layer l, Algorithm 1 iteratesl−1 times

    proceeds layer-by-layer. For a target layer l, Algorithm 1 iteratesl−1 times. Each iteration involves:SecMatMul (1 round) → slope multiplication (1 round)→Π δ (3 rounds), yielding 5 rounds per iteration. The bias accumulation in Lines 6-7 overlaps with Πδ: the SecMatMul(⟨A⟩,⟨b...

    2021

Pith tools

Reviewed July 7, 2026 · model on record in the stance chip above.