WebAssembly (Wasm) is a novel low-level bytecode format that swiftly gained popularity for its efficiency, versatility and security, with near-native performance. Besides, trusted execution environments (TEEs) shield critical software assets against compromised infrastructures. However, TEEs do not guarantee the code to be trustworthy or that it was not tampered with. Instead, one relies on remote attestation to assess the code before execution. This paper describes WaTZ, which is (i) an efficient and secure runtime for trusted execution of Wasm code for Arm's TrustZone TEE, and (ii) a lightweight remote attestation system optimised for Wasm applications running in TrustZone, as it lacks built-in mechanisms for attestation. The remote attestation protocol is formally verified using a state-of-the-art analyser and model checker. Our extensive evaluation of Arm-based hardware uses synthetic and real-world benchmarks, illustrating typical tasks IoT devices achieve. WaTZ's execution speed is on par with Wasm runtimes in the normal world and reaches roughly half the speed of native execution, which is compensated by the additional security guarantees and the interoperability offered by Wasm. WaTZ is open-source and available on GitHub along with instructions to reproduce our experiments.

翻译：WebAssembly（Wasm）是一种新型低级字节码格式，因其高效性、多功能性、安全性以及接近原生的性能而迅速普及。此外，可信执行环境（TEE）可保护关键软件资产免受受损基础设施的威胁。然而，TEE本身无法保证代码的可信性或未被篡改，而是依赖远程证明机制在执行前评估代码。本文介绍WaTZ，它是一个：（i）为Arm TrustZone TEE设计的高效安全Wasm代码可信运行时环境；（ii）针对TrustZone中Wasm应用优化的轻量级远程证明系统，弥补其缺乏内置证明机制的缺陷。该远程证明协议通过最新分析工具与模型检验器进行形式化验证。我们基于Arm硬件开展了广泛评估，采用合成基准与真实场景基准，涵盖物联网设备的典型任务。WaTZ的执行速度与普通世界中的Wasm运行时相当，可达原生执行速度的一半左右，而Wasm提供的额外安全保证与互操作性可弥补这一性能差异。WaTZ为开源项目，可在GitHub获取，并附有实验复现指南。