PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot

• URL: http://arxiv.org/abs/2209.07936v3
• Date: Mon, 21 Apr 2025 04:17:04 GMT
• Title: PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
• Authors: Zhuoruo Zhang, Rui Chang, Mingshuai Chen, Wenbo Shen, Chenyang Yu, He Huang, Qinming Dai, Yongwang Zhao,
• Abstract summary: Hardware supply-chain attacks can bypass multiprocessor secure boot.<n>We present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems.
• Score: 7.945777469643774
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. This paper identifies a new, prevalent hardware supply-chain attack surface that can bypass multiprocessor secure boot due to the absence of processor-authentication mechanisms. To defend against such attacks, we present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems. PA-Boot is proved functionally correct and is guaranteed to detect multiple adversarial behaviors, e.g., processor replacements, man-in-the-middle attacks, and tampering with certificates. The fine-grained formalization of PA-Boot and its fully mechanized security proofs are carried out in the Isabelle/HOL theorem prover with 306 lemmas/theorems and ~7,100 LoC. Experiments on a proof-of-concept implementation indicate that PA-Boot can effectively identify boot-process attacks with a considerably minor overhead and thereby improve the security of multiprocessor systems.

Related papers

• Peacock: UEFI Firmware Runtime Observability Layer for Detection and Response [21.022582425069675]
  Peacock is a framework that introduces integrity monitoring and remote verification for the boot process.<n>Our evaluation shows that Peacock reliably detects multiple real-world UEFI bootkits, including Glupteba, BlackLotus, LoJax, and MosaicRegressor.
  arXiv  Detail & Related papers  (2026-01-12T10:38:43Z)
• Binding Agent ID: Unleashing the Power of AI Agents with accountability and credibility [46.323590135279126]
  BAID (Binding Agent ID) is a comprehensive identity infrastructure establishing verifiable user-code binding.<n>We implement and evaluate a complete prototype system, demonstrating the practical feasibility of blockchain-based identity management and zkVM-based authentication protocol.
  arXiv  Detail & Related papers  (2025-12-19T13:01:54Z)
• Breaking Precision Time: OS Vulnerability Exploits Against IEEE 1588 [0.0]
  Precision Time Protocol (PTP) underpins critical infrastructure in telecommunications, finance, power systems, and industrial automation.<n>Prior work has extensively analyzed PTP's vulnerability to network-based attacks, prompting the development of cryptographic protections and anomaly detectors.<n>We identify and exploit a critical blind spot in current threat models: kernel-level adversaries operating from within the host running the PTP stack.
  arXiv  Detail & Related papers  (2025-10-07T20:00:42Z)
• Cuckoo Attack: Stealthy and Persistent Attacks Against AI-IDE [64.47951172662745]
  Cuckoo Attack is a novel attack that achieves stealthy and persistent command execution by embedding malicious payloads into configuration files.<n>We formalize our attack paradigm into two stages, including initial infection and persistence.<n>We contribute seven actionable checkpoints for vendors to evaluate their product security.
  arXiv  Detail & Related papers  (2025-09-19T04:10:52Z)
• Design and analysis of a set of discrete variable protocols for secure quantum communication [0.0]
  quantum identity authentication (QIA) protocols have been proposed over the past three decades.<n>This thesis presents two novel QKD protocols that eliminate the need for entanglement or ideal single-photon sources.<n>These protocols are rigorously proven to be secure against various attacks, including intercept-resend and certain collective attacks.
  arXiv  Detail & Related papers  (2025-08-08T15:12:29Z)
