SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

• URL: http://arxiv.org/abs/2409.02918v1
• Date: Wed, 4 Sep 2024 17:54:29 GMT
• Title: SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
• Abstract summary: We instrument the networking and cryptographic library the application uses to obtain a stream of events. We then use an efficient algorithm to match these observations to traces that are valid in the specification model.
• Score: 5.202524136984542
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and cryptographic library the application uses to obtain a stream of events. This is possible even without source code access. We then use an efficient algorithm to match these observations to traces that are valid in the specification model. In contrast to prior work, our algorithm can handle non-determinism and thus, multiple sessions. It also achieves a low overhead, which we demonstrate on the WireGuard reference implementation and a case study from prior work. We find that the reference Tamarin model for WireGuard can be used with little change: We only need to specify wire formats and correct some small inaccuracies that we discovered while conducting the case study. We also provide a soundness result for our algorithm that ensures it accepts only event streams that are valid according to the specification model.

Related papers

• From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp [8.86750495352076]
  We develop a model of WhatsApp Web's implementation of the Signal protocol.<n>For the core components of the Signal protocol, we verify authentication and secrecy properties.<n>Monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork.
  arXiv  Detail & Related papers  (2026-09-10T17:48:49Z)
• AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation [0.0]
  We present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations.<n>We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation.<n>We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol.
  arXiv  Detail & Related papers  (2026-06-18T08:34:17Z)
• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  We introduce textbfCIAware-Bench, a benchmark for measuring textbfcontrol textbfintervention (CI) awareness across frontier models.<n>CIAware-Bench tests whether models can distinguish their own trajectories from those modified by a control intervention.
  arXiv  Detail & Related papers  (2026-06-09T16:24:16Z)
• Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
  We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code.<n>PDD defines a governance model for automated software engineering.
  arXiv  Detail & Related papers  (2026-05-13T04:23:14Z)
• Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
  We present a verification framework and protocol that replaces full proofs with a lightweight, sampling-based approach.<n>We formalize the conditions under which trace separation between functionally dissimilar models can be leveraged to argue the security of verifiable inference protocols.<n>Our approach reduces proving times by several orders of magnitude compared to state-of-the-art cryptographic proof systems.
  arXiv  Detail & Related papers  (2026-03-19T15:24:27Z)
• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  We present IMMACULATE, a practical auditing framework that detects economically motivated deviations.<n>IMMACULATE selectively audits a small fraction of requests using verifiable computation, achieving strong detection guarantees while amortizing cryptographic overhead.
  arXiv  Detail & Related papers  (2026-02-26T07:21:02Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• The Surprising Effectiveness of Membership Inference with Simple N-Gram Coverage [71.8564105095189]
  We introduce N-Gram Coverage Attack, a membership inference attack that relies solely on text outputs from the target model.<n>We first demonstrate on a diverse set of existing benchmarks that N-Gram Coverage Attack outperforms other black-box methods.<n>We find that more recent models, such as GPT-4o, exhibit increased robustness to membership inference.
  arXiv  Detail & Related papers  (2025-08-13T08:35:16Z)
• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  Faults in protocol behavior can lead to vulnerabilities and system failures.<n>A common approach to protocol testing involves constructing Markovian models that capture the state transitions and expected behaviors of the protocol.<n>We propose a novel method that leverages large language models (LLMs) to automatically generate sequences for testing network protocol implementations.
  arXiv  Detail & Related papers  (2025-08-03T13:16:18Z)
• How to Verify that a Small Device is Quantum, Unconditionally [12.663567847694427]
  A proof of quantumness (PoQ) allows a classical verifier to efficiently test if a quantum machine is performing a computation that is infeasible for any classical machine.<n>We propose a new approach for constructing PoQ protocols where soundness holds unconditionally assuming a bound on the memory of the prover.
  arXiv  Detail & Related papers  (2025-05-29T20:09:22Z)
• 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)
• Learning Verifiable Control Policies Using Relaxed Verification [49.81690518952909]
  This work proposes to perform verification throughout training to aim for policies whose properties can be evaluated throughout runtime. The approach is to use differentiable reachability analysis and incorporate new components into the loss function.
  arXiv  Detail & Related papers  (2025-04-23T16:54:35Z)
• PoGO: A Scalable Proof of Useful Work via Quantized Gradient Descent and Merkle Proofs [0.0]
  We present a design called Proof of Gradient Optimization (PoGO) for blockchain consensus. PoGO miners produce verifiable evidence of training large-scale machine-learning models. We provide an empirical cost analysis showing that verification is significantly cheaper than training.
  arXiv  Detail & Related papers  (2025-04-10T08:09:34Z)
