diff --git a/SPIN-verification/LICENSE.txt b/formal-verification/LICENSE.txt similarity index 100% rename from SPIN-verification/LICENSE.txt rename to formal-verification/LICENSE.txt diff --git a/SPIN-verification/README.md b/formal-verification/README.md similarity index 71% rename from SPIN-verification/README.md rename to formal-verification/README.md index c315b0f..8c7c136 100644 --- a/SPIN-verification/README.md +++ b/formal-verification/README.md @@ -1,38 +1,40 @@ # A Functional Verification of the KMS in SPIN -Verification in SPIN that verifies the functionality of KEK assignment, encryption, decryption and re-encryption.
-There are 4 different models that each verify different operations.
+Verification in SPIN that verifies the functionality of KEK assignment, encryption, decryption and re-encryption. + +There are 4 different models that each verify different operations. ## Models -Model can be set by changing the MODEL constant.
- -1=A 2=B 3=C 4=D In the paper.
+Model can be set by changing the MODEL constant. + +1=A 2=B 3=C 4=D In the paper. -1: Assignemnt and Encryption.
-2: Decryption after assignment and encryption has been finalized.
-3: Re-Encryption of envelopes after assignment and encryption has been finalized.
-4: Tenant 1 assignment and encryption then invalid credentials, Tenant 2 only Decrypts envelopes received from Tenant 1 with different grants.
+1: Assignemnt and Encryption. +2: Decryption after assignment and encryption has been finalized. +3: Re-Encryption of envelopes after assignment and encryption has been finalized. +4: Tenant 1 assignment and encryption then invalid credentials, Tenant 2 only Decrypts envelopes received from Tenant 1 with different grants. -If MODEL == 1 then IS_MODEL_1 == 1
-If MODEL != 1 then IS_MODEL_1 == 0
+If MODEL == 1 then IS_MODEL_1 == 1 +If MODEL != 1 then IS_MODEL_1 == 0 ## To Run and Verify -Most of this can be done with an external tool such as iSPIN, additional information found [here](https://spinroot.com/spin/Man/README.html).
-**Run Code**
-spin -T model.pml - Regular run that will halt on error and print any statements in the code.
-spin -a model.pml - generates pan.c for verification.
+Most of this can be done with an external tool such as iSPIN, additional information found [here](https://spinroot.com/spin/Man/README.html). -**Compile pan.c**
-gcc -DMEMLIM=N -O2 -DXUSAFE -DCOLLAPSE -DNFAIR=3 (-DSAFETY) -w -o pan pan.c
+**Run Code** +spin -T model.pml - Regular run that will halt on error and print any statements in the code. +spin -a model.pml - generates pan.c for verification. --DSAFETY used when verifying safety.
+**Compile pan.c** +gcc -DMEMLIM=N -O2 -DXUSAFE -DCOLLAPSE -DNFAIR=3 (-DSAFETY) -w -o pan pan.c -**Verify**
-./pan -mN (-a -f) (-N claim)
-In -mN, N is an integer for max depth, however -N is a flag to specify which claim to verify, e.g ./pan -m1000000 -N safety
--a -f used when verifying liveness.
+-DSAFETY used when verifying safety. + +**Verify** +./pan -mN (-a -f) (-N claim) +In -mN, N is an integer for max depth, however -N is a flag to specify which claim to verify, e.g ./pan -m1000000 -N safety +-a -f used when verifying liveness. # Additional Documentation @@ -42,23 +44,24 @@ This project implements a key management service (KMS) based on the design and f ### Architecture -The current implementation in the Valv repository does not yet fully reflect the layered architecture described in the thesis. Instead, it implements a single-layer structure with envelope encryption, where a KEK is used to encrypt data or a DEK (see encrypt() in `crates/keystore/src/lib.rs`). +The current implementation in the Valv repository does not yet fully reflect the layered architecture described in the thesis. Instead, it implements a single-layer structure with envelope encryption, where a KEK is used to encrypt data or a DEK (see encrypt() in `crates/valv/src/lib.rs`). ### Protocol Operations The verified protocol operations are partially implemented: -1. **KEK Assignment**: Implemented in `crates/keystore/src/lib.rs` in the `create_crypto_key()` function of the `KeystoreAPI` trait. The `ValvAPI` struct in `crates/valv/src/main.rs` exposes this functionality. +1. **KEK Assignment**: Implemented in `crates/valv/src/lib.rs` in the `create_crypto_key()` function of the `ValvAPI` trait. The `API` struct in `crates/valv/src/api/server.rs` exposes this functionality. -2. **Encryption**: Core encryption logic is in `crates/keystore/src/lib.rs` in the `encrypt()` function of the `KeystoreAPI` trait. The `ValvAPI` in `crates/valv/src/main.rs` will expose this through the `encrypt` method (currently unimplemented). +2. **Encryption**: Core encryption logic is in `crates/valv/src/lib.rs` in the `encrypt()` function of the `ValvAPI` trait. The `API` struct in `crates/valv/src/api/server.rs` exposes this functionality. -3. **Decryption**: Implemented in `crates/keystore/src/lib.rs` in the `decrypt()` function of the `KeystoreAPI` trait. The `ValvAPI` will expose this through the `decrypt` method in `crates/valv/src/main.rs` (currently unimplemented). +3. **Decryption**: Implemented in `crates/valv/src/lib.rs` in the `decrypt()` function of the `ValvAPI` trait. The `API` struct in `crates/valv/src/api/server.rs` exposes this functionality. 4. **Re-encryption**: Not explicitly implemented yet, but the foundation exists within the encryption and decryption functions. ### Components The implementation separates the following components: + - Tenant - Keystore - Database @@ -82,6 +85,3 @@ While the current implementation incorporates key concepts from the thesis, ther It's important to note that while the implemented protocol is based on the verified model from the thesis, the current implementation may not yet fully adhere to all the requirements verified in the thesis. Further work is needed to ensure that the implementation preserves all the properties proven in the formal verification. As development continues, this documentation should be updated to reflect progress and maintain traceability to the thesis. Any deviations from or extensions to the verified design should be carefully considered and documented. - - - diff --git a/SPIN-verification/model.pml b/formal-verification/model.pml similarity index 100% rename from SPIN-verification/model.pml rename to formal-verification/model.pml