Главная Manuals WebAssembly Specification Release 1.1 (Draft 2021-12-18)

Search copyright infringement

Content .. 1 2 ..

WebAssembly Specification Release 1.1 (Draft 2021-12-18) - page 1

Implementation Limitations

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190

Validation Algorithm

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192

Custom Sections

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207

211

ii

CHAPTER

1

Introduction

1.1 Introduction

WebAssembly (abbreviated Wasm

) is a

safe, portable, low-level code format

designed for efficient execution and

compact representation. Its main goal is to enable high performance applications on the Web, but it does not make

any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as

well.
WebAssembly is an open standard developed by a

W3C Community Group

This document describes version 1.1 (Draft 2021-12-18) of the

WebAssembly standard. It is intended that it

will be superseded by new incremental releases with additional features in the future.

1.1.1 Design Goals

The design goals of WebAssembly are the following:

• Fast, safe, and portable

semantics

:

– Fast

: executes with near native code performance, taking advantage of capabilities common to all

contemporary hardware.

– Safe

: code is validated and executes in a memory-safe

, sandboxed environment preventing data cor-

ruption or security breaches.

– Well-defined

: fully and precisely defines valid programs and their behavior in a way that is easy to

reason about informally and formally.

– Hardware-independent

: can be compiled on all modern architectures, desktop or mobile devices and

embedded systems alike.

– Language-independent

: does not privilege any particular language, programming model, or object

model.

– Platform-independent

: can be embedded in browsers, run as a stand-alone VM, or integrated in other

environments.

2

A contraction of “WebAssembly”, not an acronym, hence not using all-caps.

1

https://www.w3.org/community/webassembly/

3

No program can break WebAssembly’s memory model. Of course, it cannot guarantee that an unsafe language compiling to WebAssembly

does not corrupt its own memory layout, e.g. inside WebAssembly’s linear memory.

1

– Open

: programs can interoperate with their environment in a simple and universal manner.

• Efficient and portable

representation

:

– Compact

: has a binary format that is fast to transmit by being smaller than typical text or native code

formats.

– Modular

: programs can be split up in smaller parts that can be transmitted, cached, and consumed

separately.

– Efficient

: can be decoded, validated, and compiled in a fast single pass, equally with either just-in-time

(JIT) or ahead-of-time (AOT) compilation.

– Streamable

: allows decoding, validation, and compilation to begin as soon as possible, before all data

has been seen.

– Parallelizable

: allows decoding, validation, and compilation to be split into many independent parallel

tasks.

– Portable

: makes no architectural assumptions that are not broadly supported across modern hardware.

WebAssembly code is also intended to be easy to inspect and debug, especially in environments like web browsers,

but such features are beyond the scope of this specification.

1.1.2 Scope

At its core, WebAssembly is a

virtual instruction set architecture (virtual ISA)

. As such, it has many use cases

and can be embedded in many different environments. To encompass their variety and enable maximum reuse, the

WebAssembly specification is split and layered into several documents.
This document is concerned with the core ISA layer of WebAssembly. It defines the instruction set, binary en-

coding, validation, and execution semantics, as well as a textual representation. It does not, however, define how

WebAssembly programs can interact with a specific environment they execute in, nor how they are invoked from

such an environment.
Instead, this specification is complemented by additional documents defining interfaces to specific embedding

environments such as the Web. These will each define a WebAssembly

application programming interface (API)

suitable for a given environment.

1.1.3 Security Considerations

WebAssembly provides no ambient access to the computing environment in which code is executed. Any inter-

action with the environment, such as I/O, access to resources, or operating system calls, can only be performed

by invoking

provided by the

and imported into a WebAssembly

. An embedder can

establish security policies suitable for a respective environment by controlling or limiting which functional capa-

bilities it makes available for import. Such considerations are an embedder’s responsibility and the subject of

for a specific environment.

Because WebAssembly is designed to be translated into machine code running directly on the host’s hardware, it

is potentially vulnerable to side channel attacks on the hardware level. In environments where this is a concern, an

embedder may have to put suitable mitigations into place to isolate WebAssembly computations.

2

Chapter 1. Introduction

Function Names

The

function name subsection

has the id 1. It consists of a

assigning function names to

function indices

::=

Local Names

The

local name subsection

has the id 2. It consists of an

indirect name map

assigning local names to

local indices

grouped by

function indices

localnamesubsec

::=

indirectnamemap

7.5 Soundness

The

of WebAssembly is

sound

, implying both

type safety

and

memory safety

with respect to the We-

bAssembly semantics. For example:

• All types declared and derived during validation are respected at run time; e.g., every

or

variable

will only contain type-correct values, every

will only be applied to operands of the expected type,

and every

function invocation

always evaluates to a result of the right type (if it does not

or diverge).

