Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond

• URL: http://arxiv.org/abs/2311.14246v1
• Date: Fri, 24 Nov 2023 01:38:19 GMT
• Title: Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond
• Abstract summary: 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.
• Score: 2.803675461772196
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We claim that existing techniques and tools for generating and verifying constant-time code are incomplete, since they rely on assumptions that compiler optimization passes do not break constant-timeness or that certain operations execute in constant time on the hardware. We present the first end-to-end constant-time-aware compilation process that preserves constant-time semantics at every step from a high-level language down to microarchitectural guarantees, provided by the forthcoming ARM PSTATE.DIT feature. First, we present a new compiler-verifier suite based on the JIT-style runtime Wasmtime, modified to compile ct-wasm, a preexisting type-safe constant-time extension of WebAssembly, into ARM machine code while maintaining the constant-time property throughout all optimization passes. The resulting machine code is then fed into an automated verifier that requires no human intervention and uses static dataflow analysis in Ghidra to check the constant-timeness of the output. Our verifier leverages characteristics unique to ct-wasm-generated code in order to speed up verification while preserving both soundness and wide applicability. We also consider the resistance of our compilation and verification against speculative timing leakages such as Spectre. Finally, in order to expose ct-Wasmtime at a high level, we present a port of FaCT, a preexisting constant-time-aware DSL, to target ct-wasm.

Related papers

• FutureRTC: Real-Time Robot Execution with Anticipatory-Conditioned Action Chunking [51.97839311685636]
  FutureRTC is a plug-and-play adaptation framework that predicts execution-time observations and states for asynchronous VLA control without modifying the underlying policy.<n>We show that FutureRTC achieves robustness to inference delays, resulting in smoother trajectories, faster execution, and consistently higher task success rates.
  arXiv  Detail & Related papers  (2026-07-27T05:10:16Z)
• DISARM: Target Electronic Device Informed Mitigation of Software Runtime Side-Channel Vulnerabilities [2.537406035246369]
  Program runtime or timing attacks exploit variations in a program's execution times to extract sensitive information.<n>We propose DISARM, a joint hardware-software methodology for mitigating runtime side-channel vulnerabilities.<n>We implement DISARM to support C, C++, and Java source codes and validate it across 22 standard benchmarks.
  arXiv  Detail & Related papers  (2026-06-18T05:22:38Z)
• Harnessing Generalist Agents for Contextualized Time Series [67.28481985993467]
  Time series are often embedded in rich contexts that are essential for holistic modeling.<n>In this work, we introduce TimeClaw, an agentic harness framework for time series.<n>TimeClaw integrates executable temporal tools for grounded and auditable analysis, experience-driven capability evolution for creating reusable analytical routines, and episodic multimodal memory for retrieving relevant reasoning traces.
  arXiv  Detail & Related papers  (2026-06-03T20:20:34Z)
• DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification [0.08749675983608168]
  We propose a novel approach for verifying constant-time programs based on dynamic analysis of low-level execution traces.<n>We developed an open-source tool called DALC-CT, for the constant-time verification of programs using this approach.
  arXiv  Detail & Related papers  (2026-04-18T04:47:54Z)
• Tamper-Proofing with Self-Modifying Code [0.0]
  Self-modifying code (SMC) on a deterministic universal Turing machine can be simulated by non-SMC code on the same model.<n>We argue that once timing, ordering, and self-introspective effects are treated as observables, a practically faithful non-SMC reproduction becomes detectably expensive on commodity systems.<n>We present a tamper-proofing model that combines introspective and polymorphic SMC, reliable clocks, and timing predicates to bind runtime checks to execution behavior.
  arXiv  Detail & Related papers  (2026-04-14T07:44:17Z)
• TempoNet: Slack-Quantized Transformer-Guided Reinforcement Scheduler for Adaptive Deadline-Centric Real-Time Dispatchs [8.818252253980985]
  TempoNet is a reinforcement learning scheduler that pairs a permutation-invariant Transformer with a deep Q-approximation.<n>A latency-aware sparse attention stack with blockwise top-k selection and locality-sensitive chunking enables global reasoning over unordered task sets.
  arXiv  Detail & Related papers  (2026-02-20T09:56:23Z)
• MEMTS: Internalizing Domain Knowledge via Parameterized Memory for Retrieval-Free Domain Adaptation of Time Series Foundation Models [51.506429027626005]
  Memory for Time Series (MEMTS) is a lightweight and plug-and-play method for retrieval-free domain adaptation in time series forecasting.<n>Key component of MEMTS is a Knowledge Persistence Module (KPM), which internalizes domain-specific temporal dynamics.<n>This paradigm shift enables MEMTS to achieve accurate domain adaptation with constant-time inference and near-zero latency.
  arXiv  Detail & Related papers  (2026-02-14T14:00:06Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• Timely Machine: Awareness of Time Makes Test-Time Scaling Agentic [72.97800570813175]
  We propose Timely Machine, redefining test-time as wall-clock time.<n>We introduce Timely-Eval, a benchmark spanning high-frequency tool calls, low-frequency tool calls, and time-constrained reasoning.<n>We find smaller models excel with fast feedback through more interactions, while larger models dominate high-latency settings via superior interaction quality.
  arXiv  Detail & Related papers  (2026-01-23T06:28:52Z)
• 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)
• Context-Guided Decompilation: A Step Towards Re-executability [50.71992919223209]
  Binary decompilation plays an important role in software security analysis, reverse engineering and malware understanding.<n>Recent advances in large language models (LLMs) have enabled neural decompilation, but the generated code is typically only semantically plausible.<n>We propose ICL4Decomp, a hybrid decompilation framework that leverages in-context learning (ICL) to guide LLMs toward generating re-executable source code.
  arXiv  Detail & Related papers  (2025-11-03T17:21:39Z)
