[[ ":$PATH:" != *":$HOME/.bky:"* ]] && export PATH="$PATH:$HOME/.bky"
ln -sf "$HOME/.bky/bky-as-v0.1.0-beta.12" "$HOME/.bky/bky-as"

# Verifying Function Execution

In the [Attesting Function Calls](/attestation-service/v0.1.0-beta.12/attest-fn-call) tutorial, we described how
to use the Blocky AS CLI to attest a function call. The result was an
[enclave attestation](/attestation-service/v0.1.0-beta.12/concepts#enclave-attestations) and a
[transitive attestation](/attestation-service/v0.1.0-beta.12/concepts#transitive-attestations) that work
together to attest the function execution. In this tutorial, we go over how to
verify the claims made by these attestations to trust an execution of an
attested function call.

## Prerequisites

- Install the [Blocky AS CLI](https://github.com/blocky/attestation-service-cli)
by following the [Getting Started](/attestation-service/v0.1.0-beta.12#setup) instructions.
- Make sure you have
[Docker](https://www.docker.com/),
[jq](https://jqlang.org/), and
[yq](https://github.com/mikefarah/yq)
installed on your system.
- Create a `verification` directory and navigate into it by running:
mkdir -p verification
cd verification
- (Optional) Review the [Attesting Function Calls](/attestation-service/v0.1.0-beta.12/attest-fn-call)
tutorial.
- (Optional) Review Blocky AS [Concepts](/attestation-service/v0.1.0-beta.12/concepts) page.


## Overview

Trusting the execution of an attested function call means verifying that the
function code was executed faithfully on given inputs and secrets, producing a
specific output, while ensuring that intermediate function state and secrets are
not leaked.

Let's define these goals more precisely as a set of guarantees:

- Guarantee 1: Attested function output is the result of an execution of a
specific function on given inputs and secrets.
- Guarantee 2: The intermediate state of the function execution is not tampered
with.
- Guarantee 3: The intermediate state of the function execution is not leaked.
- Guarantee 4: The secrets passed to the function are not leaked.


The Blocky AS attestations make these guarantees concrete through a set of
claims. In the [Attesting Function Calls](/attestation-service/v0.1.0-beta.12/attest-fn-call) tutorial we
obtained `out.json` that contains an
[enclave attestation](/attestation-service/v0.1.0-beta.12/concepts#enclave-attestations)
`enclave_attested_application_public_key` and a
[transitive attestation](/attestation-service/v0.1.0-beta.12/concepts#transitive-attestations)
`transitive_attested_function_call`.
In the [Attesting Function Calls](/attestation-service/v0.1.0-beta.12/attest-fn-call) tutorial we invoked a
function on a local server running in dev mode, i.e. not on a TEE enclave.
For this tutorial, we've prepared [out.json](/v0.1.0-beta.12/out.json)
containing attestations over the same "Hello World" function produced by a Blocky
AS server running on an AWS Nitro Enclave TEE. Download it by running:

curl -o out.json https://docs.blocky.rocks/v0.1.0-beta.12/out.json

We can inspect the claims of the attestations in [out.json](/v0.1.0-beta.12/out.json) by running

jq '.enclave_attested_application_public_key.claims.enclave_measurement' out.json
jq '.transitive_attested_function_call.claims' out.json

Together, these attestations claim that a Blocky AS server with an enclave image
measurement `code` ran on a `platform` (in this case an AWS Nitro Enclave TEE)
and invoked a `function` (in this case `helloWorld`) on a WASM binary with a
hash of `hash_of_code` using an input with a hash of `hash_of_input` and secrets
with a hash of `hash_of_secrets`, producing an output encoded in base64 in the
`output` field (in this case, `SGVsbG8sIFdvcmxkIQ==`, which decodes to
`Hello, World!`).

In this tutorial, we go over how to verify these claims are subject to the
guarantees we defined above, and so how to trust the execution of the attested
function call.

## Verification Process

### Step 1: Identify Blocky AS Release

To verify the claims made by the attestations, we need to identify the Blocky AS
server implementation that produced the attestations. Let's parse out the
attested Blocky AS `code` and runtime `platform` from the
`enclave_attested_application_public_key` enclave attestation
in [out.json](/v0.1.0-beta.12/out.json) by running:

jq -r '.enclave_attested_application_public_key.claims.enclave_measurement.platform' out.json > enclave_platform.txt
cat enclave_platform.txt
jq -r '.enclave_attested_application_public_key.claims.enclave_measurement.code' out.json > enclave_code.txt
cat enclave_code.txt

The value in `enclave_platform.txt` indicates the runtime platform of the Blocky
AS server. In this example, it is `nitro`, indicating that the Blocky AS server
was running on an AWS Nitro Enclave TEE. The value in `enclave_code.txt` is a
measurement of the enclave image containing the Blocky AS server application
running inside a TEE.

These values allow us to identify the Blocky AS server implementation that
produced the attestations [out.json](/v0.1.0-beta.12/out.json).
On the [Releases](/releases) page we list `platform` and `code`
measurements for each Blocky AS release.
We can download the
[code_measurement.toml](/v0.1.0-beta.12/code_measurement.toml)
file for the `v0.1.0-beta.12` release by running:

curl -o code_measurement.toml https://docs.blocky.rocks/v0.1.0-beta.12/code_measurement.toml

and extract its measurements by running:

yq '.code_measurement[0].platform' code_measurement.toml > release_platform.txt
cat release_platform.txt
yq '.code_measurement[0].code' code_measurement.toml > release_code.txt
cat release_code.txt

Now we can compare these measurements with:

diff enclave_platform.txt release_platform.txt
diff enclave_code.txt release_code.txt

When `diff` calls produce no output, it means that the values are the same, and
so the enclave attestation in [out.json](/v0.1.0-beta.12/out.json) attests that it was produced
by the Blocky AS server code available in the `v0.1.0-beta.12` release.

### Step 2: Identifying Release Code

Next, we need to identify the Blocky AS server source code behind the release.
We use the `v0.1.0-beta.12` release information, from the previous step, to form
a S3 bucket URL, from which we can download and unpack the source code archive:

aws s3 cp s3://enclave-archive/$(cat release_platform.txt)/$(cat release_code.txt) delphi.tar.gz
tar -xzf delphi.tar.gz

The resulting `delphi` folder contains the Blocky AS server source code in
`delphi/src.tgz` archive.
We can use it to build the Blocky AS server enclave image and compute its
measurement by running:

make -C delphi build

The reproducible build process produces a description of the enclave image file
(`delphi/output/eif-description.json`), which contains its
[measurements](https://docs.aws.amazon.com/enclaves/latest/user/set-up-attestation.html#where).
We can parse these measurements and combine them into a single string by
running:

jq -r '.Measurements | [.PCR0, .PCR1, .PCR2] | map(select(. != null)) | join(".")' delphi/output/eif-description.json > built_code.txt
cat built_code.txt

We can now compare the `built_code.txt` with `release_code.txt` parsed from
the `enclave_attested_application_public_key`.

diff built_code.txt release_code.txt

When `diff` produces no output, the measurement of the enclave image file we
built from source matches the one of the release.

> Note that `delphi/LICENSES/BLOCKY-SARL-1_0.txt` contains source-available
license for the Blocky AS server code, which allows you to inspect the code
and to build it for the purpose of computing its measurements. It does not,
however, allow you to modify, redistribute, or run the code.


### Step 3: Inspect Blocky AS Implementation

For the claims made by the attestations to be meaningful, we need to inspect
Blocky AS server code for each release to validate several properties of its
implementation.
These properties are:

- Property 1: Blocky AS server generates a unique public/private key pair on
startup and retains control of the private key.
- Property 2: Blocky AS server enclave attestations attest the unique public
key.
- Property 3: Blocky AS server uses its private key to sign transitive
attestations
of function calls executed by the Blocky AS server.
- Property 4: Blocky AS executes WASM binaries and faithfully attests the
invoked function, its inputs, secrets, output, and hash of the WASM binary.
- Property 5: Blocky AS server does not allow tampering with the intermediate
state of the function execution.
- Property 6: Blocky AS server does not leak the intermediate state of the
function execution.
- Property 7: Blocky AS server does not leak the secrets passed to the function.


To verify the claims made by the attestations, we need to verify their
signatures. As described on the [Concepts](/attestation-service/v0.1.0-beta.12/concepts) page, Blocky
AS generates a new public/private key pair `encl_app_pub_key/encl_app_priv_key`
on startup. The enclave attestation
`enclave_attested_application_public_key` attests the `encl_app_pub_key` and is
signed by the TEE hardware manufacturer's private key `tee_priv_key`, which is
the root of trust for TEE enclaves. The transitive attestation
`transitive_attested_function_call`, attesting the execution of a function, is
signed by the `encl_app_priv_key` attested in
`enclave_attested_application_public_key`.

> Note that depending on your function implementation, you may need to verify
additional properties, such as whether Blocky AS correctly implements random
number generation, timestamp generation, and HTTPS request handling.


We can then validate Properties 1 through 7 by inspecting the source code in the
`delphi/src.tgz` archive.
The validation of these properties should be done once per Blocky AS release and
is akin
to inspecting and auditing the implementation of a smart contract or of a
blockchain node and relies on the availability of our code. This
process can be done collectively by Blocky's users as well as auditors. If
you'd like help in understanding a Blocky AS server implementation,
please reach out to us on Telegram [@blocky_rocks](https://t.me/blocky_rocks).

### Step 4: Verify Attestation Signatures

To verify the claims made by the attestations, we need to verify their
signatures. As validated in [Step 2](#step-3-inspect-blocky-as-implementation),
Blocky AS generates a unique public/private key pair
`encl_app_pub_key/encl_app_priv_key`
on startup. The enclave attestation
`enclave_attested_application_public_key` attests the `encl_app_pub_key` and is
signed by the TEE hardware manufacturer's private key `tee_priv_key`, which is
the root of trust for TEE enclaves. The transitive attestation
`transitive_attested_function_call`, attesting the execution of a function, is
signed by the `encl_app_priv_key` attested in
`enclave_attested_application_public_key`.

The [out.json](/v0.1.0-beta.12/out.json) produced by the
[`bky-as attest-fn-call` command](/attestation-service/v0.1.0-beta.12/attest-fn-call) is verified on output.
So, if you've obtained [out.json](/v0.1.0-beta.12/out.json) from `bky-as` yourself, you know
that

1. `enclave_attested_application_public_key` signature is valid against the TEE
hardware manufacturer's public key `tee_pub_key` embedded in the Blocky AS
CLI
2. `transitive_attested_function_call` signature is valid against the
`encl_app_pub_key` attested in `enclave_attested_application_public_key`
3. `transitive_attested_function_call.claims`
come from parsing `transitive_attested_function_call.transitive_attestation`


and can proceed to
[Relating Attestation Claims to Blocky AS Guarantees](#relating-attestation-claims-to-blocky-as-guarantees).

> We may also use the code in the release archive to build the `bky-as` CLI
and compare its hash against the one installed on your machine. By inspecting
the CLI code, you can convince yourself that it users the correct TEE root of
trust public key and the correct processes to parse and verify Blocky AS
attestations.


If you received [out.json](/v0.1.0-beta.12/out.json) from a third party, or if
you archived `enclave_attested_application_public_key` and
`transitive_attested_function_call` in long-term storage, you may want to verify
the signatures of the attestations yourself.

The easiest way to verify these signatures is to use the `bky-as` CLI. If you
went through the [Getting Started](/attestation-service/v0.1.0-beta.12#setup) process, you should already
have a `config.toml` configured with the `acceptable_measurements` for the
current release. If you haven't, you can download a config file for this
tutorial by running:

curl -o config.toml https://docs.blocky.rocks/v0.1.0-beta.12/config.toml

To verify previously obtained attestations, simply extract the raw enclave and
transitive attestations from [out.json](/v0.1.0-beta.12/out.json), or your
long-term storage, and pass them to `bky-as verify-fn-call` command by running:

jq '{
enclave_attested_application_public_key: .enclave_attested_application_public_key.enclave_attestation,
transitive_attested_function_call: .transitive_attested_function_call.transitive_attestation
}' out.json | bky-as verify-fn-call > verified.json
cat verified.json

Notice that `verified.json` is identical in content to `out.json` by running:

diff <(jq -S '.' out.json) <(jq -S '.' verified.json)

When the `bky-as verify-fn-call` command succeeds, you know that the points
1-3 above hold true for attestations in `verified.json`.

## Relating Attestation Claims to Blocky AS Guarantees

Let's put all the pieces together and relate the claims made by the
attestations in [out.json](/v0.1.0-beta.12/out.json) to the guarantees we defined in the
[Overview](#overview) section of this tutorial.

From [Step 4](#step-4-verify-attestation-signatures), we know that the
`enclave_attested_application_public_key` attestation was signed by the TEE
hardware manufacturer's private key `tee_priv_key`, which is the root of trust
for TEE enclaves. As a consequence, we know that the
`enclave_attested_application_public_key` was generated inside a TEE.

From [Step 2](#step-2-identifying-release-code), we know that the `BUILT_CODE`
measurement matches the `RELEASE_CODE` measurement and
from [Step 1](#step-1-identify-blocky-as-release)
we know that `RELEASE_CODE` measurement matches the `enclave_code.txt` measurement.
As a consequence, we know that the `enclave_code.txt` measurement matches the
`BUILT_CODE` measurement and that `enclave_attested_application_public_key` was
produced by code in `delphi/src.tgz` archive.

Combining these facts, we know that the Blocky AS server ran on code in
`delphi/src.tgz` on a TEE.

From [Step 3](#step-3-inspect-blocky-as-implementation), we know the Blocky AS
server code in `delphi/src.tgz` has the following properties:

- Property 1: Blocky AS server generates a unique public/private key pair on
startup and retains control of the private key.
- Property 2: Blocky AS server enclave attestations attest the unique public
key.
- Property 3: Blocky AS server uses its private key to sign transitive
attestations of function calls executed by the Blocky AS server.
- Property 4: Blocky AS executes WASM binaries and faithfully attests the
invoked function, its inputs, secrets, output, and hash of the WASM binary.
- Property 5: Blocky AS server does not allow tampering with the intermediate
state of the function execution.
- Property 6: Blocky AS server does not leak the intermediate state of the
function execution.
- Property 7: Blocky AS server does not leak the secrets passed to the function.


From [Step 4](#step-4-verify-attestation-signatures) and Properties 1 and 2 we
know that `enclave_attested_application_public_key` attests the unique public
key `encl_app_pub_key` of the Blocky AS server. Further, from Property 3 we know
that `transitive_attested_function_call` is signed by
the unique private key `encl_app_priv_key` of the Blocky AS server. Finally,
from Property 4 we know that `transitive_attested_function_call` claims
represent the execution of a function in a WASM binary, which was executed by
the Blocky AS server inside a TEE enclave.

Ultimately, we can proceed to demonstrate the guarantees of Blocky AS defined in
the [Overview](#overview) section of this tutorial:

- Guarantee 1: Attested function output is the result of an execution of a
specific function on given inputs and secrets, since
`transitive_attested_function_call` contains the
`hash_of_code`, `function`, `hash_of_input`, `hash_of_secrets`, and
`output` fields, which attest the function execution on a TEE.
- Guarantee 2: The intermediate state of the function execution is not tampered
with, since the function execution took place inside a TEE and Property 5
guarantees that the Blocky AS server does not allow tampering with the
intermediate state of the function execution.
- Guarantee 3: The intermediate state of the function execution is not leaked
since the function execution took place inside a TEE and Property 6 guarantees
that the Blocky AS server does not leak the intermediate state of the function
execution.
- Guarantee 4: The secrets passed to the function are not leaked, since the
function execution took place inside a TEE and Property 7 guarantees that the
Blocky AS server does not leak the secrets passed to the function.


## Summary

OK, that was a lot of detail. Let's zoom out summarize the facts we learned
in the verification process.

Simply put, attested function output:

jq -r '.transitive_attested_function_call.claims.output | @base64d' out.json

was produced by invoking the:

jq -r '.transitive_attested_function_call.claims.function' out.json

function in a WASM binary that hashes to:

jq -r '.transitive_attested_function_call.claims.hash_of_code' out.json

on input hashing to:

jq -r '.transitive_attested_function_call.claims.hash_of_input' out.json

and secrets hashing to:

jq -r '.transitive_attested_function_call.claims.hash_of_secrets' out.json

while ensuring that the intermediate state of the function execution is not
tampered with and is not leaked, and that the secrets passed to the function are
not leaked, since the function execution took place inside a TEE enclave.

Now you, or anyone else, with `out.json` can verify these claims by following
the verification process described in this tutorial, and so trust the execution
of the attested function call.

## Next Steps

You can store Blocky AS attestations to always demonstrate the veracity of the
attested function output. You can also
[verify Blocky AS attestations on chain](/attestation-service/v0.1.0-beta.12/on-chain)
to use their output to trigger on-chain actions in your smart contracts.

rm -rf verification