tls: update CBMC proofs

firedancer-io · Jan 26, 2024 · 851b524 · 851b524
1 parent d17e587
commit 851b524
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 0 deletions.
diff --git a/verification/proofs/tls/client_hs/Makefile b/verification/proofs/tls/client_hs/Makefile
@@ -10,6 +10,7 @@ PROOF_SOURCES += $(PROOF_STUB)/fd_ed25519.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_aes.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_sha.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_tls_proto.c
+PROOF_SOURCES += $(PROOF_STUB)/fd_tls_sign.c
 PROJECT_SOURCES = $(SRCDIR)/tango/tls/fd_tls.c
 
 CBMC_OBJECT_BITS = 16

diff --git a/verification/proofs/tls/client_hs/fd_tls_client_hs_harness.c b/verification/proofs/tls/client_hs/fd_tls_client_hs_harness.c
@@ -68,6 +68,14 @@ tls_quic_tp_peer( void  *       handshake,
   __CPROVER_r_ok( quic_tp, quic_tp_sz );
 }
 
+/* From stubs/fd_tls_sign.c */
+
+extern void * fd_tls_sign_ctx_stub;
+extern void
+fd_tls_sign_fn_stub( void *        ctx,
+                     uchar *       sig,
+                     uchar const * payload );
+
 void
 harness( void ) {
   fd_tls_t * tls = fd_tls_join( fd_tls_new( malloc( fd_tls_footprint() ) ) );
@@ -79,6 +87,10 @@ harness( void ) {
   };
   tls->secrets_fn = tls_secrets;
   tls->sendmsg_fn = tls_sendmsg;
+  tls->sign = (fd_tls_sign_t) {
+    .ctx     = fd_tls_sign_ctx_stub,
+    .sign_fn = fd_tls_sign_fn_stub
+  };
   if( tls->quic ) {
     tls->quic_tp_self_fn = tls_quic_tp_self;
     tls->quic_tp_peer_fn = tls_quic_tp_peer;

diff --git a/verification/proofs/tls/server_hs/Makefile b/verification/proofs/tls/server_hs/Makefile
@@ -10,6 +10,7 @@ PROOF_SOURCES += $(PROOF_STUB)/fd_ed25519.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_aes.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_sha.c
 PROOF_SOURCES += $(PROOF_STUB)/fd_tls_proto.c
+PROOF_SOURCES += $(PROOF_STUB)/fd_tls_sign.c
 PROJECT_SOURCES = $(SRCDIR)/tango/tls/fd_tls.c
 
 CBMC_OBJECT_BITS = 16

diff --git a/verification/proofs/tls/server_hs/fd_tls_server_hs_harness.c b/verification/proofs/tls/server_hs/fd_tls_server_hs_harness.c
@@ -68,6 +68,14 @@ tls_quic_tp_peer( void  *       handshake,
   __CPROVER_r_ok( quic_tp, quic_tp_sz );
 }
 
+/* From stubs/fd_tls_sign.c */
+
+extern void * fd_tls_sign_ctx_stub;
+extern void
+fd_tls_sign_fn_stub( void *        ctx,
+                     uchar *       sig,
+                     uchar const * payload );
+
 void
 harness( void ) {
   fd_tls_t * tls = fd_tls_join( fd_tls_new( malloc( fd_tls_footprint() ) ) );
@@ -79,6 +87,10 @@ harness( void ) {
   };
   tls->secrets_fn = tls_secrets;
   tls->sendmsg_fn = tls_sendmsg;
+  tls->sign = (fd_tls_sign_t) {
+    .ctx     = fd_tls_sign_ctx_stub,
+    .sign_fn = fd_tls_sign_fn_stub
+  };
   if( tls->quic ) {
     tls->quic_tp_self_fn = tls_quic_tp_self;
     tls->quic_tp_peer_fn = tls_quic_tp_peer;

diff --git a/verification/stubs/fd_tls_proto.c b/verification/stubs/fd_tls_proto.c
@@ -166,3 +166,11 @@ fd_tls_encode_cert_verify( fd_tls_cert_verify_t const * in,
                            ulong                       wire_sz ) {
   return generic_encode( in, sizeof(fd_tls_cert_verify_t), wire, wire_sz );
 }
+
+long
+fd_tls_encode_cert_x509( uchar const * x509,
+                         ulong         x509_sz,
+                         uchar *       wire,
+                         ulong         wire_sz ) {
+  return generic_encode( x509, x509_sz, wire, wire_sz );
+}
diff --git a/verification/stubs/fd_tls_sign.c b/verification/stubs/fd_tls_sign.c
@@ -0,0 +1,14 @@
+#include <tango/tls/fd_tls.h>
+
+/* fd_tls_sign_fn_stub implements the fd_tls_sign_fn_t callback. */
+
+extern void * fd_tls_sign_ctx_stub;
+
+void
+fd_tls_sign_fn_stub( void *        ctx,
+                     uchar *       sig,
+                     uchar const * payload ) {
+  __CPROVER_assert( ctx == fd_tls_sign_ctx_stub, "invalid context" );
+  __CPROVER_r_ok( payload, 130UL );
+  __CPROVER_havoc_slice( sig, 64UL );
+}