Merge branch 'main' into ecdsa_sigalg

.github/workflows/proof_ci.yaml

@@ -1,6 +1,6 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
-# CBMC starter kit 2.9
+# CBMC starter kit 2.10
 name: Run CBMC proofs
 on:
   push:
@@ -38,11 +38,11 @@ jobs:
       - name: Parse config file
         run: |
           CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml'
-          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version proofs-dir run-cbmc-proofs-command; do
+          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version z3-version bitwuzla-version proofs-dir run-cbmc-proofs-command; do
             VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _)
             echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV
           done
-      - name: Ensure CBMC, CBMC viewer, Litani versions have been specified
+      - name: Ensure CBMC, CBMC viewer, Litani, Z3, Bitwuzla versions have been specified
         shell: bash
         run: |
           should_exit=false
@@ -58,6 +58,22 @@ jobs:
             echo "You must specify a Litani version (e.g. 'latest' or '1.27.0')"
             should_exit=true
           fi
+          if [ "${{ env.Z3_VERSION }}" == "" ]; then
+            echo "You must specify a Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.Z3_VERSION }}" == "latest" ]; then
+            echo "Z3 latest not supported at this time. You must specify an exact Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "" ]; then
+            echo "You must specify a Bitwuzla version (e.g. '0.5.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "latest" ]; then
+            echo "Bitwuzla latest not supported at this time. You must specify an exact version (e.g. '0.5.0')"
+            should_exit=true
+          fi
           if [[ "$should_exit" == true ]]; then exit 1; fi
       - name: Install latest CBMC
         if: ${{ env.CBMC_VERSION == 'latest' }}
@@ -84,15 +100,15 @@ jobs:
         run: |
           CBMC_VIEWER_REL="https://api.github.com/repos/model-checking/cbmc-viewer/releases/latest"
           CBMC_VIEWER_VERSION=$(curl -s $CBMC_VIEWER_REL --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r .name | sed  's/viewer-//')
-          pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
+          sudo pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
       - name: Install CBMC viewer ${{ env.CBMC_VIEWER_VERSION }}
         if: ${{ env.CBMC_VIEWER_VERSION != 'latest' }}
         shell: bash
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes \
             build-essential universal-ctags
-          pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
+          sudo pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
       - name: Install latest Litani
         if: ${{ env.LITANI_VERSION == 'latest' }}
         shell: bash
@@ -114,6 +130,37 @@ jobs:
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes ./litani.deb
           rm ./litani.deb
