Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata

• URL: http://arxiv.org/abs/2310.20392v1
• Date: Tue, 31 Oct 2023 12:10:35 GMT
• Title: Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
• Authors: \'Etienne Andr\'e (Universit\'e Sorbonne Paris Nord, LIPN, CNRS, Villetaneuse, France), Engel Lefaucheux (Universit\'e de Lorraine, CNRS, Inria, LORIA, Nancy, France), Didier Lime (Nantes Universit\'e, \'Ecole Centrale Nantes, CNRS, LS2N, Nantes, France), Dylan Marinho (Universit\'e de Lorraine, CNRS, Inria, LORIA, Nancy, France), Jun Sun (School of Computing and Information Systems, Singapore Management University, Singapore)
• Abstract summary: 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.
• Score: 2.2003515924552044
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with a set of clocks evolving linearly and that can be tested or reset, making this formalism able to reason on systems involving concurrency and timing constraints. In this paper, we summarize a recent line of works using timed automata as the input formalism, in which we assume that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed system modeled by a timed automaton, given a secret location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the secret location was visited. This means that for any such execution time, the system is opaque: either the final location is not reachable, or it is reachable with that execution time for both a run visiting and a run not visiting the secret location. We also address the full execution-time opacity problem, asking whether the system is opaque for all execution times; we also study a weak counterpart. Second, we add timing parameters, which are a way to configure a system: we identify a subclass of parametric timed automata with some decidability results. In addition, we devise a semi-algorithm for synthesizing timing parameter valuations guaranteeing that the resulting system is opaque. Third, we report on problems when the secret has itself an expiration date, thus defining expiring execution-time opacity problems. We finally show that our method can also apply to program analysis with configurable internal timings.

Related papers

• AdaSpot: Spend Resolution Where It Matters for Precise Event Spotting [59.31340724915079]
  Event Spotting is a key task for applications in sports analytics, robotics, and autonomous systems.<n>bfAdaSpot achieves state-of-the-art performance under strict evaluation metrics.
  arXiv  Detail & Related papers  (2026-02-25T16:24:48Z)
• 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)
• Maxwait: A Generalized Mechanism for Distributed Time-Sensitive Systems [0.45880283710344055]
  maxwait is a simple coordination mechanism with surprising generality.<n>It subsumes classical distributed system methods such as PTIDES, Chandy-and-Misra with or without null messages, Jefferson's Time-Warp, and Lamport's time-based fault detection.<n> maxwait enforces logical-time consistency when communication latencies are bounded and provides structured fault handling when bounds are violated.
  arXiv  Detail & Related papers  (2026-01-29T00:57:25Z)
• Learning to Wait: Synchronizing Agents with the Physical World [16.592968251465475]
  Real-world agentic tasks often involve non-blocking actions with variable latencies, creating a fundamental textitTemporal Gap between action initiation and completion.<n>Existing environment-side solutions, such as blocking wrappers or frequent polling, either limit scalability or dilute the agent's context window with redundant observations.<n>We propose an textbfAgent-side Approach that empowers Large Language Models to actively align their textitCognitive Timeline with the physical world.
  arXiv  Detail & Related papers  (2025-12-18T07:24:44Z)
• 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)
• Code-as-Monitor: Constraint-aware Visual Programming for Reactive and Proactive Robotic Failure Detection [56.66677293607114]
  We propose Code-as-Monitor (CaM) for both open-set reactive and proactive failure detection. To enhance the accuracy and efficiency of monitoring, we introduce constraint elements that abstract constraint-related entities. Experiments show that CaM achieves a 28.7% higher success rate and reduces execution time by 31.8% under severe disturbances.
  arXiv  Detail & Related papers  (2024-12-05T18:58:27Z)
• 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)
• Expiring opacity problems in parametric timed automata [0.0]
  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.
  arXiv  Detail & Related papers  (2024-03-12T13:30:53Z)
• Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
  offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of a global clock. We propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions.
  arXiv  Detail & Related papers  (2024-03-05T16:09:55Z)
• RelayAttention for Efficient Large Language Model Serving with Long System Prompts [59.50256661158862]
  This paper aims to improve the efficiency of LLM services that involve long system prompts. handling these system prompts requires heavily redundant memory accesses in existing causal attention algorithms. We propose RelayAttention, an attention algorithm that allows reading hidden states from DRAM exactly once for a batch of input tokens.
  arXiv  Detail & Related papers  (2024-02-22T18:58:28Z)
• 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)
• Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond [2.803675461772196]
  We present a new compiler-verifier suite based on the JIT-style runtime Wasmtime for generating and verifying constant-time code. We also present a port of FaCT, a preexisting constant-time-aware DSL, to target ct-wasm.
  arXiv  Detail & Related papers  (2023-11-24T01:38:19Z)
• Better than the Best: Gradient-based Improper Reinforcement Learning for Network Scheduling [60.48359567964899]
  We consider the problem of scheduling in constrained queueing networks with a view to minimizing packet delay. We use a policy gradient based reinforcement learning algorithm that produces a scheduler that performs better than the available atomic policies.
  arXiv  Detail & Related papers  (2021-05-01T10:18:34Z)
• A Fast Edge-Based Synchronizer for Tasks in Real-Time Artificial Intelligence Applications [0.8122270502556374]
  Task synchronization across devices is an important problem that affects the timely progress of an AI application. We develop a fast edge-based synchronization scheme that can time align the execution of input-output tasks as well compute tasks.
  arXiv  Detail & Related papers  (2020-12-21T23:02:21Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  We present ISA, an approach for learning and exploiting subgoals in episodic reinforcement learning (RL) tasks. ISA interleaves reinforcement learning with the induction of a subgoal automaton, an automaton whose edges are labeled by the task's subgoals. A subgoal automaton also consists of two special states: a state indicating the successful completion of the task, and a state indicating that the task has finished without succeeding.
  arXiv  Detail & Related papers  (2020-09-08T16:42:55Z)
• Towards Streaming Perception [70.68520310095155]
  We present an approach that coherently integrates latency and accuracy into a single metric for real-time online perception. The key insight behind this metric is to jointly evaluate the output of the entire perception stack at every time instant. We focus on the illustrative tasks of object detection and instance segmentation in urban video streams, and contribute a novel dataset with high-quality and temporally-dense annotations.
  arXiv  Detail & Related papers  (2020-05-21T01:51:35Z)
• 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.