• No memory location will be read or written except those explicitly defined by the program, i.e., as a

, a

, an element in a

, or a location within a linear

• There is no undefined behavior, i.e., the

execution rules

cover all possible cases that can occur in a

program, and the rules are mutually consistent.

Soundness also is instrumental in ensuring additional properties, most notably,

encapsulation

of function and

module scopes: no

can be accessed outside their own function and no

components can be accessed

outside their own module unless they are explicitly

or

The typing rules defining WebAssembly

only cover the

static

components of a WebAssembly program.

In order to state and prove soundness precisely, the typing rules must be extended to the

dynamic

components of

the abstract

, that is, the

configurations

, and

administrative instructions

7.5.1 Results

can be classified by

as follows.

Results

• For each

in

:

–

The value

is

with some

𝑡

𝑖

.

• Let

𝑡

*

be the concatenation of all

𝑡

𝑖

.

• Then the result is valid with

[

𝑡

*

]

.

(

𝑆

:

𝑡

)

*

: [

𝑡

*

]

50

The formalization and theorems are derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan

Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman.

Bringing the Web up to Speed with WebAssembly

. Proceedings of the

38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.

51

https://dl.acm.org/citation.cfm?doid=3062341.3062363

198

Chapter 7. Appendix

Results

• The result is valid with

[

𝑡

*

]

, for any sequence

𝑡

*

of

: [

𝑡

*

]

7.5.2 Store Validity

The following typing rules specify when a runtime

𝑆

is

valid

. A valid store must consist of

, and

instances that are themselves valid, relative to

𝑆

.

To that end, each kind of instance is classified by a respective

, or

type. Module

instances are classified by

module contexts

, which are regular

repurposed as module types describing the

defined by a module.

Store

𝑆

• Each

function instance

in

𝑆.

must be

with some

function type

.

• Each

table instance

in

𝑆.

must be

with some

.

• Each

memory instance

in

𝑆.

must be

with some

.

• Each

global instance

in

𝑆.

must be

with some

.

• Each

element instance

in

𝑆.

must be

• Each

data instance

in

𝑆.

must be

• Then the store is valid.

(

*

(

*

(

*

(

*

(

ok

)

*

(

ok

)

*

𝑆

=

}

𝑆

ok

Function Instances

• The

function type

must be

• The

module instance

must be

with some

𝐶

.

• Under

𝐶

, the

must be

with

function type

• Then the function instance is valid with

function type

ok

:

𝐶

Host Function Instances

hf

}

• The

function type

must be

• Let

[

𝑡

*

1

[

𝑡

*

2

]

be the

function type

• For every

𝑆

1

𝑆

and every sequence

of

whose

coincide with

𝑡

*

1

:

–

hf

in store

𝑆

1

with arguments

has a non-empty set of possible outcomes.

–

For every element

𝑅

of this set:

∗ Either

𝑅

must be

⊥

(i.e., divergence).

∗ Or

𝑅

consists of a

𝑆

2

𝑆

1

and a

whose

coincides with

[

𝑡

*

2

]

.

• Then the function instance is valid with

function type

[

𝑡

*

1

[

𝑡

*

2

]

ok

∀

𝑆

1

,

𝑆

1

ok

∧

𝑆

1

∧

𝑆

: [

𝑡

*

1

] =

⇒

hf

(

𝑆

1

)

⊃ ∅ ∧

∀

𝑅

∈

hf

(

𝑆

1

)

, 𝑅

=

⊥ ∨

∃

𝑆

2

𝑆

2

ok

∧

𝑆

𝑆

2

∧

𝑆

: [

𝑡

*

2

]

∧

𝑅

= (

𝑆

2

[

𝑡

*

1

[

𝑡

*

2

]

hf

}

: [

𝑡

*

1

[

𝑡

*

2

]

Note:

This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing

the host function must satisfy appropriate post-conditions about store and results. The post-conditions match the

ones in the

execution rule

for invoking host functions.

Any store under which the function is invoked is assumed to be an extension of the current store. That way, the

function itself is able to make sufficient assumptions about future stores.

Table Instances

𝑡

)

}

• The

𝑡

must be

• The length of

must equal

• For each

in the table’s elements

:

–

The

must be

with

reference type

𝑡

.

• Then the table instance is valid with

𝑡

.

𝑡

ok

𝑛

(

𝑆

:

𝑡

)

𝑛

𝑡

)

}

𝑡

Memory Instances

𝑏

*

}

• The

𝑚

?

}

must be

• The length of

𝑏

*

must equal

multiplied by the

64 Ki

.

• Then the memory instance is valid with

ok

𝑛

·

64 Ki

𝑏

𝑛

}

Content .. 1 2 ..

///////////////////////////////////////