feat: introduce Std.Internal.SSL.Context

script/prepare-llvm-macos.sh

@@ -19,7 +19,7 @@ else
   ln -s llvm llvm-host
 fi
 SDK=$(xcrun --show-sdk-path)
-mkdir -p stage1/{bin,lib/libc,include/clang}
+mkdir -p stage1/{bin,lib/libc,lib/frameworks,include/clang}
 CP="gcp -d"  # preserve symlinks
 # a C compiler!
 gcp -L llvm/bin/clang stage1/bin/
@@ -51,11 +51,22 @@ if [[ -L llvm-host ]]; then
   gcp $GMP/lib/libgmp.a stage1/lib/
   gcp $LIBUV/lib/libuv.a stage1/lib/
   gcp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lssl -lcrypto'"
+  # macOS reads its trust store from the Keychain via the Security framework (and its
+  # CoreFoundation dependency). The standalone toolchain links with `--sysroot ROOT`, which does
+  # not search the host SDK, so bundle the framework stubs here just like libSystem above. We also
+  # bundle `libobjc.A.tbd` (under `usr/lib`, where the re-export's install name resolves) because
+  # CoreFoundation re-exports it.
+  for fw in CoreFoundation Security; do
+    mkdir -p stage1/lib/frameworks/$fw.framework
+    gcp -L $SDK/System/Library/Frameworks/$fw.framework/$fw.tbd stage1/lib/frameworks/$fw.framework/
+  done
+  mkdir -p stage1/usr/lib
+  gcp -L $SDK/usr/lib/libobjc.A.tbd stage1/usr/lib/
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lssl -lcrypto -framework CoreFoundation -framework Security'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
 fi
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/libc -F ROOT/lib/frameworks -fuse-ld=lld'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

src/CMakeLists.txt

@@ -426,6 +426,17 @@ if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
   string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
   if(NOT LEAN_STANDALONE)
     string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
+    # macOS reads its trust store from the Keychain via the Security framework rather than from
+    # OpenSSL's default certificate paths, so link it (and its CoreFoundation dependency).
+    if(CMAKE_SYSTEM_NAME MATCHES "Darwin")
+      string(APPEND LEAN_EXTRA_LINKER_FLAGS " -framework CoreFoundation -framework Security")
+    endif()
+
+    # OpenSSL's Windows trust store loader reaches the `ROOT` store through the CryptoAPI in
+    # crypt32, which a static libcrypto expects its consumer to provide.
+    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+      string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32")
+    endif()
   endif()
 endif()
 

src/Std/Internal.lean

@@ -11,6 +11,7 @@ public import Std.Http
 public import Std.Internal.ForIn
 public import Std.Internal.Parsec
 public import Std.Internal.UV
+public import Std.Internal.SSL
 
 @[expose] public section
 

src/Std/Internal/SSL.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+prelude
+public import Std.Internal.SSL.Context