+      - name: Install Z3 ${{ env.Z3_VERSION }}
+        if: ${{ env.Z3_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          curl -o z3.zip -L \
+            https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-2.31.zip
+          sudo apt-get install --no-install-recommends --yes unzip
+          unzip z3.zip
+          cd z3-${{ env.Z3_VERSION }}-x64-glibc-2.31/bin \
+            && echo "Adding $(pwd) to PATH for Z3" \
+            && echo "$(pwd)" >> $GITHUB_PATH
+          rm ../../z3.zip
+      - name: Build and Install Bitwuzla ${{ env.BITWUZLA_VERSION }}
+        if: ${{ env.BITWUZLA_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          echo "Installing Bitwuzla dependencies"
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes libgmp-dev cmake
+          sudo pip3 install meson
+          echo "Building Bitwuzla"
+          BITWUZLA_TAG_NAME=${{ env.BITWUZLA_VERSION }}
+          git clone https://github.com/bitwuzla/bitwuzla.git \
+            && cd bitwuzla \
+            && git checkout $BITWUZLA_TAG_NAME \
+            && ./configure.py \
+            && cd build \
+            && ninja;
+          cd src/main \
+            && echo "Adding $(pwd) to PATH for Bitwuzla" \
+            && echo "$(pwd)" >> $GITHUB_PATH
       - name: Install ${{ env.KISSAT_TAG }} kissat
         if: ${{ env.KISSAT_TAG != '' }}
         shell: bash

.github/workflows/proof_ci_resources/config.yaml

@@ -1,7 +1,9 @@
 cadical-tag: latest
-cbmc-version: "5.95.1"
+cbmc-version: "6.1.0"
 cbmc-viewer-version: latest
 kissat-tag: latest
 litani-version: latest
+z3-version: "4.13.0"
+bitwuzla-version: "0.5.0"
 proofs-dir: tests/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py

.gitignore

@@ -21,7 +21,6 @@ tests/unit/*_test
 tests/fuzz/*_test
 tests/fuzz/*.txt
 tests/fuzz/fuzz-*.log
-tests/benchmark/*_benchmark
 bin/s2nc
 bin/s2nd
 bin/policy

CMakeLists.txt

@@ -539,26 +539,6 @@ if (BUILD_TESTING)
         target_compile_options(s2nd PRIVATE -flto)
     endif()
 
-    if(BENCHMARK)
-        find_package(benchmark REQUIRED)
-        file(GLOB BENCHMARK_SRC "tests/benchmark/*.cc")
-        file(GLOB BENCHMARK_UTILS "tests/benchmark/utils/*.cc")
-        enable_language(CXX)
-        foreach(benchmark ${BENCHMARK_SRC})
-            string(REGEX REPLACE ".+\\/(.+)\\.cc" "\\1" benchmark_name ${benchmark})
-            add_executable(${benchmark_name} ${benchmark} "bin/echo.c" "bin/common.c" ${BENCHMARK_UTILS})
-            target_include_directories(${benchmark_name} PRIVATE api)
-            target_include_directories(${benchmark_name} PRIVATE tests)
-            target_link_libraries(${benchmark_name} PUBLIC ${PROJECT_NAME} testss2n benchmark::benchmark)
-
-            # Based off the flags in tests/benchmark/Makefile
-            target_compile_options(${benchmark_name} PRIVATE -pedantic -Wall -Werror -Wunused -Wcomment -Wchar-subscripts
-                    -Wuninitialized -Wshadow -Wcast-qual -Wcast-align -Wwrite-strings -Wno-deprecated-declarations
-                    -Wno-unknown-pragmas -Wformat-security -Wno-missing-braces -fvisibility=hidden -Wno-unreachable-code
-                    -Wno-unused-but-set-variable)
-        endforeach(benchmark)
-    endif()
-
     if (S2N_INTEG_TESTS)
         find_package (Python3 COMPONENTS Interpreter Development)
         file(GLOB integv2_test_files "${PROJECT_SOURCE_DIR}/tests/integrationv2/test_*.py")

Makefile

@@ -88,10 +88,6 @@ fuzz-linux : export S2N_UNSAFE_FUZZING_MODE = 1
 fuzz-linux : bin
 	$(MAKE) -C tests fuzz
 
-.PHONY : benchmark
-benchmark: bin
-	$(MAKE) -C tests benchmark
-
 .PHONY : coverage
 coverage: run-lcov run-genhtml
 

bin/common.c

@@ -314,6 +314,9 @@ int s2n_setup_external_psk_list(struct s2n_connection *conn, char *psk_optarg_li
 
 int s2n_set_common_server_config(int max_early_data, struct s2n_config *config, struct conn_settings conn_settings, const char *cipher_prefs, const char *session_ticket_key_file_path)
 {
+    /* The s2n-tls blinding security feature is disabled for testing purposes to make debugging easier. */
+    GUARD_EXIT(s2n_config_set_max_blinding_delay(config, 0), "Error setting blinding delay");
+
     GUARD_EXIT(s2n_config_set_server_max_early_data_size(config, max_early_data), "Error setting max early data");
 
     GUARD_EXIT(s2n_config_add_dhparams(config, dhparams), "Error adding DH parameters");

bin/s2nc.c

@@ -33,6 +33,7 @@
 #include "api/unstable/npn.h"
 #include "api/unstable/renegotiate.h"
 #include "common.h"
+#include "crypto/s2n_libcrypto.h"
 #include "error/s2n_errno.h"
 #include "tls/s2n_connection.h"
 
@@ -76,6 +77,9 @@ const char default_trusted_cert[] =
 void usage()
 {
     /* clang-format off */
+    fprintf(stderr, "s2nc is an s2n-tls client testing utility.\n");
+    fprintf(stderr, "It is not intended for production use.\n");
+    fprintf(stderr, "\n");
     fprintf(stderr, "usage: s2nc [options] host [port]\n");
     fprintf(stderr, " host: hostname or IP address to connect to\n");
     fprintf(stderr, " port: port to connect to\n");
@@ -201,6 +205,9 @@ static void setup_s2n_config(struct s2n_config *config, const char *cipher_prefs
         exit(1);
     }
 
+    /* The s2n-tls blinding security feature is disabled for testing purposes to make debugging easier. */
+    GUARD_EXIT(s2n_config_set_max_blinding_delay(config, 0), "Error setting blinding delay");
+
     GUARD_EXIT(s2n_config_set_cipher_preferences(config, cipher_prefs), "Error setting cipher prefs");
 
     GUARD_EXIT(s2n_config_set_status_request_type(config, type), "OCSP validation is not supported by the linked libCrypto implementation. It cannot be set.");
@@ -585,6 +592,7 @@ int main(int argc, char *const *argv)
     }
 
     GUARD_EXIT(s2n_init(), "Error running s2n_init()");
+    printf("libcrypto: %s\n", s2n_libcrypto_get_version_name());
 
     if ((r = getaddrinfo(host, port, &hints, &ai_list)) != 0) {
         fprintf(stderr, "error: %s\n", gai_strerror(r));

bin/s2nd.c

@@ -34,6 +34,7 @@
 #include "api/s2n.h"
 #include "api/unstable/npn.h"
 #include "common.h"
+#include "crypto/s2n_libcrypto.h"
 #include "utils/s2n_safety.h"
 
 #define MAX_CERTIFICATES 50
@@ -138,6 +139,9 @@ static char default_private_key[] =
 void usage()
 {
     /* clang-format off */
+    fprintf(stderr, "s2nd is an s2n-tls server testing utility.\n");
+    fprintf(stderr, "It is not intended for production use.\n");
+    fprintf(stderr, "\n");
     fprintf(stderr, "usage: s2nd [options] host port\n");
     fprintf(stderr, " host: hostname or IP address to listen on\n");
     fprintf(stderr, " port: port to listen on\n");
@@ -562,6 +566,7 @@ int main(int argc, char *const *argv)
     }
 
     GUARD_EXIT(s2n_init(), "Error running s2n_init()");
+    printf("libcrypto: %s\n", s2n_libcrypto_get_version_name());
 
     printf("Listening on %s:%s\n", host, port);
 

bindings/rust/s2n-tls-hyper/Cargo.toml

@@ -7,13 +7,14 @@ edition = "2021"
 rust-version = "1.63.0"
 repository = "https://github.com/aws/s2n-tls"
 license = "Apache-2.0"
+publish = false
 
 [features]
 default = []
 
 [dependencies]
-s2n-tls = { version = "=0.2.9", path = "../s2n-tls" }
-s2n-tls-tokio = { version = "=0.2.9", path = "../s2n-tls-tokio" }
+s2n-tls = { version = "=0.3.0", path = "../s2n-tls" }
+s2n-tls-tokio = { version = "=0.3.0", path = "../s2n-tls-tokio" }
 hyper = { version = "1" }
 hyper-util = { version = "0.1", features = ["client-legacy", "tokio", "http1"] }
 tower-service = { version = "0.3" }

bindings/rust/s2n-tls-sys/templates/Cargo.template

@@ -1,7 +1,7 @@
 [package]
 name = "s2n-tls-sys"
 description = "A C99 implementation of the TLS/SSL protocols"
-version = "0.2.9"
+version = "0.3.0"
 authors = ["AWS s2n"]
 edition = "2021"
 rust-version = "1.63.0"

bindings/rust/s2n-tls-tokio/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "s2n-tls-tokio"
 description = "An implementation of TLS streams for Tokio built on top of s2n-tls"
-version = "0.2.9"
+version = "0.3.0"
 authors = ["AWS s2n"]
 edition = "2021"
 rust-version = "1.63.0"
@@ -15,7 +15,7 @@ default = []
 errno = { version = "0.3" }
 libc = { version = "0.2" }
 pin-project-lite = { version = "0.2" }
-s2n-tls = { version = "=0.2.9", path = "../s2n-tls" }
+s2n-tls = { version = "=0.3.0", path = "../s2n-tls" }
 tokio = { version = "1", features = ["net", "time"] }
 
 [dev-dependencies]