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

• On Synthesis of Metric Interval Temporal Logics [0.5505634045241289]
  This paper presents the first framework to tackle emphprecise passive learning for an expressive timed logic.<n>Our approach formally reduces the timed learning problem into a scalable untimed one.<n>We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.
  arXiv  Detail & Related papers  (2026-09-01T10:30:46Z)
• Autonomous Cyber Defense: Real-Time Attack Detection and Mitigation in Software-Defined Networks Using Machine Learning [78.29352305480285]
  In recent intrusions, the interval between initial access and the first lateral movement has been observed to be as short as 27 seconds.<n>This paper presents a closed-loop framework that detects and blocks attacks in software-defined networks without operator involvement.
  arXiv  Detail & Related papers  (2026-08-22T18:38:39Z)
• A Self-Triggered Agentic Push Recommendation System [77.13502692161426]
  Push notification is a critical recommendation scenario on large-scale platforms.<n>We propose a proactive, Self-Triggered End-to-end Agentic Push Recommendation System.<n>STEPS is already fully deployed at Douyin with over 1 billion users.
  arXiv  Detail & Related papers  (2026-08-03T09:20:53Z)
• Toward the Right Analytical Model and System Software for Autonomous Driving Systems: Open Problems and Research Directions [0.0]
  This paper surveys the remaining gaps along five dimensions: units of timing constraints, timing metrics, resource models, execution-time variability, and safety integration.<n>This raises a two-sided question: what analytical models are needed to reason about timing in AD systems, and what system software is needed to realize, observe, and enforce those models on real platforms.
  arXiv  Detail & Related papers  (2026-07-05T06:10:47Z)
• 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)
• 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.