Update and fix documentation

doc/SUMMARY.md

@@ -6,22 +6,25 @@
   - [About CCA](./getting-started/cca.md)
   - [How to Build and Run Islet](./getting-started/islet-how-to.md)
     - [Network Configuration](./getting-started/network.md)
-    - [Command Shortcut](./getting-started/run-shortcut.md)
   - [Application Developer](./getting-started/app-dev.md)
 - [Components](./components/index.md)
   - [CCA platform architecture](./components/cca_design.md)
   - [Realm Management Monitor](./components/rmm.md)
-  - [Command Line Interface](./components/cli.md)
+    - [Remote attestation](./components/remote_attestation.md)
+    - [Sealing Key Derivation](./components/sealing.md)
+    - [Realm metadata](./components/realm_metadata.md)
+    - [Vendor-specific SMC Allocation for Realm Metadata mechanism and Sealing Keys Derivation](./components/vendor_specific_smcs.md)
+  - [Hardware Enforced Security](./components/hes.md)
   - [Software Development Kit](./components/sdk.md)
     - [SDK Design](./sdk-sdd.md)
   - [Attestation](./components/attestation.md)
   - [Certifier](./components/certifier.md)
-- Coding Standards
+- [Coding Standards](./coding-standards/index.md)
   - [Platform development](./platform-development/index.md)
     - [Secure interactions with the Host](./platform-development/secure-interaction.md)
   - [Rust Unsafe Code](./coding-standards/rust-unsafe-analysis.md)
   - [Format and Lint](./coding-standards/format-lint.md)
-- Code Analysis
+- [Code Analysis](./code-analysis/index.md)
   - [RMM Spec Compliance Test](./code-analysis/unit-tests.md)
   - [Verification](./code-analysis/verification.md)
     - [Model Checking](./code-analysis/islet-model-checking.md)
@@ -31,6 +34,8 @@
   - [Confidential Machine Learning](./usecases/confidential_ml.md)
   - [Cross Platform E2EE](./usecases/cross-platform-e2ee.md)
   - [Remote Attestation](./usecases/remote-attestation.md)
+    - [Remote Attestation Example](./usecases/remote-attestation-running.md)
+  - [Application Provisioning](./usecases/app-provisioning.md)
 - [Rust Crates](./crates/index.md)
   - [Realm Management Monitor](./plat-doc/islet_rmm/index.html)
   - [Confidential Application SDK](./app-doc/islet_sdk/index.html)

doc/book.toml

@@ -1,9 +1,14 @@
 [book]
 authors = ["Islet Contributors"]
 language = "en"
-multilingual = false
+#multilingual = false
 src = "."
 title = "Islet Documentation"
 
 [build]
 build-dir = "../out/book"
+
+[output.html]
+additional-js = [ "zoom.js" ]
+additional-css = [ "custom.css" ]
+

doc/code-analysis/fuzzing.md

@@ -1,5 +1,8 @@
 # Fuzz Testing Guide for Islet RMM
 
