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
• Authors: Étienne André, Engel Lefaucheux, Dylan Marinho,
• 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

• 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.