aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification

• URL: http://arxiv.org/abs/2512.07520v1
• Date: Mon, 08 Dec 2025 12:58:35 GMT
• Title: aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification
• Authors: Noé Amiot, Quentin L. Meunier, Karine Heydemann, Emmanuelle Encrenaz,
• Abstract summary: We present aLEAKator, an open-source framework for the automated formal verification of cryptographic accelerators and software running on CPUs.<n>Our method introduces mixed-domain simulation, enabling precise modeling and verification under various (including robust and relaxed) 1-probing leakage models.<n>Our approach is validated against existing tools and real-world measurements while providing innovative results such as the verification of a full, first-order masked AES on various CPUs.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying the security of masked hardware and software implementations, under advanced leakage models, remains a significant challenge, especially then accounting for glitches, transitions and CPU micro-architectural specifics. Existing verification approaches are either restricted to small hardware gadgets, small programs on CPUs such as Sboxes, limited leakage models, or require hardware-specific prior knowledge. In this work, we present aLEAKator, an open-source framework for the automated formal verification of masked cryptographic accelerators and software running on CPUs from their HDL descriptions. Our method introduces mixed-domain simulation, enabling precise modeling and verification under various (including robust and relaxed) 1-probing leakage models, and supports variable signal granularity without being restricted to 1-bit wires. aLEAKator also supports verification in the presence of lookup tables, and does not require prior knowledge of the target CPU architecture. Our approach is validated against existing tools and real-world measurements while providing innovative results such as the verification of a full, first-order masked AES on various CPUs

Related papers

• From Bits to Chips: An LLM-based Hardware-Aware Quantization Agent for Streamlined Deployment of LLMs [43.33830246397275]
  We introduce the Hardware-Aware Quantization Agent (HAQA) to streamline the quantization and deployment process.<n>Results demonstrate up to a 2.3x speedup in inference, along with increased throughput and improved accuracy.
  arXiv  Detail & Related papers  (2026-01-07T00:39:09Z)
• UnicEdit-10M: A Dataset and Benchmark Breaking the Scale-Quality Barrier via Unified Verification for Reasoning-Enriched Edits [43.59555184340113]
  We introduce a lightweight data pipeline that replaces multi-toolchains with an end-to-end model and a unified post-verification stage.<n>For scalable quality control, we train a 7B dual-task expert model, textbfQwen-Verify, for efficient failure detection and instruction recaptioning.<n>This pipeline yields textbfUnicEdit-10M, a 10M-scale dataset spanning diverse basic and complex editing tasks.
  arXiv  Detail & Related papers  (2025-12-01T17:45:44Z)
• AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
  Assurance for artificial intelligence (AI) systems remains fragmented across software supply-chain security, adversarial machine learning, and governance documentation.<n>This paper introduces the AI Risk Scanning (AIRS) Framework, a threat-model-based, evidence-generating framework designed to operationalize AI assurance.
  arXiv  Detail & Related papers  (2025-11-16T16:10:38Z)
• Quant-dLLM: Post-Training Extreme Low-Bit Quantization for Diffusion Large Language Models [47.41616630151171]
  Diffusion large language models (dLLMs) offer bidirectional context and flexible masked-denoising generation.<n>We propose Quant-dLLM, an ultra-lowbit PTQ framework tailored to dLLMs.<n> Quant-dLLM consistently achieves higher accuracy than state-of-the-art (SOTA) AR-transfer PTQ methods on dLLMs.
  arXiv  Detail & Related papers  (2025-09-27T13:50:42Z)
• Detecting Hardware Trojans in Microprocessors via Hardware Error Correction Code-based Modules [49.1574468325115]
  Hardware Trojans (HTs) enable attackers to execute unauthorized software or gain illicit access to privileged operations.<n>This manuscript introduces a hardware-based methodology for detecting runtime HT activations using Error Correction Codes (ECCs) on a RISC-V microprocessor.
  arXiv  Detail & Related papers  (2025-06-18T12:37:14Z)
• CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
  Fault injection attacks pose significant security threats to embedded systems.<n>Early detection and understanding of how physical faults propagate to system-level behavior are essential to safeguarding cyberinfrastructure.<n>This work introduces CRAFT, a framework that combines pre-silicon analysis with post-silicon validation to systematically uncover and analyze fault injection vulnerabilities.
  arXiv  Detail & Related papers  (2025-03-05T20:17:46Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• A Lean Transformer Model for Dynamic Malware Analysis and Detection [0.0]
  Malware is a fast-growing threat to the modern computing world and existing lines of defense are not efficient enough to address this issue. Previous works have shown some success leveraging Neural Networks and API calls sequences extracted from execution reports. In this paper, we design an emulation-Only model, based on the Transformers architecture, to detect malicious files.
  arXiv  Detail & Related papers  (2024-08-05T08:46:46Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  Hardware-firmware co-verification is critical to design trustworthy systems. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification.
  arXiv  Detail & Related papers  (2023-09-14T19:24:57Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
  arXiv  Detail & Related papers  (2023-08-15T13:19:17Z)
• AWQ: Activation-aware Weight Quantization for LLM Compression and Acceleration [54.692405042065815]
  We propose Activation-aware Weight Quantization (AWQ), a hardware-friendly approach for LLM low-bit weight-only quantization. AWQ protects only 1% salient weights and achieves excellent quantization performance for instruction-tuned LMs and, for the first time, multi-modal LMs. We also implement TinyChat, an efficient and flexible inference framework tailored for 4-bit on-device LLM/VLMs.
  arXiv  Detail & Related papers  (2023-06-01T17:59:10Z)
• DeepGEMM: Accelerated Ultra Low-Precision Inference on CPU Architectures using Lookup Tables [49.965024476651706]
  DeepGEMM is a lookup table based approach for the execution of ultra low-precision convolutional neural networks on SIMD hardware. Our implementation outperforms corresponding 8-bit integer kernels by up to 1.74x on x86 platforms.
  arXiv  Detail & Related papers  (2023-04-18T15:13:10Z)

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.