feat: introduce Std.Internal.SSL.Session

src/Std/Internal/SSL.lean

@@ -6,3 +6,4 @@ Authors: Sofia Rodrigues
 module
 prelude
 public import Std.Internal.SSL.Context
+public import Std.Internal.SSL.Session

src/runtime/CMakeLists.txt

@@ -85,6 +85,7 @@ set(
   uv/signal.cpp
   openssl.cpp
   openssl/context.cpp
+  openssl/session.cpp
   openssl/ssl_error.cpp
   openssl/trust_store.cpp
 )

src/runtime/init_module.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "runtime/libuv.h"
 #include "runtime/openssl.h"
 #include "runtime/openssl/context.h"
+#include "runtime/openssl/session.h"
 
 namespace lean {
 // idempotent as it may be called both by the generated `main` and, via `lean_initialize`,
@@ -35,6 +36,7 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_stack_overflow();
     initialize_openssl();
     initialize_openssl_context();
+    initialize_openssl_session();
     initialize_libuv();
 }
 void initialize_runtime_module() {

src/runtime/openssl/context.cpp

@@ -70,7 +70,11 @@ static void configure_ctx_options(SSL_CTX * ctx) {
 
         // Disables RFC 5077 session tickets in TLS 1.2. In TLS 1.3 it only downgrades them to the
         // stateful form; the call below is what stops those being sent.
-        SSL_OP_NO_TICKET
+        SSL_OP_NO_TICKET |
+
+        // TLS 1.2 and below only; TLS 1.3 has no compression. A libssl built against zlib and
+        // running at security level 1 would otherwise negotiate it, which is CRIME.
+        SSL_OP_NO_COMPRESSION
     );
 
     // Without this a TLS 1.3 server still puts two NewSessionTickets on the wire per connection.
@@ -355,23 +359,6 @@ static lean_obj_res mk_client_ctx_checked(b_obj_arg ca, uint8_t ca_is_file, uint
     return mk_client_ctx(verify_peer, trust_system_roots, allow_partial_chain, has_ca != 0, ca_src);
 }
 
-// Runs a constructor behind the two guards every entry point needs: OpenSSL initialized before any
-// `ERR_*` call can register `atexit(OPENSSL_cleanup)` behind `OPENSSL_INIT_NO_ATEXIT`'s back, and no
-// C++ exception escaping into Lean-generated code.
-template<typename F>
-static lean_obj_res ssl_entry_point(F && build) {
-    try {
-        if (!ensure_openssl_initialized()) {
-            return lean_io_result_mk_error(lean_mk_io_user_error(
-                mk_string("OPENSSL_init_ssl failed")));
-        }
-
-        return build();
-    } catch (std::exception & ex) {
-        return lean_io_result_mk_error(lean_mk_io_user_error(mk_string(ex.what())));
-    }
-}
-
 /* Std.Internal.SSL.Context.Server.mkImpl (cert : @& String) (certIsFile : Bool) (key : @& String) (keyIsFile : Bool) : IO Context.Server */
 extern "C" LEAN_EXPORT lean_obj_res lean_ssl_ctx_mk_server(b_obj_arg cert, uint8_t cert_is_file, b_obj_arg key, uint8_t key_is_file) {
     return ssl_entry_point([&] { return mk_server_ctx(cert, cert_is_file, key, key_is_file); });