Automated Verification of Correctness for Masked Arithmetic Programs

• URL: http://arxiv.org/abs/2305.16596v1
• Date: Fri, 26 May 2023 02:55:46 GMT
• Title: Automated Verification of Correctness for Masked Arithmetic Programs
• Authors: Mingyang Liu and Fu Song and Taolue Chen
• Abstract summary: We study the problem for masked arithmetic programs over Galois fields of characteristic 2. We propose an automated approach based on term rewriting, aided by random testing and SMT solving. We implement the approach as a new tool FISCHER and carry out extensive experiments on various benchmarks.
• Score: 7.9330271653905235
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Masking is a widely-used effective countermeasure against power side-channel attacks for implementing cryptographic algorithms. Surprisingly, few formal verification techniques have addressed a fundamental question, i.e., whether the masked program and the original (unmasked) cryptographic algorithm are functional equivalent. In this paper, we study this problem for masked arithmetic programs over Galois fields of characteristic 2. We propose an automated approach based on term rewriting, aided by random testing and SMT solving. The overall approach is sound, and complete under certain conditions which do meet in practice. We implement the approach as a new tool FISCHER and carry out extensive experiments on various benchmarks. The results confirm the effectiveness, efficiency and scalability of our approach. Almost all the benchmarks can be proved for the first time by the term rewriting system solely. In particular, FISCHER detects a new flaw in a masked implementation published in EUROCRYPT 2017.

Related papers

• Encrypted system identification as-a-service via reliable encrypted matrix inversion [0.0]
  Encrypted computation opens up promising avenues across a plethora of application domains. In particular, Arithmetic homomorphic encryption is a natural fit for cloud-based computational services. This paper presents an encrypted system identification service enabled by a reliable encrypted solution to at least squares problems.
  arXiv  Detail & Related papers  (2024-10-27T20:00:04Z)
• A General Online Algorithm for Optimizing Complex Performance Metrics [5.726378955570775]
  We introduce and analyze a general online algorithm that can be used in a straightforward way with a variety of complex performance metrics in binary, multi-class, and multi-label classification problems. The algorithm's update and prediction rules are appealingly simple and computationally efficient without the need to store any past data.
  arXiv  Detail & Related papers  (2024-06-20T21:24:47Z)
• On Uncertainty Quantification for Near-Bayes Optimal Algorithms [2.622066970118316]
  We show that it is possible to recover the Bayesian posterior defined by the task distribution, which is unknown but optimal in this setting, by building a martingale posterior using the algorithm. Experiments based on a variety of non-NN and NN algorithms demonstrate the efficacy of our method.
  arXiv  Detail & Related papers  (2024-03-28T12:42:25Z)
• Interpretable Anomaly Detection via Discrete Optimization [1.7150329136228712]
  We propose a framework for learning inherently interpretable anomaly detectors from sequential data. We show that this problem is computationally hard and develop two learning algorithms based on constraint optimization. Using a prototype implementation, we demonstrate that our approach shows promising results in terms of accuracy and F1 score.
  arXiv  Detail & Related papers  (2023-03-24T16:19:15Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  We study a novel attack paradigm, which modifies model parameters in the deployment stage. Considering the effectiveness and stealthiness goals, we provide a general formulation to perform the bit-flip based weight attack. We present two cases of the general formulation with different malicious purposes, i.e., single sample attack (SSA) and triggered samples attack (TSA)
  arXiv  Detail & Related papers  (2022-07-25T03:24:58Z)
• Regret Bounds for Expected Improvement Algorithms in Gaussian Process Bandit Optimization [63.8557841188626]
  The expected improvement (EI) algorithm is one of the most popular strategies for optimization under uncertainty. We propose a variant of EI with a standard incumbent defined via the GP predictive mean. We show that our algorithm converges, and achieves a cumulative regret bound of $mathcal O(gamma_TsqrtT)$.
  arXiv  Detail & Related papers  (2022-03-15T13:17:53Z)
• Meta-Regularization: An Approach to Adaptive Choice of the Learning Rate in Gradient Descent [20.47598828422897]
  We propose textit-Meta-Regularization, a novel approach for the adaptive choice of the learning rate in first-order descent methods. Our approach modifies the objective function by adding a regularization term, and casts the joint process parameters.
  arXiv  Detail & Related papers  (2021-04-12T13:13:34Z)
• MixNet for Generalized Face Presentation Attack Detection [63.35297510471997]
  We have proposed a deep learning-based network termed as textitMixNet to detect presentation attacks. The proposed algorithm utilizes state-of-the-art convolutional neural network architectures and learns the feature mapping for each attack category.
  arXiv  Detail & Related papers  (2020-10-25T23:01:13Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Bayesian Optimization with Machine Learning Algorithms Towards Anomaly Detection [66.05992706105224]
  In this paper, an effective anomaly detection framework is proposed utilizing Bayesian Optimization technique. The performance of the considered algorithms is evaluated using the ISCX 2012 dataset. Experimental results show the effectiveness of the proposed framework in term of accuracy rate, precision, low-false alarm rate, and recall.
  arXiv  Detail & Related papers  (2020-08-05T19:29:35Z)
• Accelerated Message Passing for Entropy-Regularized MAP Inference [89.15658822319928]
  Maximum a posteriori (MAP) inference in discrete-valued random fields is a fundamental problem in machine learning. Due to the difficulty of this problem, linear programming (LP) relaxations are commonly used to derive specialized message passing algorithms. We present randomized methods for accelerating these algorithms by leveraging techniques that underlie classical accelerated gradient.
  arXiv  Detail & Related papers  (2020-07-01T18:43:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.