src/Std/Internal/SSL/Context.lean

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+prelude
+public import Init.System.IO
+
+/-!
+OpenSSL context types for server and client TLS sessions. Contexts configure the TLS method,
+certificate/key, peer-verification mode, and protocol options shared across all sessions created
+from the same context.
+
+For every context, session tickets and TLS compression are disabled, renegotiation is refused, and
+TLS 1.2 is the minimum version. A server built here therefore offers no session resumption; a client
+does not resume either, since resuming additionally requires selecting a session per connection,
+which the session layer never does.
+
+A context settles who is trusted, not who is being talked to: nothing here checks that a peer
+certificate matches the host it came from. That check belongs to the session layer, which binds a
+hostname per connection.
+
+The certificate, key and CA material passed to these constructors is refused outright when it is
+encrypted, rather than prompted for, so no constructor can block on a terminal asking for a
+passphrase. Material reached through `SSL_CERT_FILE` or `SSL_CERT_DIR` is read by OpenSSL with an
+empty passphrase instead: it cannot prompt either, but an encrypted block whose passphrase happens
+to be empty is decrypted and trusted there, where the same bytes in a `PEM.file` would be rejected.
+-/
+
+public section
+
+namespace Std.Internal.SSL
+
+/--
+PEM-encoded material, named either by the path of a file holding it or by its bytes directly.
+
+The two differ in how a NUL byte is treated. A path is passed to the OS as a C string, so an
+embedded NUL is rejected outright; `PEM.text` is read with an explicit length, so a NUL is ordinary
+input the PEM parser then has to make sense of.
+-/
+inductive PEM where
+
+  /--
+  Read the PEM from the file at `path`.
+  -/
+  | file (path : String)
+
+  /--
+  Take `contents` as the PEM bytes themselves.
+  -/
+  | text (contents : String)
+
+namespace PEM
+
+@[inline] private def bytes : PEM → String
+  | .file path => path
+  | .text contents => contents
+
+@[inline] private def isFile : PEM → Bool
+  | .file _ => true
+  | .text _ => false
+
+end PEM
+
+private opaque ContextServerImpl : NonemptyType.{0}
+
+/--
+Server-side TLS context (`SSL_CTX` configured with `TLS_server_method`).
+-/
+def Context.Server : Type := ContextServerImpl.type
+
+instance : Nonempty Context.Server := ContextServerImpl.property
+
+private opaque ContextClientImpl : NonemptyType.{0}
+
+/--
+Client-side TLS context (`SSL_CTX` configured with `TLS_client_method`).
+-/
+def Context.Client : Type := ContextClientImpl.type
+
+instance : Nonempty Context.Client := ContextClientImpl.property
+
+namespace Context.Server
+
+/--
+The credentials a server presents. Both fields are required: a server that cannot prove who it is
+has nothing to offer a client.
+-/
+structure Config where
+  /--
+  The leaf certificate followed by any intermediates. The whole chain is sent, so clients can build
+  a path to a trusted root.
+  -/
+  cert : PEM
+  /-- An unencrypted private key matching the leaf in `cert`. -/
+  key : PEM
+
+@[extern "lean_ssl_ctx_mk_server"]
+private opaque mkImpl (cert : @& String) (certIsFile : Bool) (key : @& String) (keyIsFile : Bool) :
+    IO Context.Server
+
+/--
+Creates a server-side TLS context from the given certificate chain and private key. The server
+presents its certificate but does not authenticate the client (no mutual TLS).
+
+The certificate is parsed but not validated against the clock: an expired certificate loads here and
+is rejected by the peer at handshake time. A key that does not match the leaf certificate is
+rejected, as is an encrypted key — decrypting one would mean asking for a passphrase.
+-/
+def mk (cfg : Config) : IO Context.Server :=
+  mkImpl cfg.cert.bytes cfg.cert.isFile cfg.key.bytes cfg.key.isFile
+
+end Server
+
+namespace Client
+
+/--
+Which anchors a client trusts, and whether it checks the peer against them at all.
+-/
+structure Config where
+  /--
+  Trust anchors supplied by the caller, trusted in addition to the platform anchors or — with
+  `trustSystemRoots := false` — instead of them. `none` supplies no anchors of its own.
+
+  Private key and CRL entries in the material are ignored, so a bundle may hold them; no revocation
+  checking is performed. Material yielding no certificate at all is rejected.
+  -/
+  ca : Option PEM := none
+  /--
+  Whether to verify that the peer certificate chains to a trusted anchor. `false` disables
+  verification entirely, and neither `ca` nor the platform anchors are then consulted. This cannot
+  be undone: a context built this way can never be made to verify.
+  -/
+  verifyPeer : Bool := true
+  /--
+  Whether the platform default trust anchors are trusted.
+
+  With `true`, connections to public HTTPS servers work out of the box. Which anchors those are is
+  platform-specific: the Keychain on macOS, the `ROOT` store on Windows, OpenSSL's configured paths
+  elsewhere. `SSL_CERT_FILE` and `SSL_CERT_DIR` are honoured on every platform, and are consulted
+  afresh for every context. On macOS the Keychain is read once per process, since doing so costs
+  around a tenth of a second, so a root added to it after the first context is built is not picked
+  up until the process restarts. The per-certificate trust settings decide, so a root added locally
+  (as `mkcert` and `security add-trusted-cert` do) is trusted and one explicitly denied is not; a
+  setting that applies only to a named host, key usage, or application grants no trust, since an
+  anchor cannot carry that restriction. OpenSSL's own bundle is not merged on top of the Keychain,
+  as it would reinstate the roots those settings turned away; it is read only when the Keychain
+  yields no anchor at all. `SSL_CERT_FILE` and `SSL_CERT_DIR` name locations of their own, which are
+  read in addition to the Keychain and do not drag OpenSSL's bundle in with them.
+
+  With `false` none of that is consulted, environment variables included, and only `ca` is trusted.
+  -/
+  trustSystemRoots : Bool := true
+  /--
+  Whether a certificate in the trust store may anchor a chain without being self-signed itself.
+
+  With `false`, the default, a chain is accepted only once it reaches a self-signed certificate, so
+  an intermediate CA cannot serve as a trust anchor. Supplying nothing but intermediates as `ca`
+  while also excluding the platform anchors then describes a context that could never verify
+  anything, and is rejected outright rather than left to fail at every handshake. Alongside the
+  platform anchors an intermediate is merely redundant, so it passes.
+
+  With `true` any certificate in the store anchors a chain, which is what pinning to an intermediate
+  rather than to the root above it requires.
+  -/
+  allowPartialChain : Bool := false
+
+@[extern "lean_ssl_ctx_mk_client"]
+private opaque mkImpl (ca : @& String) (caIsFile : Bool) (hasCA : Bool) (verifyPeer : Bool)
+    (trustSystemRoots : Bool) (allowPartialChain : Bool) : IO Context.Client
+
+/--
+Creates a client-side TLS context trusting the anchors named by `cfg`.
+
+Pinning against a specific CA is `{ ca := some ca, trustSystemRoots := false }`: a certificate
+issued by any other authority, public roots included, is then rejected. `ca` must supply at least
+one certificate in that case, since a verifying context with no anchor at all could never complete a
+handshake; that combination is refused here rather than at connection time.
+
+A trusted CA has to be self-signed unless `allowPartialChain` says otherwise, since a chain is only
+accepted once it reaches a self-signed certificate. Pinning to nothing but intermediates is refused
+here rather than failing at every handshake.
+
+Verifying the peer proves the certificate chains to a trusted anchor; it does **not** prove the
+certificate belongs to the host being connected to. Binding a hostname is the session layer's job.
+-/
+def mk (cfg : Config := {}) : IO Context.Client :=
+  match cfg.ca with
+  | none => mkImpl "" false false cfg.verifyPeer cfg.trustSystemRoots cfg.allowPartialChain
+  | some ca =>
+    mkImpl ca.bytes ca.isFile true cfg.verifyPeer cfg.trustSystemRoots cfg.allowPartialChain
+
+end Client
+end Context
+end Std.Internal.SSL
+
+end