+> [!NOTE]
+> This document regards an older version of Islet (tag [ccav1.0-eac5](https://github.com/islet-project/islet/releases/tag/ccav1.0-eac5)).
+
 ## Overview
 Islet is built in Rust, which inherently ensures memory safety by design. To further enhance security, we employ tools like **Miri** to verify that `unsafe` code adheres to safety rules and **Kani**, a model checker, for formal verification. Beyond these measures, we also incorporate fuzz testing, a proven method for discovering vulnerabilities, into the Islet RMM development process. We utilize **cargo fuzz**, which leverages **libFuzzer**, to perform fuzz testing effectively.
 
@@ -138,9 +141,9 @@ By default, `rust-fuzz` fuzzes a raw bytearray which is not suitable for Islet R
 ```
 
 - The above snippet demonstrates an example of RSI fuzzing. Much of the setup remains similar to RMI fuzzing.
-- The `MEASUREMENT_EXTEND` RSI command is run using `REC_ENTER` RMI command as seen in lines 26-40. 
+- The `MEASUREMENT_EXTEND` RSI command is run using `REC_ENTER` RMI command as seen in lines 26-40.
 
-In normal contexts, `REC_ENTER` takes only two arguments but in fuzzing contexts, it can take a variable number of arguments. The third argument is the RSI call command and further arguments are passed as arguments to the RSI call. This is needed as realm code is not exercised in fuzzing. 
+In normal contexts, `REC_ENTER` takes only two arguments but in fuzzing contexts, it can take a variable number of arguments. The third argument is the RSI call command and further arguments are passed as arguments to the RSI call. This is needed as realm code is not exercised in fuzzing.
 
 The same method can also be used to simulate non-RSI realm exit scenarios by using the pseudo-call `REC_ENTER_EXIT_CMD` followed by the exit code and their arguments as shows in the below example.
 

doc/code-analysis/index.md

@@ -0,0 +1,6 @@
+# Contents
+- [4.1. RMM Spec Compliance Test](./unit-tests.html)
+- [4.2. Verification](./verification.html)
+    - [4.2.1 Model Checking](./islet-model-checking.html)
+- [4.3 Fuzzing](./fuzzing.html)
+- [4.4 Miri](./miri.html)

doc/code-analysis/verification.md

@@ -1,5 +1,8 @@
 # Verification
 
+> [!NOTE]
+> This document regards an older version of Islet (tag [v1.0-seur](https://github.com/islet-project/islet/releases/tag/v1.0-seur)).
+
 We formally verify Islet using [Kani](https://github.com/model-checking/kani/)'s model
 checking. Our verification harnesses adopt the same input and output conditions as well
 as similar structures used in [TF-RMM](https://www.trustedfirmware.org/projects/tf-rmm/)'s

doc/coding-standards/index.md

@@ -0,0 +1,5 @@
+# Contents
+- [3.1. Platform development](../platform-development/index.html)
+    - [3.1.1 Secure interactions with the Host](../platform-development/secure-interaction.html)
+- [3.2. Rust Unsafe Code](./rust-unsafe-analysis.html)
+- [3.3. Format and Lint](./format-lint.html)

doc/components/attestation.md

@@ -12,7 +12,7 @@ An attestation report (shortly, *report*) is an *evidence* produced by *attester
 - *CCA Platform token*: it is used to assure that *attester* is running on a secure CCA platform. It covers the measurements of CCA platform components (e.g., RMM and EL3M) and whether it is in debug state.
 - *Realm token*: this token is used to hold the measurement of Realm, which is equivalent to a virtual machine that may contain kernel and root file system.
 
-You can quickly test and see what this report looks like through [our CLI tool](https://islet-project.github.io/islet/components/cli.html).
+You can quickly test and see what this report looks like through [our rsictl tool](https://github.com/islet-project/rsictl).
 
 ## Appraisal policy
 

doc/components/hes.md

@@ -0,0 +1 @@
+../../hes/README.md

doc/components/images

@@ -0,0 +1 @@
+../../hes/images/

doc/components/index.md

@@ -1,7 +1,11 @@
 # Contents
-- [2.1. CCA platform architecture](https://islet-project.github.io/islet/components/cca_design.html)
-- [2.2. Realm Management Monitor](https://islet-project.github.io/islet/components/rmm.html)
-- [2.3. Command Line Interface](https://islet-project.github.io/islet/components/cli.html)
-- [2.4. Software Development Kit](https://islet-project.github.io/islet/components/sdk.html)
-- [2.5. Attestation](https://islet-project.github.io/islet/components/attestation.html)
-- [2.6. Certifier](https://islet-project.github.io/islet/components/certifier.html)
+- [2.1. CCA platform architecture](./cca_design.html)
+- [2.2. Realm Management Monitor](./rmm.html)
+    - [2.2.1 Remote attestation](./remote_attestation.html)
+    - [2.2.2 Sealing Key Derivation](./sealing.html)
+    - [2.2.3 Realm metadata](./realm_metadata.html)
+    - [2.2.4 Vendor-Specific SMC Allocation for Realm Metadata Mechanism and Sealing Keys Derivation](./vendor_specific_smcs.html)
+- [2.3. Hardware Enforced Security](./hes.html)
+- [2.4. Software Development Kit](./sdk.html)
+- [2.5. Attestation](./attestation.html)
+- [2.6. Certifier](./certifier.html)

doc/components/metadata-sequence.puml

@@ -0,0 +1,18 @@
+@startuml
+hide footbox
+
+entity Host
+entity RMM
+
+note over Host, RMM: D1.2.1 Realm creation flow
+Host -> Host: (mdg, meta_ptr) = alloc_granules()
+Host -> Host: Initialize meta_ptr
+note over Host:  Realm metadata (meta_ptr) is passed as an NS granule
+Host -> RMM: RMI_GRANULE_DELEGATE(mdg)
+RMM --> Host: RMI_SUCCESS
+Host -> RMM: RMI_ISLET_REALM_SET_METADATA(rd, mdg, meta_ptr)
+note over RMM:- populate the metadata granule (mdg) with the metadata (pointed by meta_ptr)\n- set the rd.g_metadata := granule(mdg)\n- transition the metadata granule (mdg) state to METADATA
+RMM --> Host: RMI_SUCCESS
+Host -> Host: free_granule(meta_ptr)
+note over Host, RMM: RMI_REALM_ACTIVATE
+@enduml