Merge pull request #148 from cryspen/artifact

Update F*, SSProve, ProVerif in sync

Author: jschneider-bensch

.github/workflows/scheduled.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: EmbarkStudios/cargo-deny-action@v1
         # TODO: Check licenses, too.
         with:

Cargo.toml

@@ -28,7 +28,8 @@ libcrux-ecdsa = { version = "0.0.3-alpha.1", features = ["rand"] }
 hax-lib = { version = "0.3" }
 
 [features]
-default = ["api", "std"]
+default = ["api", "std", "defensive"]
+defensive = []
 std = []
 test_utils = []
 secret_integers = []
@@ -78,4 +79,4 @@ default-members = [
 ]
 
 [lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(bench)'] }
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(bench)', 'cfg(hax)'] }

PROOFS.md

@@ -1,9 +1,115 @@
 # Security and Functional Correctness Proofs for Bertie
 
-The `proofs/` directory holds ProVerif F\* proofs for code compiled by
+The `proofs/` directory holds ProVerif, F\*, and SSProve proofs for code compiled by
 hax from the Bertie Rust implementation of TLS 1.3.
 
-## Correctness Proofs in F\*
+## Prerequisites
+### Setting up the hax toolchain
+We use the hax toolchain to extract proof artifacts from the Rust
+source code in `src`. To be able to reproduce this extraction for
+yourself, please follow the installation instructions for `hax`
+provided at:
+
+https://github.com/cryspen/hax?tab=readme-ov-file#installation
+
+#### `hax-driver.py`
+We use the Python 3 script `hax-driver.py` to drive extraction and
+verification of the proof artifacts, so an installation of Python 3 is
+required.
+
+### Setting up F*
+We use F* version 2025.03.25 to prove runtime safety and transcript
+unambiguity as described in section 7 of the paper submission. To
+reproduce these results for yourself, please install F* following the
+instructions at:
+
+https://fstar-lang.org/index.html#download
+
+### Setting up Rocq + SSProve
+We use Rocq version 8.18.0 and SSProve for the security proofs of the
+key schedule as described in section 5 of the paper submission. Installation
+instructions can be found at:
+
+https://rocq-prover.org/install
+https://github.com/SSProve/ssprove
+
+Furthermore, Rust core library, which is used by the Hax translation, for Rocq/SSProve is located at:
+
+https://github.com/cryspen/hax/tree/main/proof-libs
+
+### Setting up ProVerif
+We use ProVerif version 2.05 to perform protocol security analysis of the
+implementation, as described in section 6 of the paper submission.
+To be able to reproduce the analysis, please follow the installation
+instructions provided at:
+
+https://bblanche.gitlabpages.inria.fr/proverif/
+
+## Proof extraction using hax
+### F*
+To regenerate the extraction to F*, run
+```
+./hax-driver.py extract-fstar
+```
+
+### SSProve
+To regenerate the extraction for the key schedule in SSProve, run
+```
+./hax-driver.py extract-ssprove
+```
+
+To get the code running we apply a patch
+```
+patch -d extraction/ < extraction.patch
+rm -rf fextraction/
+mv extraction/ fextraction/
+```
+
+### ProVerif
+The ProVerif proofs described in section 6 of the paper submission can
+be extracted from the Rust source code by running
+```
+./hax-driver.py extract-proverif
+```
+
+This will generate the file `proofs/proverif/extraction/lib.pvl` from
+the Rust source code.
+
+## Running the Proofs
+### F*
+To run the F* proofs, run the following command:
+```
+./hax-driver.py typecheck
+```
+
+### SSProve
+First generate the Makefile from the _CoqProject
+```
+coq_makefile -f _CoqProject -o Makefile
+```
+and run `make`.
+
+### ProVerif
+To run the ProVerif analysis, as described in section 6 of the paper
+submission, run
+```
+./hax-driver.py typecheck-proverif
+```
+
+This will run the command 
+```
+proverif -lib proofs/proverif/handwritten_lib.pvl -lib
+proofs/proverif/extraction/lib.pvl proofs/proverif/extraction/analysis.pv
+```
+to start the analysis. The file `handwritten_lib.pvl` exists for
+technical reasons and contains early
+definitions of certain terms. The file `analysis.pvl` contains the
+top-level protocol process and analysis queries, as described in
+section 6 of the paper submission.
+
+## Results
+
+### Correctness Proofs in F\*
 
 Each Rust module `m` in the implementation is translated to two files:
 `M.fst` contains the functionalized F\* code compiled from Rust, and
@@ -54,31 +160,30 @@ the verified code will never create a panic. Of course, there is other
 code outside the verification boundary that may yet panic and we intend
 to expand the scope of our verification ocer time.
 
-## Security Proofs in ProVerif
+### Security Proofs in ProVerif
 
 We also prove security for the TLS 1.3 protocol code in Bertie.
 Using hax, we generate a ProVerif model of the TLS 1.3 handshake
 in `proofs/proverif/extraction/lib.pvl`.  This file contains the bulk of the extraction,
 while `analysis.pv` contains the top-level processes are set up and analysis queries.
 
-We provide patches that include changes to the extracted model (described below), which allow us to show
+We can show
 * that the modeled handshake can fully complete for both parties (as a baseline for further analysis)
-* Server authenticity, assuming neither the certificate signing key nor a potential pre-shared key have been compromised
-* Secrecy of the resulting session key under the same assumptions.
+* Server authenticity, assuming the certificate signing key is not
+  compromised 
+* Forward secrecy of the resulting session key under the same assumptions.
 
-The intended flow using the driver is to run
+### Security of the Key Schedule in SSProve
 
-./hax-driver.py extract-proverif to extract the ProVerif model to proofs/proverif/extraction.
-./hax-driver.py patch-proverif to apply the patches on the extracted model.
-./hax-driver.py typecheck-proverif to run the analysis on the patched model.
+We extract the implementation of the Key Schedule from SSProve.
+We then fix the implementation to only include the parts we need and make sure the translation is actually valid.
+This is done with a patch file to allow easier updates to the implementation.
 
-The patches are necessary for parts of the model that we cannot currently generate (properly, or at all):
-* a top-level process structure which instantiates Client and Server with ciphersuites and psk-mode configuration,
-* event definitions and analysis queries,
-* cryptographic operations and their semantics
-* tls13formats related code, especially anything that relates to concatenation primitives
+The proof for security of the key schedule is done on a specification.
+The entry functions of the specification are generalized and then instantiated with the functions in the implementation.
+We show the implemented functions fulfill some properties to be valid in the key schedule proof.
 
-Additionally, the patches introduce the following modifications:
-* A mock certificate validation, checking that the name in the certificate agrees with the name of the expected peer from the top-level process. This is because Bertie does not include full certificate validation at this time, but some binding between the name and the certificate is necessary for showing server authentication.
-* A model-side fix for the issue that is fixed on the Rust side in Correct argument order for process_psk_binder_zero_rtt #101 (until that is fixed on the Rust side).
-* The removal of all automatically generated events, since that leads to poor performance from ProVerif and is not necessary at all for the analysis (cf. [ProVerif] Emitting events unnecessarily blows up the extracted model hacspec/hax#581)
+The proof for the specification follows the proof in "Key-schedule Security for the TLS 1.3 Standard."
+We prove the Core Key Schedule Theorem by showing the main lemma D6.
+The other lemmas are a direct consequence of the correct implementation of the cryptographic primitives, which we inherit from libcrux.
+These lemmas are therefore only stated, and the proof is Admitted.

bench.md

@@ -0,0 +1,90 @@
+# Raspberry Pi 3
+```
+       _,met$$$$$gg.          jonas@raspberrypi
+    ,g$$$$$$$$$$$$$$$P.       -----------------
+  ,g$$P"     """Y$$.".        OS: Debian GNU/Linux 11 (bullseye) aarch64
+ ,$$P'              `$$$.     Host: Raspberry Pi 3 Model B Rev 1.2
+',$$P       ,ggs.     `$$b:   Kernel: 6.1.21-v8+
+`d$$'     ,$P"'   .    $$$    Uptime: 2 hours, 41 mins
+ $$P      d$'     ,    $$P    Packages: 660 (dpkg)
+ $$:      $$.   -    ,d$$'    Shell: bash 5.1.4
+ $$;      Y$b._   _,d$P'      Terminal: /dev/pts/0
+ Y$$.    `.`"Y$$$$P"'         CPU: BCM2835 (4) @ 1.200GHz
+ `$$b      "-.__              Memory: 82MiB / 909MiB
+  `Y$$
+   `Y$$.
+     `$$b.
+       `Y$$b.
+          `"Y$b._
+              `"""
+```
+
+## Client
+Client
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1:
+	Handshake: 7122 μs | 140.4094748062547 /s
+	Application: 244 μs | 63.7759811051013 MB/s
+	Message Sizes: 200, 838, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519:
+	Handshake: 4566 μs | 218.98451159470278 /s
+	Application: 245 μs | 63.71299735155773 MB/s
+	Message Sizes: 167, 805, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1:
+	Handshake: 21473 μs | 46.56802728954948 /s
+	Application: 254 μs | 61.3644019146746 MB/s
+	Message Sizes: 200, 2230, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519:
+	Handshake: 18850 μs | 53.05039006817865 /s
+	Application: 254 μs | 61.42504065826636 MB/s
+	Message Sizes: 167, 2197, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519Kyber768Draft00:
+	Handshake: 5582 μs | 179.1359595215902 /s
+	Application: 256 μs | 61.01392340465518 MB/s
+	Message Sizes: 1351, 1893, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519MlKem768:
+	Handshake: 5487 μs | 182.24313662925482 /s
+	Application: 253 μs | 61.53509645857742 MB/s
+	Message Sizes: 1351, 1892, 58 bytes
+    
+## Client Stack
+Client Stack Usage:
+===================
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1
+[Client Connect] Highest stack usage: 56.1 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519
+[Client Connect] Highest stack usage: 55.4 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1
+[Client Connect] Highest stack usage: 56.1 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519
+[Client Connect] Highest stack usage: 55.4 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519Kyber768Draft00
+[Client Connect] Highest stack usage: 78.2 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519MlKem768
+[Client Connect] Highest stack usage: 78.2 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+## Server
+Server
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1:
+	Handshake: 5481 μs | 182.43040791837637 /s
+	Application: 259 μs | 60.18269424576024 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519:
+	Handshake: 2819 μs | 354.63931635299485 /s
+	Application: 256 μs | 60.92005874557329 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1:
+	Handshake: 699193 μs | 1.430219917317012 /s
+	Application: 262 μs | 59.581248116755916 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519:
+	Handshake: 694248 μs | 1.4404070652725713 /s
+	Application: 260 μs | 60.00107706253405 MB/s

benches/client.rs

@@ -1,5 +1,6 @@
 #![allow(dead_code)]
 
+use std::collections::HashMap;
 use std::time::{Duration, Instant};
 
 use bertie::{
@@ -23,7 +24,7 @@ use bertie::{
         SignatureScheme,
     },
     tls13utils::Bytes,
-    Client, Server,
+    Client, Server, TLSkeyscheduler,
 };
 use rand::RngCore;
 
@@ -160,6 +161,9 @@ fn protocol() {
 
     for ciphersuite in CIPHERSUITES {
         let mut rng = rand::rng();
+        let mut ks: TLSkeyscheduler = TLSkeyscheduler {
+            keys: HashMap::new(),
+        };
 
         // Server
         let server_name_str = "localhost";
@@ -187,24 +191,26 @@ fn protocol() {
         for _ in 0..ITERATIONS {
             let start_time = Instant::now();
             let (client_hello, client) =
-                Client::connect(ciphersuite, &server_name, None, None, &mut rng).unwrap();
+                Client::connect(ciphersuite, &server_name, None, None, &mut rng, &mut ks).unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
             size1 += client_hello.declassify().len();
 
             let (server_hello, server_finished, server) =
-                Server::accept(ciphersuite, db.clone(), &client_hello, &mut rng).unwrap();
+                Server::accept(ciphersuite, db.clone(), &client_hello, &mut rng, &mut ks).unwrap();
             size2 += server_hello.declassify().len();
             size2 += server_finished.declassify().len();
 
             let start_time = Instant::now();
-            let (_client_msg, client) = client.read_handshake(&server_hello).unwrap();
-            let (client_msg, client) = client.read_handshake(&server_finished).unwrap();
+            let (_client_msg, client) = client.read_handshake(&server_hello, &mut ks).unwrap();
+            let (client_msg, client) = client.read_handshake(&server_finished, &mut ks).unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
             size3 += client_msg.as_ref().unwrap().declassify().len();
 
-            let server = server.read_handshake(&client_msg.unwrap()).unwrap();
+            let server = server
+                .read_handshake(&client_msg.unwrap(), &mut ks)
+                .unwrap();
 
             let application_data = payload.clone().into();