src/runtime/CMakeLists.txt

@@ -84,6 +84,8 @@ set(
   uv/system.cpp
   uv/signal.cpp
   openssl.cpp
+  openssl/context.cpp
+  openssl/trust_store.cpp
 )
 
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})

src/runtime/init_module.cpp

@@ -14,6 +14,8 @@ Author: Leonardo de Moura
 #include "runtime/mutex.h"
 #include "runtime/init_module.h"
 #include "runtime/libuv.h"
+#include "runtime/openssl.h"
+#include "runtime/openssl/context.h"
 
 namespace lean {
 // idempotent as it may be called both by the generated `main` and, via `lean_initialize`,
@@ -31,13 +33,16 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_mutex();
     initialize_process();
     initialize_stack_overflow();
+    initialize_openssl();
+    initialize_openssl_context();
     initialize_libuv();
 }
 void initialize_runtime_module() {
     lean_initialize_runtime_module();
 }
 void finalize_runtime_module() {
     finalize_stack_overflow();
+    finalize_openssl();
     finalize_process();
     finalize_mutex();
     finalize_thread();

src/runtime/openssl.cpp

@@ -7,6 +7,7 @@ Author: Sofia Rodrigues
 
 #ifndef LEAN_EMSCRIPTEN
 #include <openssl/opensslv.h>
+#include <openssl/crypto.h>
 #include <openssl/err.h>
 #include <openssl/ssl.h>
 
@@ -17,10 +18,25 @@ void initialize_openssl() {
 
 void finalize_openssl() {}
 
+bool ensure_openssl_initialized() {
+    // `OPENSSL_INIT_NO_ATEXIT` is the load-bearing flag. By default OpenSSL registers
+    // `atexit(OPENSSL_cleanup)`, which tears down global state — among it the ENGINE lock that
+    // `SSL_CTX_new` reads — while other threads may still be inside OpenSSL, dereferencing the
+    // freed lock. Lean hands work to a thread pool that can outlive `main`, so that handler
+    // must not be installed. Nothing then frees OpenSSL's globals, which is intended: they stay
+    // reachable from static storage for the life of the process.
+    static const bool ok = OPENSSL_init_ssl(OPENSSL_INIT_NO_ATEXIT, nullptr) == 1;
+
+    return ok;
+}
+
 }
 
 extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
-    return lean_unsigned_to_nat(OPENSSL_VERSION_NUMBER);
+    // The linked library rather than the headers it was compiled against, so a Lean binary running
+    // against an upgraded shared OpenSSL reports what it actually loaded (as `lean_libuv_version`
+    // does for libuv).
+    return lean_unsigned_to_nat(OpenSSL_version_num());
 }
 
 #else

src/runtime/openssl.h

@@ -6,4 +6,16 @@ Author: Sofia Rodrigues
 #pragma once
 #include <lean/lean.h>
 
-extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);
+namespace lean {
+void initialize_openssl();
+void finalize_openssl();
+
+#ifndef LEAN_EMSCRIPTEN
+// Initializes OpenSSL on first call, returning whether the library is usable. Deliberately lazy: a
+// program that never opens a TLS connection never loads OpenSSL's providers. Every entry point that
+// touches OpenSSL must call this first.
+bool ensure_openssl_initialized();
+#endif
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);