• 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)
• Exploiting Inaccurate Branch History in Side-Channel Attacks [54.218160467764086]
  This paper examines how resource sharing and contention affect two widely implemented but underdocumented features: Bias-Free Branch Prediction and Branch History Speculation.<n>We show that these features can inadvertently modify the Branch History Buffer (BHB) update behavior and create new primitives that trigger malicious mis-speculations.<n>We present three novel attack primitives: two Spectre attacks, namely Spectre-BSE and Spectre-BHS, and a cross-privilege control flow side-channel attack called BiasScope.
  arXiv  Detail & Related papers  (2025-06-08T19:46:43Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• SAFE-SiP: Secure Authentication Framework for System-in-Package Using Multi-party Computation [0.0]
  Chiplet-based heterogeneous integration is transforming the semiconductor, AI, and high-performance computing industries.<n>Current solutions often depend on dedicated security chiplets or changes to the timing flow, which assume a trusted SiP integrator.<n>We present SAFE-SiP, a scalable authentication framework that garbles chiplet signatures and uses MPC for verifying integrity.
  arXiv  Detail & Related papers  (2025-05-13T22:36:17Z)
• The Cost of Performance: Breaking ThreadX with Kernel Object Masquerading Attacks [16.54210795506388]
  We show that popular real-time operating systems (RTOSs) lack essential security protections. We identify a performance optimization practice in ThreadX that introduces security vulnerabilities, allowing for the circumvention of parameter sanitization processes. We introduce an automated approach involving under-constrained symbolic execution to identify the Kernel Object Masquerading (KOM) Attack.
  arXiv  Detail & Related papers  (2025-04-28T05:01:35Z)
• MIP against Agent: Malicious Image Patches Hijacking Multimodal OS Agents [60.92962583528122]
  Recent advances in operating system (OS) agents have enabled vision-language models (VLMs) to directly control a user's computer.<n>We uncover a novel attack vector against these OS agents: Malicious Image Patches (MIPs)<n>MIPs adversarially perturbed screen regions that, when captured by an OS agent, induce it to perform harmful actions by exploiting specific APIs.
  arXiv  Detail & Related papers  (2025-03-13T18:59:12Z)
• 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)
• Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  We propose Authenticated Cyclic Redundancy Integrity Check (ACRIC) ACRIC preserves backward compatibility without requiring additional hardware and is protocol agnostic. We show that ACRIC offers robust security with minimal transmission overhead ( 1 ms)
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• A Scheduling-Aware Defense Against Prefetching-Based Side-Channel Attacks [16.896693436047137]
  Speculative loading of memory, called prefetching, is common in real-world CPUs. Prefetching can be exploited to bypass process isolation and leak secrets, such as keys used in RSA, AES, and ECDH implementations. We implement our countermeasure for an x86_64 and an ARM processor.
  arXiv  Detail & Related papers  (2024-10-01T07:12:23Z)
• PACCOR4ESP: Embedded Device Security Attestation using Platform Attribute Certificates [0.3474871319204387]
  This paper proposes an extension of the NSA Cybersecurity Directorate's Platform Attribute Certificate Creator for the ESP32. The toolkit extracts security-relevant information from an ESP32-S3, such as the firmware hash, and automatically embeds it into a Platform Attribute Certificate.
  arXiv  Detail & Related papers  (2024-07-19T13:17:00Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• ALPC Is In Danger: ALPChecker Detects Spoofing and Blinding [2.5782420501870296]
  This study is to evaluate the possibility of implementing an attack on ALPC connection in the Windows operating system through the kernel. ALPC is used in various Windows information protection systems, including antivirus systems (AV) and Detection and Response systems (EDR)
  arXiv  Detail & Related papers  (2023-12-30T16:58:28Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• A Lightweight and Secure PUF-Based Authentication and Key-exchange Protocol for IoT Devices [0.0]
  Device Authentication and Key exchange are major challenges for the Internet of Things. PUF appears to offer a practical and economical security mechanism in place of typically sophisticated cryptosystems like PKI and IBE. We present a system in which the IoT device does not require a continuous active internet connection to communicate with the server in order to Authenticate itself.
  arXiv  Detail & Related papers  (2023-11-07T15:42:14Z)
• Citadel: Real-World Hardware-Software Contracts for Secure Enclaves Through Microarchitectural Isolation and Controlled Speculation [8.414722884952525]
  Hardware isolation primitives such as secure enclaves aim to protect programs, but remain vulnerable to transient execution attacks. This paper advocates for processors to incorporate microarchitectural isolation primitives and mechanisms for controlled speculation. We introduce two mechanisms to securely share memory between an enclave and an untrusted OS in an out-of-order processor.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)
• Practical quantum secure direct communication with squeezed states [55.41644538483948]
  We report the first table-top experimental demonstration of a CV-QSDC system and assess its security. This realization paves the way into future threat-less quantum metropolitan networks, compatible with coexisting advanced wavelength division multiplexing (WDM) systems.
  arXiv  Detail & Related papers  (2023-06-25T19:23:42Z)
• When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
  We develop two lightweight driver authentication systems based on Random Forest and Recurrent Neural Network architectures. We are the first to propose attacks against these systems by developing two novel evasion attacks, SMARTCAN and GANCAN. Through our contributions, we aid practitioners in safely adopting these systems, help reduce car thefts, and enhance driver security.
  arXiv  Detail & Related papers  (2023-06-09T14:33:26Z)
• Preprocessors Matter! Realistic Decision-Based Attacks on Machine Learning Systems [56.64374584117259]
  Decision-based attacks construct adversarial examples against a machine learning (ML) model by making only hard-label queries. We develop techniques to (i) reverse-engineer the preprocessor and then (ii) use this extracted information to attack the end-to-end system. Our preprocessors extraction method requires only a few hundred queries, and our preprocessor-aware attacks recover the same efficacy as when attacking the model alone.
  arXiv  Detail & Related papers  (2022-10-07T03:10:34Z)

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.