Expiring opacity problems in parametric timed automata

• URL: http://arxiv.org/abs/2403.07647v1
• Date: Tue, 12 Mar 2024 13:30:53 GMT
• Title: Expiring opacity problems in parametric timed automata
• Abstract summary: We study expiring timed opacity problems in timed automata. We consider the set of time bounds for which a system is opaque and show when they can be effectively computed for timed automata.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Information leakage can have dramatic consequences on the security of real-time systems. Timing leaks occur when an attacker is able to infer private behavior depending on timing information. In this work, we propose a definition of expiring timed opacity w.r.t. execution time, where a system is opaque whenever the attacker is unable to deduce the reachability of some private state solely based on the execution time; in addition, the secrecy is violated only when the private state was entered "recently", i.e., within a given time bound (or expiration date) prior to system completion. This has an interesting parallel with concrete applications, notably cache deducibility: it may be useless for the attacker to know the cache content too late after its observance. We study here expiring timed opacity problems in timed automata. We consider the set of time bounds (or expiration dates) for which a system is opaque and show when they can be effectively computed for timed automata. We then study the decidability of several parameterized problems, when not only the bounds, but also some internal timing constants become timing parameters of unknown constant values.

Related papers

• The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
  We argue that token commitment can be learned as a reusable trace-state policy.<n>We introduce TraceLock, a lightweight plug-in controller that instantiates this policy for a frozen diffusion language model.
  arXiv  Detail & Related papers  (2026-05-23T18:23:46Z)
• Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
  We consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces.<n>Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations.<n>We present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment offMT.
  arXiv  Detail & Related papers  (2026-05-14T10:23:11Z)
• QUACK! Making the (Rubber) Ducky Talk: A Systematic Study of Keystroke Dynamics for HID Injection Detection [60.105690843777666]
  We show that robust, privacy-preserving detection is achievable using lightweight models operating solely on timing features.<n>Our analysis reveals that attacker sophistication does not monotonically translate into improved evasion.
  arXiv  Detail & Related papers  (2026-04-17T08:53:24Z)
• Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
  Real-time online object tracking in videos constitutes a core task in computer vision.<n>We propose interpreting object tracking as a sequential hypothesis test, wherein evidence for or against tracking failures is gradually accumulated over time.<n>We propose both supervised and unsupervised variants by leveraging either ground-truth or solely internal tracking information.
  arXiv  Detail & Related papers  (2026-02-13T14:57:15Z)
• Opacity problems in multi-energy timed automata [1.4732811715354452]
  We study the verification of opacity problems over systems with observation over both timing and energy information.<n>Despite undecidability of this general formalism, we establish positive results over a number of subclasses.
  arXiv  Detail & Related papers  (2025-12-04T16:15:48Z)
• Auditing Prompt Caching in Language Model APIs [77.02079451561718]
  We investigate the privacy leakage caused by prompt caching in large language models (LLMs) We detect global cache sharing across users in seven API providers, including OpenAI. We find evidence that OpenAI's embedding model is a decoder-only Transformer, which was previously not publicly known.
  arXiv  Detail & Related papers  (2025-02-11T18:58:04Z)
• Exploring Temporally-Aware Features for Point Tracking [58.63091479730935]
  Chrono is a feature backbone specifically designed for point tracking with built-in temporal awareness. Chrono achieves state-of-the-art performance in a refiner-free setting on the TAP-Vid-DAVIS and TAP-Vid-Kinetics datasets.
  arXiv  Detail & Related papers  (2025-01-21T15:39:40Z)
• Execution-time opacity control for timed automata [0.0]
  Timing leaks in timed automata can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. We show that we are able to decide whether a TA can be controlled at runtime to ensure opacity.
  arXiv  Detail & Related papers  (2024-09-16T14:46:52Z)
• A Framework for Differential Privacy Against Timing Attacks [0.0]
  We establish a general framework for ensuring differential privacy in the presence of timing side channels. We define a new notion of timing privacy, which captures programs that remain differentially private to an adversary. We show how our framework can be realized in code through a natural extension of the OpenDP Programming Framework.
  arXiv  Detail & Related papers  (2024-09-09T13:56:04Z)
• The Bright Side of Timed Opacity [0.0]
  We show that opacity can mostly be retrieved, except for one-action TAs and for one-clock TAs with $epsilon$-transitions. We then exhibit a new decidable subclass in which the number of observations made by the attacker is limited.
  arXiv  Detail & Related papers  (2024-08-22T09:17:59Z)
• On the Identification of Temporally Causal Representation with Instantaneous Dependence [50.14432597910128]
  Temporally causal representation learning aims to identify the latent causal process from time series observations. Most methods require the assumption that the latent causal processes do not have instantaneous relations. We propose an textbfIDentification framework for instantanetextbfOus textbfLatent dynamics.
  arXiv  Detail & Related papers  (2024-05-24T08:08:05Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. Checking these process constraints is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. We present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change.
  arXiv  Detail & Related papers  (2023-12-20T13:26:31Z)
• Triad: Trusted Timestamps in Untrusted Environments [0.6937243101289335]
  We introduce Triad, a trusted timestamp dispatcher of time readings. The solution provides trusted timestamps enforced by mutually supportive enclave-based clock servers. We leverage enclave properties such as forced exits and CPU-based counters to mitigate attacks on the server's timestamp counters.
  arXiv  Detail & Related papers  (2023-11-10T16:22:08Z)
• Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata [2.2003515924552044]
  Timed automata are an extension of finite-state automata with a set of clocks evolving linearly. We use timed automata as the input formalism, in which we assume that the attacker has access only to the system execution time.
  arXiv  Detail & Related papers  (2023-10-31T12:10:35Z)
• CenTime: Event-Conditional Modelling of Censoring in Survival Analysis [49.44664144472712]
  We introduce CenTime, a novel approach to survival analysis that directly estimates the time to event. Our method features an innovative event-conditional censoring mechanism that performs robustly even when uncensored data is scarce. Our results indicate that CenTime offers state-of-the-art performance in predicting time-to-death while maintaining comparable ranking performance.
  arXiv  Detail & Related papers  (2023-09-07T17:07:33Z)
• The Adversarial Implications of Variable-Time Inference [47.44631666803983]
  We present an approach that exploits a novel side channel in which the adversary simply measures the execution time of the algorithm used to post-process the predictions of the ML model under attack. We investigate leakage from the non-maximum suppression (NMS) algorithm, which plays a crucial role in the operation of object detectors. We demonstrate attacks against the YOLOv3 detector, leveraging the timing leakage to successfully evade object detection using adversarial examples, and perform dataset inference.
  arXiv  Detail & Related papers  (2023-09-05T11:53:17Z)
• Neural Laplace Control for Continuous-time Delayed Systems [76.81202657759222]
  We propose a continuous-time model-based offline RL method that combines a Neural Laplace dynamics model with a model predictive control (MPC) planner. We show experimentally on continuous-time delayed environments it is able to achieve near expert policy performance.
  arXiv  Detail & Related papers  (2023-02-24T12:40:28Z)
• Time-varying Gaussian Process Bandit Optimization with Non-constant Evaluation Time [93.6788993843846]
  We propose a novel time-varying Bayesian optimization algorithm that can effectively handle the non-constant evaluation time. Our bound elucidates that a pattern of the evaluation time sequence can hugely affect the difficulty of the problem.
  arXiv  Detail & Related papers  (2020-03-10T13:28:33Z)

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.