Why WebAssembly?
WebAssembly is one of the core technologies that the Dfinity platform is building on.
WebAssembly (or Wasm) is one of the core technologies that the Dfinity platform is building on. In fact, Wasm has become common grounds for a number of projects in the blockchain space and elsewhere.
It also sees increasing interest from the research community. As a result, we were invited to publish an article on Wasm in the Communications of the ACM. We are happy to announce that it just appeared in the latest issue:
If you are looking for comprehensive technical background on Wasm’s goals, design, and semantics, then this article is for you.
So, what is Wasm, and what makes it interesting?
In a nutshell, Wasm is a new code format for deploying programs that is portable, safe, efficient, and universal. That means that it potentially enables software written in arbitrary programming languages to run safely and fast on arbitrary hardware — think of Wasm as an intermediary language between the developer’s programming language of choice and the user’s hardware.
As an industrial technology, Wasm is quite remarkable for at least two reasons:
- It has been designed and implemented in collaboration between all major competitors in its space.
- It has been designed and released along with a complete mathematical, machine-verified formalisation.
To the best of our knowledge, Wasm is unprecedented as a major programming (let alone Web) technology on both these accounts.
An Open Technology
Wasm has originally been designed in 2015–2016 by teams from the four major browser vendors (Google, Mozilla, Apple, Microsoft — I was one of the Googlers at the time). The original elevator pitch was to bring near-native machine performance to the Web and liberate it from the stranglehold that JavaScript has over the Web. Those obviously are important (and overdue) goals. However, we wanted to go further than that:
- We wanted to create a technology that is useful beyond “only” the Web. Despite its name (which is really a misnomer), WebAssembly is in fact carefully designed to be completely agnostic to the Web; at its core, it simply is a cross-platform low-level virtual machine that can equally be “embedded” into any other environment. Wasm also is completely neutral towards the programming model used to express programs — it is an abstraction over common hardware, not over a programming language or paradigm.
- We wanted to keep the design process open to the public and avoid any sort of licensing, copyrighting, or patenting nonsense from interfering with the use of the technology. As a result, Wasm is defined by an open standard: anybody can freely use it, implement it, or contribute to it. Moreover, all major implementations are open source.
Both these goals are in sharp contrast to other technologies that have dominated the market of virtual machines so far. They make Wasm viable both technically and legally for a broad range of applications. Consequently, it didn’t take long before Wasm was picked up in a number of domains: cloud computing as e.g. provided by Dfinity, content delivery networks, mobile platforms, embedded systems, and even as a stand-alone technology on desktop. You name it.
That was what we had hoped for! While use cases outside the Web were a bit hypothetical initially, they have become very real already. Dfinity is at the forefront of this development — we contribute significantly to the further development of the standard, champion various proposals, and collaborate with research groups for advancing its foundations.
A Formal Semantics
The industry’s approach to defining programming languages and related technologies basically hasn’t progressed in 50 years: produce a bit of grammar to define syntax and then pages over pages of clumsy prose to explain what it is supposed to mean. That is complemented with a lot of wishful thinking that it all makes sense, is complete, consistent, and has the properties you think it has. Of course, in practice, it usually isn’t and hasn’t: language definitions have gaping holes, inaccuracies and outright bugs, and consequently, implementations accidentally allow unsafe programs and are not fully compatible with one another, leading to bugs, crashes, vulnerabilities, etc.
Honestly, with languages being the foundation of all software, this situation is embarrassing and dangerous. And it doesn’t need to be like that! Over the past 4 decades, the research community has established well-understood methods for making the definition of programming languages mathematically precise, concise, and eligible to formal reasoning about their correctness and behaviour.
With Wasm, we managed to make the leap. Wasm has been designed and standardised with a complete formal semantics using state-of-the-art methodology that makes precise every detail of its definition. In addition, we formally proved that this semantics is sound, i.e., that it has certain basic safety properties and that there is no undefined behaviour leaving room for incompatibilities or exploits. The tight feedback loop between design and formalisation also led to a significantly simpler and cleaner semantics.
And not just that: this semantics and the accompanying proofs have been machine-verified using state-of-the-art theorem provers. We don’t just assume, we know it is correct.
This opens up interesting possibilities. For example, one can now build certified compilers for high-level programming languages that translate to Wasm. Such a translation then provably maintains the semantics of the original program, if defined. Symmetrically, a certified implementation of Wasm could be proved correct relative to a given hardware architecture and its formalisation. Together, this provides the possibility of specification and certification in depth. A well-defined semantics also enables rigorous reasoning about (and testing of) programs distributed in Wasm. For example, we can build tools enriching the semantics to check for information leaks.
For a platform like Dfinity, which strives to support high assurance applications from areas like finance or accounting, such a level of precision and rigour of course is highly desirable. Hence, Wasm was a natural choice for Dfinity as well as other blockchain projects.
The Future
Wasm, as currently released, is merely a first step. There is a longer road map for making it a richer platform. Wasm’s initial release was consciously limited in scope to supporting applications written in low-level programming languages like C++ or Rust well. In the Wasm group, we are now working on a stream of proposals for extending efficient support to more high-level languages. Dfinity is both a contributor to and an early adopter of some of these proposals.
Stay tuned.
PS: In case you wondered, yes, “Wasm” (not “WASM”) is the official spelling — it is a contraction, not an acronym.