• Fast and Compact Tsetlin Machine Inference on CPUs Using Instruction-Level Optimization [0.4499833362998488]
  The Tsetlin Machine (TM) offers high-speed inference on resource-constrained devices such as CPUs.<n>We propose an efficient software implementation of the TM by leveraging instruction-level bitwise operations.<n>We introduce an early exit mechanism, which exploits the TM's AND-based clause evaluation to avoid unnecessary computations.
  arXiv  Detail & Related papers  (2025-10-17T13:44:20Z)
• Fun with flags: How Compilers Break and Fix Constant-Time Code [0.0]
  We analyze how compiler optimizations break constant-time code.<n>Key insight is that a small set of passes are at the root of most leaks.<n>We propose an original and practical mitigation that requires no source code modification or custom compiler.
  arXiv  Detail & Related papers  (2025-07-08T15:52:17Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Towards Stabilized and Efficient Diffusion Transformers through Long-Skip-Connections with Spectral Constraints [51.83081671798784]
  Diffusion Transformers (DiT) have emerged as a powerful architecture for image and video generation, offering superior quality and scalability.<n>DiT's practical application suffers from inherent dynamic feature instability, leading to error amplification during cached inference.<n>We propose Skip-DiT, an image and video generative DiT variant enhanced with Long-Skip-Connections (LSCs) - the key efficiency component in U-Nets.
  arXiv  Detail & Related papers  (2024-11-26T17:28:10Z)
• Timer-XL: Long-Context Transformers for Unified Time Series Forecasting [67.83502953961505]
  We present Timer-XL, a causal Transformer for unified time series forecasting. Based on large-scale pre-training, Timer-XL achieves state-of-the-art zero-shot performance.
  arXiv  Detail & Related papers  (2024-10-07T07:27:39Z)
• Temporal Feature Matters: A Framework for Diffusion Model Quantization [105.3033493564844]
  Diffusion models rely on the time-step for the multi-round denoising. We introduce a novel quantization framework that includes three strategies. This framework preserves most of the temporal information and ensures high-quality end-to-end generation.
  arXiv  Detail & Related papers  (2024-07-28T17:46:15Z)
• Sparser is Faster and Less is More: Efficient Sparse Attention for Long-Range Transformers [58.5711048151424]
  We introduce SPARSEK Attention, a novel sparse attention mechanism designed to overcome computational and memory obstacles. Our approach integrates a scoring network and a differentiable top-k mask operator, SPARSEK, to select a constant number of KV pairs for each query. Experimental results reveal that SPARSEK Attention outperforms previous sparse attention methods.
  arXiv  Detail & Related papers  (2024-06-24T15:55:59Z)
• Towards Efficient Verification of Constant-Time Cryptographic Implementations [5.433710892250037]
  Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks. We put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Our approach is implemented as a cross-platform and fully automated tool CT-Prover.
  arXiv  Detail & Related papers  (2024-02-21T03:39:14Z)
• 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)
• DECLASSIFLOW: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security Measures (Full Version) [9.816078445230305]
  Speculative execution attacks undermine the security of constant-time programming. This paper proposes DECLASSIFLOW to efficiently protect constant-time code from speculative leakage.
  arXiv  Detail & Related papers  (2023-12-14T21:00:20Z)
• 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)
• Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
  We introduce a novel gated recurrent unit (GRU) with a weighted time-delay feedback mechanism. We show that $tau$-GRU can converge faster and generalize better than state-of-the-art recurrent units and gated recurrent architectures.
  arXiv  Detail & Related papers  (2022-12-01T02:26:34Z)
• Securing Optimized Code Against Power Side Channels [1.589424114251205]
  Security engineers often sacrifice code efficiency by turning off compiler optimization and/or performing local, post-compilation transformations. This paper proposes SecConCG, a constraint-based compiler approach that generates optimized yet secure code.
  arXiv  Detail & Related papers  (2022-07-06T12:06:28Z)
• Distortion-Aware Network Pruning and Feature Reuse for Real-time Video Segmentation [49.17930380106643]
  We propose a novel framework to speed up any architecture with skip-connections for real-time vision tasks. Specifically, at the arrival of each frame, we transform the features from the previous frame to reuse them at specific spatial bins. We then perform partial computation of the backbone network on the regions of the current frame that captures temporal differences between the current and previous frame.
  arXiv  Detail & Related papers  (2022-06-20T07:20:02Z)
• MAPLE-Edge: A Runtime Latency Predictor for Edge Devices [80.01591186546793]
  We propose MAPLE-Edge, an edge device-oriented extension of MAPLE, the state-of-the-art latency predictor for general purpose hardware. Compared to MAPLE, MAPLE-Edge can describe the runtime and target device platform using a much smaller set of CPU performance counters. We also demonstrate that unlike MAPLE which performs best when trained on a pool of devices sharing a common runtime, MAPLE-Edge can effectively generalize across runtimes.
  arXiv  Detail & Related papers  (2022-04-27T14:00:48Z)
• Lightweight Jet Reconstruction and Identification as an Object Detection Task [5.071565475111431]
  We apply convolutional techniques to end-to-end jet identification and reconstruction tasks encountered at the CERN Large Hadron Collider. PFJet-SSD performs simultaneous localization, classification and regression tasks to cluster jets and reconstruct their features. We show that the ternary network closely matches the performance of its full-precision equivalent and outperforms the state-of-the-art rule-based algorithm.
  arXiv  Detail & Related papers  (2022-02-09T15:01:53Z)

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.