本文一篇关于WebAssembly的多语言沙箱的学术论文的翻译，原文参考：

Provably-Safe Multilingual Software Sandboxing using WebAssembly

Provably-Safe Multilingual Software Sandboxing using WebAssembly

使用WebAssembly的可证明安全的多语言软件的沙箱

Abstract

Many applications, from the Web to smart contracts, need to safely execute untrusted code.

许多应用程序，从Web到智能合约(区块链相关)，都需要安全地执行不受信任的代码。

We observe that WebAssembly (Wasm) is ideally positioned to support such applications, since it promises safety and performance, while serving as a compiler target for many high-level languages.

我们发现WebAssembly(Wasm)是一个理想的方向去支持这种应用的运行，这是由于它保证了安全和性能，同时也是一个许多高级语言编译器的编译目标。

However, Wasm’s safety guarantees are only as strong as the implementation that enforces them.

无论如何，Wasm的安全保障[TODO]

Hence, we explore two distinct approaches to producing provably sandboxed Wasm code.

因此，我们探索出两种截然不同的方法得出了可证明沙箱化的wasm代码。

One draws on traditional formal methods to produce mathematical, machine-checked proofs of safety.

一个是利用传统的形式化方法来产生数学上的、经过机器检查的安全性证明。

The second carefully embeds Wasm semantics in safe Rust code such that the Rust compiler can emit safe executable code with good performance.

第二种是在safe rust代码下谨慎地嵌入wasm语义，这样Rust编译器就能够编译出安全的可执行的高性能代码

Our implementation and evaluation of these two techniques indicate that leveraging Wasm gives us provably-safe multilingual sandboxing with performance comparable to standard, unsafe approaches.

我们实现并评估了这两个技术，结果表明，利用wasm带给我们可证明安全的多语言的沙盒，其性能可与标准的，不安全的方法相媲美。

1. Introduction

Lightweight, safe execution of untrusted code is valuable in many contexts, including software plugins, third-party libraries, or even client-side code run when browsing the Web.

轻量的，安全的执行不受信任的代码在许多情形下都是有价值的，包括软件插件，第三方库，或者甚至是浏览Web网页时运行客户端代码。

New contexts such as dynamic content delivery networks (CDNs), edge computing, and smart contracts have created additional motivation to run untrusted code that could potentially harm its execution environment.

现在有这么一种情形，像是动态的内容分发网络(CDNs)，边缘计算与智能合约已经产生了一个额外的动机[TODO]，去运行具有潜在地破坏其执行环境的不受信任的代码。

Software sandboxing (via software fault isolation [41]) is a well-studied technique, with a long and rich history [7, 17, 21, 27, 29, 30, 37, 52], to provide this crucial primitive. Nevertheless, previous effortsto deploy it in production have failed, due to technical and marketplace hurdles (Section 2.2).

<未完待续>