doc: Add an initial document about verification

Signed-off-by: Changho Choi <ch754.choi@samsung.com>
islet-project · May 9, 2024 · a27a323 · a27a323
1 parent d5e2f2b
commit a27a323
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -27,6 +27,7 @@ machine-to-machine computing without the need for server intervention
 - Realm Management Monitor
 - Hardware Enforced Security
 - Confidential Computing API Standardization
+- Automated Verification
 - Use case : Confidential Machine Learning
 
 ## Overall Architecture

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
@@ -7,6 +7,7 @@
   - [Application Developer](./getting-started/app-dev.md)
   - [Platform Developer](./getting-started/plat-dev.md)
     - [Network Configuration](./network.md)
+  - [Verification](./getting-started/verification.md)
 - [Components](./components/index.md)
   - [CCA platform architecture](./components/cca_design.md)
   - [Realm Management Monitor](./components/rmm.md)

diff --git a/doc/getting-started/index.md b/doc/getting-started/index.md
@@ -2,3 +2,4 @@
 - [1.1. About CCA](https://islet-project.github.io/islet/getting-started/cca.html)
 - [1.2. Application Developer](https://islet-project.github.io/islet/getting-started/app-dev.html)
 - [1.3. Platform Developer](https://islet-project.github.io/islet/getting-started/plat-dev.html)
+- [1.4. Verification](https://islet-project.github.io/islet/getting-started/verification.html)
diff --git a/doc/getting-started/verification.md b/doc/getting-started/verification.md
@@ -0,0 +1,27 @@
+# Verification
+
+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
+harnesses which are extracted from Machine Readable Specification. It would help to check
+the conformance of the two systems written in different languages.
+
+## Verification dependency
+* [patched Kani](https://github.com/zpzigi754/kani/tree/use-aarch64-latest)
+
+## Available RMI targets
+
+```sh
+rmi_features
+rmi_granule_delegate
+rmi_granule_undelegate
+```
+
+## Verifying Islet
+
+```sh
+(in islet/model-checking)
+
+# Choose one among the list in `Available RMI targets` for the value of `RMI_TARGET`
+$ RMI_TARGET=rmi_granule_undelegate make verify
+```