Merge branch 'main' into docs_pq

.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

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

@@ -13,8 +13,8 @@ publish = false
 default = []
 
 [dependencies]
-s2n-tls = { version = "=0.2.10", path = "../s2n-tls" }
-s2n-tls-tokio = { version = "=0.2.10", 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.10"
+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.10"
+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.10", path = "../s2n-tls" }
+s2n-tls = { version = "=0.3.0", path = "../s2n-tls" }
 tokio = { version = "1", features = ["net", "time"] }
 
 [dev-dependencies]

bindings/rust/s2n-tls-tokio/src/lib.rs

@@ -24,6 +24,10 @@ use tokio::{
     time::{sleep, Duration, Sleep},
 };
 
+// TODO use the version from s2n_quic_core
+mod task;
+use task::waker::debug_assert_contract as debug_assert_waker_contract;
+
 macro_rules! ready {
     ($x:expr) => {
         match $x {
@@ -105,37 +109,39 @@ where
     type Output = Result<(), Error>;
 
     fn poll(mut self: Pin<&mut Self>, ctx: &mut Context<'_>) -> Poll<Self::Output> {
-        // Retrieve a result, either from the stored error
-        // or by polling Connection::poll_negotiate().
-        // Connection::poll_negotiate() only completes once,
-        // regardless of how often this method is polled.
-        let result = match self.error.take() {
-            Some(err) => Err(err),
-            None => {
-                let handshake_poll = self.tls.with_io(ctx, |context| {
-                    let conn = context.get_mut().as_mut();
-                    conn.poll_negotiate().map(|r| r.map(|_| ()))
-                });
-                ready!(handshake_poll)
-            }
-        };
-        // If the result isn't a fatal error, return it immediately.
-        // Otherwise, poll Connection::poll_shutdown().
-        //
-        // Shutdown is only best-effort.
-        // When Connection::poll_shutdown() completes, even with an error,
-        // we return the original Connection::poll_negotiate() error.
-        match result {
-            Ok(r) => Ok(r).into(),
-            Err(e) if e.is_retryable() => Err(e).into(),
-            Err(e) => match Pin::new(&mut self.tls).poll_shutdown(ctx) {
-                Pending => {
-                    self.error = Some(e);
-                    Pending
+        debug_assert_waker_contract(ctx, |ctx| {
+            // Retrieve a result, either from the stored error
+            // or by polling Connection::poll_negotiate().
+            // Connection::poll_negotiate() only completes once,
+            // regardless of how often this method is polled.
+            let result = match self.error.take() {
+                Some(err) => Err(err),
+                None => {
+                    let handshake_poll = self.tls.with_io(ctx, |context| {
+                        let conn = context.get_mut().as_mut();
+                        conn.poll_negotiate().map(|r| r.map(|_| ()))
+                    });
+                    ready!(handshake_poll)
                 }
-                Ready(_) => Err(e).into(),
-            },
-        }
+            };
+            // If the result isn't a fatal error, return it immediately.
+            // Otherwise, poll Connection::poll_shutdown().
+            //
+            // Shutdown is only best-effort.
+            // When Connection::poll_shutdown() completes, even with an error,
+            // we return the original Connection::poll_negotiate() error.
+            match result {
+                Ok(r) => Ok(r).into(),
+                Err(e) if e.is_retryable() => Err(e).into(),
+                Err(e) => match Pin::new(&mut self.tls).poll_shutdown(ctx) {
+                    Pending => {
+                        self.error = Some(e);
+                        Pending
+                    }
+                    Ready(_) => Err(e).into(),
+                },
+            }
+        })
     }
 }
 
@@ -219,7 +225,11 @@ where
         let mut async_context = Context::from_waker(tls.conn.as_ref().waker().unwrap());
         let stream = Pin::new(&mut tls.stream);
 
-        match action(stream, &mut async_context) {
+        let res = debug_assert_waker_contract(&mut async_context, |async_context| {
+            action(stream, async_context)
+        });
+
+        match res {
             Poll::Ready(Ok(len)) => len as c_int,
             Poll::Pending => {
                 set_errno(Errno(libc::EWOULDBLOCK));
@@ -258,24 +268,26 @@ where
     /// `poll_blinding` or `poll_shutdown` (which calls `poll_blinding`
     /// internally) returns ready.
     pub fn poll_blinding(self: Pin<&mut Self>, ctx: &mut Context<'_>) -> Poll<Result<(), Error>> {
-        let tls = self.get_mut();
+        debug_assert_waker_contract(ctx, |ctx| {
+            let tls = self.get_mut();
+
+            if tls.blinding.is_none() {
+                let delay = tls.as_ref().remaining_blinding_delay()?;
+                if !delay.is_zero() {
+                    // Sleep operates at the milisecond resolution, so add an extra
+                    // millisecond to account for any stray nanoseconds.
+                    let safety = Duration::from_millis(1);
+                    tls.blinding = Some(Box::pin(sleep(delay.saturating_add(safety))));
+                }
+            };
 
-        if tls.blinding.is_none() {
-            let delay = tls.as_ref().remaining_blinding_delay()?;
-            if !delay.is_zero() {
-                // Sleep operates at the milisecond resolution, so add an extra
-                // millisecond to account for any stray nanoseconds.
-                let safety = Duration::from_millis(1);
-                tls.blinding = Some(Box::pin(sleep(delay.saturating_add(safety))));
+            if let Some(timer) = tls.blinding.as_mut() {
+                ready!(timer.as_mut().poll(ctx));
+                tls.blinding = None;
             }
-        };
 
-        if let Some(timer) = tls.blinding.as_mut() {
-            ready!(timer.as_mut().poll(ctx));
-            tls.blinding = None;
-        }
-
-        Poll::Ready(Ok(()))
+            Poll::Ready(Ok(()))
+        })
     }
 
     pub async fn apply_blinding(&mut self) -> Result<(), Error> {
@@ -362,39 +374,41 @@ where
     }
 
     fn poll_shutdown(mut self: Pin<&mut Self>, ctx: &mut Context<'_>) -> Poll<io::Result<()>> {
-        ready!(self.as_mut().poll_blinding(ctx))?;
-
-        // s2n_shutdown_send must not be called again if it errors
-        if self.shutdown_error.is_none() {
-            let result = ready!(self.as_mut().with_io(ctx, |mut context| {
-                context
-                    .conn
-                    .as_mut()
-                    .poll_shutdown_send()
-                    .map(|r| r.map(|_| ()))
-            }));
-            if let Err(error) = result {
-                self.shutdown_error = Some(error);
-                // s2n_shutdown_send only writes, so will never trigger blinding again.
-                // So we do not need to poll_blinding again after this error.
+        debug_assert_waker_contract(ctx, |ctx| {
+            ready!(self.as_mut().poll_blinding(ctx))?;
+
+            // s2n_shutdown_send must not be called again if it errors
+            if self.shutdown_error.is_none() {
+                let result = ready!(self.as_mut().with_io(ctx, |mut context| {
+                    context
+                        .conn
+                        .as_mut()
+                        .poll_shutdown_send()
+                        .map(|r| r.map(|_| ()))
+                }));
+                if let Err(error) = result {
+                    self.shutdown_error = Some(error);
+                    // s2n_shutdown_send only writes, so will never trigger blinding again.
+                    // So we do not need to poll_blinding again after this error.
+                }
+            };
+
+            let tcp_result = ready!(Pin::new(&mut self.as_mut().stream).poll_shutdown(ctx));
+
+            if let Some(err) = self.shutdown_error.take() {
+                // poll methods shouldn't be called again after returning Ready, but
+                // nothing actually prevents it so poll_shutdown should handle it.
+                // s2n_shutdown can be polled indefinitely after succeeding, but not after failing.
+                // s2n_tls::error::Error isn't cloneable, so we can't just return the same error
+                // if poll_shutdown is called again. Instead, save a different error.
+                let next_error = Error::application("Shutdown called again after error".into());
+                self.shutdown_error = Some(next_error);
+
+                Ready(Err(io::Error::from(err)))
+            } else {
+                Ready(tcp_result)
             }
-        };
-
-        let tcp_result = ready!(Pin::new(&mut self.as_mut().stream).poll_shutdown(ctx));
-
-        if let Some(err) = self.shutdown_error.take() {
-            // poll methods shouldn't be called again after returning Ready, but
-            // nothing actually prevents it so poll_shutdown should handle it.
-            // s2n_shutdown can be polled indefinitely after succeeding, but not after failing.
-            // s2n_tls::error::Error isn't cloneable, so we can't just return the same error
-            // if poll_shutdown is called again. Instead, save a different error.
-            let next_error = Error::application("Shutdown called again after error".into());
-            self.shutdown_error = Some(next_error);
-
-            Ready(Err(io::Error::from(err)))
-        } else {
-            Ready(tcp_result)
-        }
+        })
     }
 }
 

bindings/rust/s2n-tls-tokio/src/task/mod.rs

@@ -0,0 +1,4 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+pub mod waker;

bindings/rust/s2n-tls-tokio/src/task/waker.rs

@@ -0,0 +1,6 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+mod contract;
+
+pub use contract::*;