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)是一种新颖的低层次字节格式,因其效率、多功能和安全性而迅速获得流行,具有近亲性性性能。此外,受信任的执行环境(TEEs)保护关键软件资产不受受损基础设施的破坏。然而,TEE并不保证代码可信或没有被篡改。相反,我们依靠远程验证来评估代码执行前的代码。本文描述WaTZ,这是(一)可靠地执行武器信任区TEE的WAM代码的有效和安全运行时间,以及(二)在信任区运行的Wasm应用程序的轻量级远程验证系统,因为它缺乏内在的验证机制。远程验证协议由州级的艺术分析器和模型检查器正式验证。我们对基于武器的硬件使用合成和真实世界基准的广泛评估,说明了IOT设备的典型任务完成。WaTZ的执行速度与正常世界的Wam运行时间相当,并且达到了在信任区运行过程中运行的大约一半的Wam应用程序。 远程验证协议被正式验证,通过附加的安全保障和常规准则来补偿。