• Formal Model Guided Conformance Testing for Blockchains [1.4838910416636741]
  We present a framework that performs protocol conformance testing using a formal model of the protocol. Our framework consists of two complementary components that use the components as trace generators and checkers.
  arXiv  Detail & Related papers  (2025-01-15T03:20:13Z)
• What If We Had Used a Different App? Reliable Counterfactual KPI Analysis in Wireless Systems [52.499838151272016]
  This paper addresses the "what-if" problem of estimating the values of key performance indicators (KPIs) that would have been obtained if a different app had been implemented by the radio access network (RAN) We propose a conformal-prediction-based counterfactual analysis method for wireless systems that provides reliable "error bars" for the estimated, containing the true with a user-defined probability.
  arXiv  Detail & Related papers  (2024-09-30T18:47:26Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  Property-based testing is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC) We devise a test that can detect various flaws in a bit-level implementation of an MPC protocol.
  arXiv  Detail & Related papers  (2024-03-08T02:02:24Z)
• Model Pairing Using Embedding Translation for Backdoor Attack Detection on Open-Set Classification Tasks [63.269788236474234]
  We propose to use model pairs on open-set classification tasks for detecting backdoors. We show that this score, can be an indicator for the presence of a backdoor despite models being of different architectures. This technique allows for the detection of backdoors on models designed for open-set classification tasks, which is little studied in the literature.
  arXiv  Detail & Related papers  (2024-02-28T21:29:16Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  We introduce a novel Unsupervised Continual Anomaly Detection framework called UCAD. The framework equips the UAD with continual learning capability through contrastively-learned prompts. We conduct comprehensive experiments and set the benchmark on unsupervised continual anomaly detection and segmentation.
  arXiv  Detail & Related papers  (2024-01-02T03:37:11Z)
• Publicly-Detectable Watermarking for Language Models [45.32236917886154]
  We present a highly detectable, trustless watermarking scheme for LLMs. The algorithm contains no secret information, and it is executable by anyone. We prove that our scheme is cryptographically correct, sound, and distortion-free.
  arXiv  Detail & Related papers  (2023-10-27T21:08:51Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  We propose a security verification framework for cryptographic protocols using machine learning. We create arbitrarily large datasets by automatically generating random protocols and assigning security labels to them. We evaluate the proposed method by applying it to verification of practical cryptographic protocols.
  arXiv  Detail & Related papers  (2023-04-26T02:37:43Z)
• Robustness of implemented device-independent protocols against constrained leakage [0.0]
  Device-independent (DI) protocols have experienced significant progress in recent years. Security proofs for those demonstrations rely on a typical assumption in DI cryptography, that the devices do not leak any unwanted information to each other or to an adversary.
  arXiv  Detail & Related papers  (2023-02-27T16:28:23Z)
• Black-box Dataset Ownership Verification via Backdoor Watermarking [67.69308278379957]
  We formulate the protection of released datasets as verifying whether they are adopted for training a (suspicious) third-party model. We propose to embed external patterns via backdoor watermarking for the ownership verification to protect them. Specifically, we exploit poison-only backdoor attacks ($e.g.$, BadNets) for dataset watermarking and design a hypothesis-test-guided method for dataset verification.
  arXiv  Detail & Related papers  (2022-08-04T05:32:20Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)
• On the Importance of Encrypting Deep Features [15.340540198612823]
  We analyze model inversion attacks with only two assumptions: feature vectors of user data are known, and a black-box API for inference is provided. Experiments have been conducted on state-of-the-art models in person re-identification, and two attack scenarios (i.e., recognizing auxiliary attributes and reconstructing user data) are investigated. Results show that an adversary could successfully infer sensitive information even under severe constraints.
  arXiv  Detail & Related papers  (2021-08-16T15:22:33Z)
• Pseudo-IoU: Improving Label Assignment in Anchor-Free Object Detection [60.522877583407904]
  Current anchor-free object detectors are quite simple and effective yet lack accurate label assignment methods. We present Pseudo-Intersection-over-Union(Pseudo-IoU): a simple metric that brings more standardized and accurate assignment rule into anchor-free object detection frameworks. Our method achieves comparable performance to other recent state-of-the-art anchor-free methods without bells and whistles.
  arXiv  Detail & Related papers  (2021-04-29T02:48:47Z)

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.