Verifying Function Execution

In the Attesting Function Calls tutorial, we described how to use the Blocky AS CLI to attest a function call. The result was an enclave attestation and a transitive attestation 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
• Make sure you have Docker, jq, and yq installed on your system.
• (Optional) Review the Attesting Function Calls tutorial.
• (Optional) Review Blocky AS 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 tutorial we obtained out.json that contains an enclave attestation enclave_attested_application_public_key and a transitive attestation transitive_attested_function_call. In the Attesting Function Calls 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 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.11/out.json

We can inspect the claims of the attestations in out.json by running

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

giving something like us:

{
  "platform": "nitro",
  "code": "bb2600f6f2ef338a4f6f9f6e3e047d5e1191ba91441a669e7f34adbf642dab149fdeaee79aa50bc8cb724fb9e60e6cd1.4b4d5b3661b3efc12920900c80e126e4ce783c522de6c02a2a5bf7af3a2b9327b86776f188e4be1c1c404a129dbda493.f4a094cdf5e9532b57cb5ad57a637fb7df303d87a21645e1b047d2e6e02ce5bb55f7619b8670b7c60f521407cb120969"
}
{
  "hash_of_code": "9f644e9815fd94b44a0376718563353376b99feafd8fafe8ba1f59e746e073ea16388afb9be633566158dc62bc472ab8eaa39e44d4e0702797be34bc04f61fec",
  "function": "helloWorld",
  "hash_of_input": "a69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26",
  "output": "SGVsbG8sIFdvcmxkIQ==",
  "hash_of_secrets": "9375447cd5307bf7473b8200f039b60a3be491282f852df9f42ce31a8a43f6f8e916c4f8264e7d233add48746a40166eec588be8b7b9b16a5eb698d4c3b06e00"
}

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:

ENCLAVE_PLATFORM=$(jq -r '.enclave_attested_application_public_key.claims.enclave_measurement.platform' out.json)
echo $ENCLAVE_PLATFORM
ENCLAVE_CODE=$(jq -r '.enclave_attested_application_public_key.claims.enclave_measurement.code' out.json)
echo $ENCLAVE_CODE

The ENCLAVE_PLATFORM value 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 ENCLAVE_CODE value 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. On the Releases page we list platform and code measurements for each Blocky AS release. We can download the code_measurement.toml file for the v0.1.0-beta.11 release and extract its measurements by running:

RELEASE_PLATFORM=$(yq '.code_measurement[0].platform' code_measurement.toml)
echo $RELEASE_PLATFORM
RELEASE_CODE=$(yq '.code_measurement[0].code' code_measurement.toml)
echo $RELEASE_CODE

Now we can compare these measurements with:

diff <(echo "$ENCLAVE_PLATFORM") <(echo "$RELEASE_PLATFORM")
diff <(echo "$ENCLAVE_CODE") <(echo "$RELEASE_CODE")

When diff calls produce no output, it means that the values are the same, and so the enclave attestation in out.json attests that it was produced by the Blocky AS server code available in the v0.1.0-beta.11 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.11 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/$RELEASE_PLATFORM/$RELEASE_CODE 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 > /dev/null

The reproducible build process produces a description of the enclave image file (delphi/output/eif-description.json), which contains its measurements. We can parse these measurements and combine them into a single string by running:

BUILT_CODE=$(jq -r '.Measurements | [.PCR0, .PCR1, .PCR2] | map(select(. != null)) | join(".")' delphi/output/eif-description.json);
echo $BUILT_CODE

We can now compare the $BUILT_CODE with RELEASE_CODE parsed from the enclave_attested_application_public_key.

diff <(echo "$BUILT_CODE") <(echo "$RELEASE_CODE")

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 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.

Step 4: Verify Attestation Signatures

To verify the claims made by the attestations, we need to verify their signatures. As validated in Step 2, 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 produced by the bky-as attest-fn-call command is verified on output. So, if you've obtained 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.

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 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. Simply extract the raw enclave and transitive attestations from out.json, or your long-term storage, and pass them to bky-as verify-fn-call command:

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

Notice that verified.json is identical 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 to the guarantees we defined in the Overview section of this tutorial.

From Step 4, 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, we know that the BUILT_CODE measurement matches the RELEASE_CODE measurement and from Step 1 we know that RELEASE_CODE measurement matches the ENCLAVE_CODE measurement. As a consequence, we know that the ENCLAVE_CODE 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, 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 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 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 to use their output to trigger on-chain actions in your smart contracts.