Privacy-Preserving Runtime Verification

• URL: http://arxiv.org/abs/2505.09276v1
• Date: Wed, 14 May 2025 10:49:07 GMT
• Title: Privacy-Preserving Runtime Verification
• Authors: Thomas A. Henzinger, Mahyar Karimi, K. S. Thejaswini,
• Abstract summary: We propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications.<n>Our protocols exchange a single message per observation step, after an initialisation phase.<n>We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.
• Score: 6.409194734638881
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification. In this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation. The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.

Related papers

• 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)
• Collaborative Inference over Wireless Channels with Feature Differential Privacy [57.68286389879283]
  Collaborative inference among multiple wireless edge devices has the potential to significantly enhance Artificial Intelligence (AI) applications. transmitting extracted features poses a significant privacy risk, as sensitive personal data can be exposed during the process. We propose a novel privacy-preserving collaborative inference mechanism, wherein each edge device in the network secures the privacy of extracted features before transmitting them to a central server for inference.
  arXiv  Detail & Related papers  (2024-10-25T18:11:02Z)
• Distributed Monitoring of Timed Properties [0.22499166814992436]
  runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. We propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components.
  arXiv  Detail & Related papers  (2024-10-01T07:46:59Z)
• Runtime Verification via Rational Monitor with Imperfect Information [2.7323347531070974]
  Traditional verification assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments. We extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally.
  arXiv  Detail & Related papers  (2024-08-21T13:56:06Z)
• Seagull: Privacy preserving network verification system [0.0]
  This paper introduces a novel approach to verify the correctness of configurations in the internet backbone governed by the BGP protocol. Not only does our proposed solution effectively address scalability concerns, but it also establishes a robust privacy framework.
  arXiv  Detail & Related papers  (2024-02-14T05:56:51Z)
• A Randomized Approach for Tight Privacy Accounting [63.67296945525791]
  We propose a new differential privacy paradigm called estimate-verify-release (EVR) EVR paradigm first estimates the privacy parameter of a mechanism, then verifies whether it meets this guarantee, and finally releases the query output. Our empirical evaluation shows the newly proposed EVR paradigm improves the utility-privacy tradeoff for privacy-preserving machine learning.
  arXiv  Detail & Related papers  (2023-04-17T00:38:01Z)
• Tight Auditing of Differentially Private Machine Learning [77.38590306275877]
  For private machine learning, existing auditing mechanisms are tight. They only give tight estimates under implausible worst-case assumptions. We design an improved auditing scheme that yields tight privacy estimates for natural (not adversarially crafted) datasets.
  arXiv  Detail & Related papers  (2023-02-15T21:40:33Z)
• Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
  This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
  arXiv  Detail & Related papers  (2022-09-28T12:19:13Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• SPAct: Self-supervised Privacy Preservation for Action Recognition [73.79886509500409]
  Existing approaches for mitigating privacy leakage in action recognition require privacy labels along with the action labels from the video dataset. Recent developments of self-supervised learning (SSL) have unleashed the untapped potential of the unlabeled data. We present a novel training framework which removes privacy information from input video in a self-supervised manner without requiring privacy labels.
  arXiv  Detail & Related papers  (2022-03-29T02:56:40Z)
• Confidence Composition for Monitors of Verification Assumptions [3.500426151907193]
  We propose a three-step framework for monitoring the confidence in verification assumptions. In two case studies, we demonstrate that the composed monitors improve over their constituents and successfully predict safety violations.
  arXiv  Detail & Related papers  (2021-11-03T18:14:35Z)
• Towards Partial Monitoring: It is Always too Soon to Give Up [0.0]
  This paper revises the notion of monitorability from a practical perspective. We show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties.
  arXiv  Detail & Related papers  (2021-10-25T01:55:05Z)

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.