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
• Authors: Garrett Gu, Hovav Shacham,
• 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

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