diff --git a/docs/guides/security/data-integrity-and-authenticity.md b/docs/guides/security/data-integrity-and-authenticity.md index a5d08d7..378a3ad 100644 --- a/docs/guides/security/data-integrity-and-authenticity.md +++ b/docs/guides/security/data-integrity-and-authenticity.md @@ -9,14 +9,14 @@ sidebar: ### Security concern -ICP offers three modes of operation for canisters: `update`, `query`, and `composite_query`. For simplicity, this guide treats `composite_query` methods as query methods for the rest of this section. +ICP offers three modes of operation for canisters: `update`, `query`, and `composite_query`. For simplicity, this guide treats `composite_query` methods as query methods for the rest of this section. For more information, view the [detailed overview between update and query calls](../canister-calls/inter-canister-calls.md#query-vs-update-calls). Update calls are slow and expensive but provide integrity guarantees as their responses include a threshold signature signed by the subnet. On the other hand, query calls are fast since a single replica formulates the response, but **there is no integrity guarantee, since the response can be manipulated by a single replica or boundary node.** For example, if the NNS app fetches proposal information from the governance canister via query calls and the responding node is malicious, it can mask an ill-intentioned proposal that causes irrevocable damage as innocuous by modifying the proposal payload in the response and mislead voters into voting yes. Another consequence of query calls is that users can't rely on [canister_inspect_message](../../references/ic-interface-spec/canister-interface.md#system-api-inspect-message) as a guard. **This makes query calls, in their raw form, unfit to serve data for security-critical applications.** ### Using certified variables for secure queries -In certain use cases, there is a third option whereby query results can return data that has been certified by the subnet in an earlier update call. This is the concept of certified data, and it requires changes to the update call to create the certification, the query call to return the certificate, and the frontend to verify the certificate. Using certified data provides query-like response times with update-like certified responses. +In certain use cases, there is a third option whereby query results can return data that has been certified by the subnet in an earlier update call. This is the concept of certified data, and it requires changes to the update call to create the certification, the query call to return the certificate, and the frontend to verify the certificate. Using certified data provides query-like response times with update-like certified responses. This forms the core of [certified variables](../backends/certified-variables.md). Some examples of certified variables are asset certification in [Internet Identity](https://github.com/dfinity/internet-identity/blob/b29a6f68bbe5a49d048e12bc7a3263a9f43d080b/src/internet_identity/src/main.rs#L775-L808), [NNS app](https://github.com/dfinity/nns-dapp/blob/372c3562127d70c2fde059bc9c268e8ae858583e/rs/src/assets.rs#L121-L145), or the [canister signature implementation in Internet Identity](https://github.com/dfinity/ic-canister-sig-creation). diff --git a/docs/guides/security/https-outcalls.md b/docs/guides/security/https-outcalls.md index f3c97fb..238e7a7 100644 --- a/docs/guides/security/https-outcalls.md +++ b/docs/guides/security/https-outcalls.md @@ -70,7 +70,7 @@ See the [HTTPS outcalls guide](../backends/https-outcalls.md) for more details. ### Security concern -The pricing of HTTPS outcalls is determined by the size of the HTTP request and the maximal response size, among other variables. Thus, if big requests are made, this could quickly drain the canister's cycles balance. This can be risky in scenarios where HTTPS outcalls are triggered by user actions (rather than a heartbeat or timer invocation). +The [pricing](../../references/cycles-costs.md#https-outcalls) of HTTPS outcalls is determined by the size of the HTTP request and the maximal response size, among other variables. Thus, if big requests are made, this could quickly drain the canister's cycles balance. This can be risky in scenarios where HTTPS outcalls are triggered by user actions (rather than a heartbeat or timer invocation). ### Recommendation diff --git a/docs/guides/security/identity-and-access-management.mdx b/docs/guides/security/identity-and-access-management.mdx index 517f6e5..c696d87 100644 --- a/docs/guides/security/identity-and-access-management.mdx +++ b/docs/guides/security/identity-and-access-management.mdx @@ -79,7 +79,7 @@ Implementing user authentication and canister calls yourself in your web app is ### Recommendation -- Consider using an identity provider such as [Internet Identity](https://github.com/dfinity/internet-identity) for authentication, and use the ICP JavaScript agent for making canister calls. +- Consider using an identity provider such as [Internet Identity](https://github.com/dfinity/internet-identity) for authentication, and use the [ICP JavaScript agent](../../references/developer-tools.md#javascript--typescript) for making canister calls. - You may consider alternative authentication frameworks on ICP for authentication. @@ -99,7 +99,7 @@ The auth-client supports [idle timeouts](https://js.icp.build/auth/latest/api/cl ### Security concern -`agent.fetchRootKey()` can be used in the ICP JavaScript agent to fetch the root subnet threshold public key from a status call in test environments. This key is used to verify threshold signatures on certified data received through canister update calls. Using this method in a production web app gives an attacker the option to supply their own public key, invalidating all authenticity guarantees of update responses. +`agent.fetchRootKey()` can be used in the [ICP JavaScript agent](../../references/developer-tools.md#javascript--typescript) to fetch the root subnet threshold public key from a status call in test environments. This key is used to verify threshold signatures on certified data received through canister update calls. Using this method in a production web app gives an attacker the option to supply their own public key, invalidating all authenticity guarantees of update responses. ### Recommendation diff --git a/docs/guides/security/inter-canister-calls.md b/docs/guides/security/inter-canister-calls.md index acaeaf9..3322176 100644 --- a/docs/guides/security/inter-canister-calls.md +++ b/docs/guides/security/inter-canister-calls.md @@ -13,7 +13,7 @@ This is also explained in the [community conversation on security best practices ### Security concern -Traps and panics roll back the canister state, as described in [Property 5](../../references/message-execution-properties.md#message-execution-properties). So any state change followed by a trap or panic can be risky. This is an important concern when inter-canister calls are made. If a trap occurs after an await to an inter-canister call, then the state is reverted to the snapshot before the inter-canister call's callback invocation, and not to the state before the entire call. +Traps and panics roll back the canister state, as described in [Property 5](../../references/message-execution-properties.md#property-5). So any state change followed by a trap or panic can be risky. This is an important concern when inter-canister calls are made. If a trap occurs after an await to an inter-canister call, then the state is reverted to the snapshot before the inter-canister call's callback invocation, and not to the state before the entire call. More precisely, suppose some state changes are applied and then an inter-canister call is issued. Also, assume that these state changes leave the canister in an inconsistent state, and that state is only made consistent again in the callback. Now if there is a trap in the callback, this leaves the canister in an inconsistent state. @@ -128,11 +128,11 @@ GoldDAO's GLDT-swap has an implementation of journaling. In their case, the jour ### Security concern -As described in the [properties of message executions on ICP](../../references/message-execution-properties.md), messages (but not entire calls) are processed atomically. In particular, as described in Property 4 in that document, messages from interleaving calls do not have a reliable execution ordering. Thus, the state of the canister (and other canisters) may change between the time an inter-canister call is started and the time when it returns, which may lead to issues if not handled correctly. These issues are generally called 'reentrancy bugs' (see the [Ethereum best practices on reentrancy](https://consensysdiligence.github.io/smart-contract-best-practices/attacks/reentrancy/)). Note, however, that the messaging guarantees, and thus the bugs, on ICP are different from Ethereum. +As described in the [properties of message executions on ICP](../../references/message-execution-properties.md), messages (but not entire calls) are processed atomically. In particular, as described in [Property 4](../../references/message-execution-properties.md#property-4) in that document, messages from interleaving calls do not have a reliable execution ordering. Thus, the state of the canister (and other canisters) may change between the time an inter-canister call is started and the time when it returns, which may lead to issues if not handled correctly. These issues are generally called 'reentrancy bugs' (see the [Ethereum best practices on reentrancy](https://consensysdiligence.github.io/smart-contract-best-practices/attacks/reentrancy/)). Note, however, that the messaging guarantees, and thus the bugs, on ICP are different from Ethereum. Here are two concrete and somewhat similar types of bugs to illustrate potential reentrancy security issues: -- **Time-of-check time-of-use issues:** These occur when some condition on global state is checked before an inter-canister call and then wrongly assuming the condition still holds when the call returns. For example, one might check if there is sufficient balance on some account, then issue an inter-canister call, and finally make a transfer as part of the callback message. When the second inter-canister call starts, it is possible that the condition that was checked initially no longer holds, because other ledger transfers may have happened before the callback of the first call is executed (see also Property 4 above). +- **Time-of-check time-of-use issues:** These occur when some condition on global state is checked before an inter-canister call and then wrongly assuming the condition still holds when the call returns. For example, one might check if there is sufficient balance on some account, then issue an inter-canister call, and finally make a transfer as part of the callback message. When the second inter-canister call starts, it is possible that the condition that was checked initially no longer holds, because other ledger transfers may have happened before the callback of the first call is executed (see also [Property 4](../../references/message-execution-properties.md#property-4)). - **Double-spending issues**: Such issues occur when a transfer is issued twice, often because of unfavorable message scheduling. For example, suppose you check if a caller is eligible for a refund, and if so, transfer some refund amount to them. When the refund ledger call returns successfully, you set a flag in the canister storage indicating that the caller has been refunded. This is vulnerable to double-spending because the refund method can be called twice by the caller in parallel, in which case it is possible that the messages before issuing the transfer (including the eligibility check) are scheduled before both callbacks. A detailed explanation of this issue can be found in the [community conversation on security best practices](https://www.youtube.com/watch?v=PneRzDmf_Xw&list=PLuhDt1vhGcrez-f3I0_hvbwGZHZzkZ7Ng&index=2&t=4s). @@ -294,7 +294,7 @@ Finally, note that the same guard can be used in several methods to restrict par ### Security concern -As stated by the [Property 6](../../references/message-execution-properties.md#message-execution-properties), inter-canister calls can fail in which case they result in a **reject**. See [reject codes](../../references/ic-interface-spec/https-interface.md#reject-codes) for more detail. The caller must correctly deal with the reject cases, as they can happen in normal operation, because of insufficient cycles on the sender or receiver side, or because some data structures like message queues are full. +As stated by the [Property 6](../../references/message-execution-properties.md#property-6), inter-canister calls can fail in which case they result in a **reject**. See [reject codes](../../references/ic-interface-spec/https-interface.md#reject-codes) for more detail. The caller must correctly deal with the reject cases, as they can happen in normal operation, because of insufficient cycles on the sender or receiver side, or because some data structures like message queues are full. 1. The call was issued as a bounded-wait (best-effort response) call, and the system responded with a `SYS_UNKNOWN` reject code. In this case, the caller cannot be a priori sure whether the call took effect or not. 2. The system responded with a `CANISTER_ERROR` reject code. This indicates a bug in the ledger canister. In this case, it is still possible that the call had a partial effect on the ledger canister. diff --git a/docs/guides/security/observability-and-monitoring.md b/docs/guides/security/observability-and-monitoring.md index 436bd37..1119f62 100644 --- a/docs/guides/security/observability-and-monitoring.md +++ b/docs/guides/security/observability-and-monitoring.md @@ -5,18 +5,24 @@ sidebar: order: 9 --- -## Monitor your canister +## Expose metrics from your canister ### Security concern -Without monitoring, it can be hard to detect attacks or vulnerabilities that are being actively exploited. For example, a sudden increase in cycles consumption could indicate a DoS attack, while unexpected changes in canister state could indicate a security breach. +In case of attacks, it is great to be able to obtain relevant metrics from canisters, such as the number of accounts, size of internal data structures, stable memory, etc. ### Recommendation -- Monitor your canister's cycles balance regularly, set up alerts for sudden changes in cycles consumption, and add an endpoint to expose health indicators. See the [DoS prevention best practices](./dos-prevention.md) for more context on cycles monitoring. +[Expose metrics from your canister](https://mmapped.blog/posts/01-effective-rust-canisters.html#expose-metrics) (from [effective Rust canisters](https://mmapped.blog/posts/01-effective-rust-canisters.html)). -- Consider emitting logs for security-relevant events (e.g., access control failures, unexpected state transitions). Since logs are stored in the canister, they provide a tamperproof audit trail. +## Do not publicly reveal a canister's cycles balance -- See [effective Rust canisters](https://mmapped.blog/posts/01-effective-rust-canisters.html) for general patterns on canister observability. +### Security concern + +Publicly revealing the canister's cycles balance allows an attacker to measure the number of instructions spent by executing the canister methods on the attacker's input. Then the attacker might be able to learn which code paths were taken during execution and derive secret information based on that. Moreover, the attacker can learn which methods and their inputs consume a lot of cycles to mount a cycles-draining attack (see also [protect against draining the cycles balance](./dos-prevention.md#handle-expensive-calls)). + +### Recommendation + +Your canisters should not publicly expose their cycles balance (available through the system API), i.e., they should only expose their cycles balance to their controllers or other trusted principals. diff --git a/docs/references/glossary.md b/docs/references/glossary.md index f2d3a99..f7a186d 100644 --- a/docs/references/glossary.md +++ b/docs/references/glossary.md @@ -2,7 +2,7 @@ title: "Glossary" description: "Definitions of ICP-specific terms: canister, cycle, principal, subnet, and more" sidebar: - order: 15 + order: 17 --- # Glossary diff --git a/docs/references/index.md b/docs/references/index.md index b90d56a..8f14cd4 100644 --- a/docs/references/index.md +++ b/docs/references/index.md @@ -33,6 +33,7 @@ Technical reference material for ICP development. These pages cover exact specif ## Specifications - **[IC Interface Specification](ic-interface-spec/index.md)**: System API, HTTPS interface, certified data, management canister, and formal specification of the Internet Computer. +- **[Message Execution Properties](message-execution-properties.md)**: The 11 properties governing atomicity, ordering, inter-canister call delivery, and cycle handling in ICP message execution. - **[HTTP Gateway Specification](http-gateway-protocol-spec.md)**: How boundary nodes serve canister HTTP responses with certification verification. - **[Candid Specification](candid-spec.md)**: The Candid interface description language: type system, encoding, and subtyping rules. - **[Internet Identity Specification](internet-identity-spec.md)**: Delegation chains, passkey management, and canister signatures. diff --git a/docs/references/message-execution-properties.md b/docs/references/message-execution-properties.md index 6aecbf8..ee482a3 100644 --- a/docs/references/message-execution-properties.md +++ b/docs/references/message-execution-properties.md @@ -1,6 +1,8 @@ --- title: "Properties of Message Executions on ICP" description: "The 11 properties of message execution on ICP, covering atomicity, ordering guarantees, inter-canister call delivery, and cycle handling for bounded-wait and unbounded-wait calls." +sidebar: + order: 11 --- ## Asynchronous messaging model @@ -17,17 +19,21 @@ These entry points can be called either by external users through the IC's HTTP A **message execution** is a set of consecutive instructions that a subnet executes when a canister's method is invoked. The code execution for any such method can be split into several message executions if the method makes inter-canister calls. The following properties are essential: -- **Property 1**: Only a single message execution is run at a time per canister. Message execution within a single canister is atomic and sequential, and never parallel. +#### Property 1 + +Only a single message execution is run at a time per canister. Message execution within a single canister is atomic and sequential, and never parallel. Note that parallel message execution over multiple canisters is possible; this property talks about just a single canister. -- **Property 2**: Each downstream call that a canister makes, query or update, triggers a message. When using `await` on the response from an inter-canister call, the code after the `await` (the callback, highlighted in blue) is executed as a separate message execution. +#### Property 2 + +Each downstream call that a canister makes, query or update, triggers a message. When using `await` on the response from an inter-canister call, the code after the `await` (the callback, highlighted in blue) is executed as a separate message execution. - For example, consider the following Motoko code: +For example, consider the following Motoko code: - ![example_highlighted_code](/img/docs/references/example_highlighted_code.png) +![example_highlighted_code](/img/docs/references/example_highlighted_code.png) - The first message execution spans the lines 2-3, until the inter-canister call is made using the `await` syntax (orange box). The second message execution spans lines 3-5 when the inter-canister call returns (blue box). This part is called the _callback_ of the inter-canister call. The two message executions involved in this example will always be scheduled sequentially. +The first message execution spans the lines 2-3, until the inter-canister call is made using the `await` syntax (orange box). The second message execution spans lines 3-5 when the inter-canister call returns (blue box). This part is called the _callback_ of the inter-canister call. The two message executions involved in this example will always be scheduled sequentially. :::note An `await` in the code does not necessarily mean that an inter-canister call is made and thus a message execution ends and the code after the `await` is executed as a separate message execution (callback). Async code with the `await` syntax (e.g. in Rust or Motoko) can also be used "internally" in the canister, without issuing an inter-canister call. In that case, the code part including the `await` will be processed within a single message execution. For Rust, both cases are possible if `await` is used. An inter-canister call is only made if the system API `ic0.call_perform` is called, e.g. when awaiting result of the CDK's `call` method. In Motoko, `await` always commits the current state and triggers a new message send, while `await*` does not necessarily commit the current state or trigger new message sends. See [Motoko actors and async programming](../languages/motoko/fundamentals/actors-async.md) for details on `await` vs. `await*`. @@ -37,41 +43,59 @@ An `await` in the code does not necessarily mean that an inter-canister call is In the Rust CDK, it is the `await` expression that triggers the canister call, rather than invoking the `call` function itself. That is, a call that is not `await`-ed is never executed. In Motoko, if the code does not `await` the response of a call, the call is still made, but the code after the call is executed in the same message execution, until the next inter-canister call is triggered using `await`. Also, multiple outgoing calls can be triggered in parallel from the same message execution; see the [parallel calls examples](https://github.com/dfinity/examples). ::: -- **Property 3**: Successfully delivered requests are received in the order in which they were sent. In particular, if a canister A sends `m1` and `m2` to canister B in that order, then, if both are accepted, `m1` is executed before `m2`. +#### Property 3 + +Successfully delivered requests are received in the order in which they were sent. In particular, if a canister A sends `m1` and `m2` to canister B in that order, then, if both are accepted, `m1` is executed before `m2`. :::note This property only gives a guarantee on when the request messages are executed, but there is no guarantee on the ordering of the responses received. ::: -- **Property 4**: Multiple message executions, e.g., from different calls, can interleave and have no reliable execution ordering. +#### Property 4 + +Multiple message executions, e.g., from different calls, can interleave and have no reliable execution ordering. + +Property 3 provides a guarantee on the order of message executions on a target canister. However, if multiple calls interleave, one cannot assume additional ordering guarantees for these interleaving calls. To illustrate this, let's consider the above example code again, and assume the method `example` is called twice in parallel, the resulting calls being Call 1 and Call 2. The following illustration shows two possible message execution orderings. On the left, the first call's message executions are scheduled first, and only then the second call's messages are executed. On the right, you can see another possible message execution scheduling, where the first messages of each call are executed first. Your code should result in a correct state regardless of the message execution ordering. + +![example_orderings](/img/docs/references/example_orderings.png) + +#### Property 5 + +On a trap or panic, modifications to the canister state for the current message execution are not applied. + +For example, if a trap occurs in the execution of the second message (blue box) of the above example, canister state changes resulting from that message execution, i.e. everything in the blue box, are discarded. However, note that any state changes from earlier message executions and in particular the first message execution (orange box) have been applied, as that message executed successfully. + +#### Property 6 + +Inter-canister calls are not guaranteed to be delivered to the destination canister, but they are guaranteed to be delivered at most once. When a call does reach the destination canister, the destination canister may trap or return a reject response while processing the call. - Property 3 provides a guarantee on the order of message executions on a target canister. However, if multiple calls interleave, one cannot assume additional ordering guarantees for these interleaving calls. To illustrate this, let's consider the above example code again, and assume the method `example` is called twice in parallel, the resulting calls being Call 1 and Call 2. The following illustration shows two possible message execution orderings. On the left, the first call's message executions are scheduled first, and only then the second call's messages are executed. On the right, you can see another possible message execution scheduling, where the first messages of each call are executed first. Your code should result in a correct state regardless of the message execution ordering. +There are many reasons why a call might not be delivered to the destination canister. Some of them are under the control of the canister developers, such as the destination having sufficient cycles to process the call. Others are not; the Internet Computer may decide to fail the call under high load. - ![example_orderings](/img/docs/references/example_orderings.png) +#### Property 7 -- **Property 5**: On a trap or panic, modifications to the canister state for the current message execution are not applied. +Every inter-canister call is guaranteed to receive a single response, either from the callee, or synthetically produced by the protocol. - For example, if a trap occurs in the execution of the second message (blue box) of the above example, canister state changes resulting from that message execution, i.e. everything in the blue box, are discarded. However, note that any state changes from earlier message executions and in particular the first message execution (orange box) have been applied, as that message executed successfully. +However, a malicious destination canister could choose to delay the response for arbitrarily long if it is willing to put in the required cycles. Also, the response does not have to be successful, but can also be a reject response. The reject may come from the called canister, but it may also be generated by ICP. Such protocol-generated rejects can occur at any time before the call reaches the callee-canister, as well as once the call does reach the callee-canister, for example if the callee-canister traps while processing the call. Thus, it's important that the calling canister handles reject responses as well. A reject response means that the message hasn't been successfully processed by the receiver but doesn't guarantee that the receiver's state wasn't changed. -- **Property 6**: Inter-canister calls are not guaranteed to be delivered to the destination canister, but they are guaranteed to be delivered at most once. When a call does reach the destination canister, the destination canister may trap or return a reject response while processing the call. +#### Property 8 - There are many reasons why a call might not be delivered to the destination canister. Some of them are under the control of the canister developers, such as the destination having sufficient cycles to process the call. Others are not; the Internet Computer may decide to fail the call under high load. +If the calling canister made an unbounded-wait (as opposed to a bounded-wait) inter-canister call, if the call is delivered to the callee and the callee responds without trapping, the protocol guarantees that the first such response will get back to the caller canister. Otherwise, the caller will receive a reject response (with the code never being `SYS_UNKNOWN`). -- **Property 7**: Every inter-canister call is guaranteed to receive a single response, either from the callee, or synthetically produced by the protocol. +#### Property 9 - However, a malicious destination canister could choose to delay the response for arbitrarily long if it is willing to put in the required cycles. Also, the response does not have to be successful, but can also be a reject response. The reject may come from the called canister, but it may also be generated by ICP. Such protocol-generated rejects can occur at any time before the call reaches the callee-canister, as well as once the call does reach the callee-canister, for example if the callee-canister traps while processing the call. Thus, it's important that the calling canister handles reject responses as well. A reject response means that the message hasn't been successfully processed by the receiver but doesn't guarantee that the receiver's state wasn't changed. +If the calling canister makes a bounded-wait call, the system may generate a reject response and deliver it to the caller. This can happen even if the call is successfully delivered to the callee and the callee responds without trapping. But this can only happen if the reject response is `SYS_UNKNOWN`. -- **Property 8**: If the calling canister made an unbounded-wait (as opposed to a bounded-wait) inter-canister call, if the call is delivered to the callee and the callee responds without trapping, the protocol guarantees that the first such response will get back to the caller canister. Otherwise, the caller will receive a reject response (with the code never being `SYS_UNKNOWN`). +Since, by property 7, the caller will only ever receive a single response, this means that the real response from the callee, if produced, will get dropped by the system if `SYS_UNKNOWN` is returned. -- **Property 9**: If the calling canister makes a bounded-wait call, the system may generate a reject response and deliver it to the caller. This can happen even if the call is successfully delivered to the callee and the callee responds without trapping. But this can only happen if the reject response is `SYS_UNKNOWN`. +#### Property 10 - Since, by property 7, the caller will only ever receive a single response, this means that the real response from the callee, if produced, will get dropped by the system if `SYS_UNKNOWN` is returned. +If cycles are attached to an unbounded-wait call, the sum of cycles accepted by the callee, and those refunded to the caller equals the amount that the caller attached. -- **Property 10**: If cycles are attached to an unbounded-wait call, the sum of cycles accepted by the callee, and those refunded to the caller equals the amount that the caller attached. +#### Property 11 -- **Property 11**: If cycles are attached to a bounded-wait call, they may get lost whenever a `SYS_UNKNOWN` response is received by the caller. In particular, any cycles refunded by the callee are lost, and if the callee doesn't receive the call, all attached cycles are lost. If any response other than `SYS_UNKNOWN` is received, property 10 holds even for bounded-wait calls. +If cycles are attached to a bounded-wait call, they may get lost whenever a `SYS_UNKNOWN` response is received by the caller. In particular, any cycles refunded by the callee are lost, and if the callee doesn't receive the call, all attached cycles are lost. If any response other than `SYS_UNKNOWN` is received, property 10 holds even for bounded-wait calls. - Note that cycles do not necessarily get lost. Even if the caller receives `SYS_UNKNOWN`, it can happen that the callee still receives the sent cycles. +Note that cycles do not necessarily get lost. Even if the caller receives `SYS_UNKNOWN`, it can happen that the callee still receives the sent cycles. For more details, refer to the [IC Interface Specification abstract behavior](./ic-interface-spec/abstract-behavior.md) which defines message execution in more detail.