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

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