Compare commits

...

6 Commits

Author SHA1 Message Date
Sofia Rodrigues
48293bb323 fix: recv selector 2026-02-14 18:48:35 -03:00
Sofia Rodrigues
adab6fefa0 feat: openssl socket 2026-02-14 17:45:23 -03:00
Sofia Rodrigues
12796e60bf Merge branch 'master' of https://github.com/leanprover/lean4 into sofia/openssl 2026-02-14 06:22:05 -03:00
Sofia Rodrigues
9e27f77a45 feat: openssl nix 2026-01-16 19:04:34 -03:00
Sofia Rodrigues
4a26fe317d fix: remove tls 2026-01-16 18:54:46 -03:00
Sofia Rodrigues
23797245eb feat: start openssl 2026-01-15 16:10:09 -03:00
13 changed files with 1320 additions and 4 deletions

View File

@@ -24,7 +24,7 @@
stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
} ({
buildInputs = with pkgs; [
cmake gmp libuv ccache pkg-config
cmake gmp libuv ccache pkg-config openssl
llvmPackages.bintools # wrapped lld
llvmPackages.llvm # llvm-symbolizer for asan/lsan
gdb

View File

@@ -347,6 +347,35 @@ if(NOT LEAN_STANDALONE)
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
endif()
# OpenSSL
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
# Only on WebAssembly we compile OpenSSL ourselves
set(OPENSSL_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
# OpenSSL needs to be configured for Emscripten using their configuration system
ExternalProject_add(openssl
PREFIX openssl
GIT_REPOSITORY https://github.com/openssl/openssl
# Sync version with flake.nix if applicable
GIT_TAG openssl-3.0.15
CONFIGURE_COMMAND <SOURCE_DIR>/Configure linux-generic32 no-shared no-dso no-engine no-tests --prefix=<INSTALL_DIR> CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} AR=${CMAKE_AR} CFLAGS=${OPENSSL_EMSCRIPTEN_FLAGS}
BUILD_COMMAND emmake make -j
INSTALL_COMMAND emmake make install_sw
BUILD_IN_SOURCE ON)
set(OPENSSL_INCLUDE_DIR "${CMAKE_BINARY_DIR}/openssl/include")
set(OPENSSL_CRYPTO_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libcrypto.a")
set(OPENSSL_SSL_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libssl.a")
set(OPENSSL_LIBRARIES "${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY}")
else()
find_package(OpenSSL REQUIRED)
set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
endif()
include_directories(${OPENSSL_INCLUDE_DIR})
if(NOT LEAN_STANDALONE)
string(JOIN " " OPENSSL_LIBRARIES ${OPENSSL_LIBRARIES})
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES}")
endif()
# Windows SDK (for ICU)
if(CMAKE_SYSTEM_NAME MATCHES "Windows")
# Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -721,9 +750,9 @@ if(STAGE GREATER 1)
endif()
else()
add_subdirectory(runtime)
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
add_dependencies(leanrt libuv)
add_dependencies(leanrt_initial-exec libuv)
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
add_dependencies(leanrt libuv openssl)
add_dependencies(leanrt_initial-exec libuv openssl)
endif()
add_subdirectory(util)

View File

@@ -21,6 +21,9 @@ opaque maxSmallNatFn : Unit → Nat
@[extern "lean_libuv_version"]
opaque libUVVersionFn : Unit Nat
@[extern "lean_openssl_version"]
opaque openSSLVersionFn : Unit Nat
def closureMaxArgs : Nat :=
closureMaxArgsFn ()
@@ -30,4 +33,7 @@ def maxSmallNat : Nat :=
def libUVVersion : Nat :=
libUVVersionFn ()
def openSSLVersion : Nat :=
openSSLVersionFn ()
end Lean

View File

@@ -9,6 +9,7 @@ prelude
public import Std.Internal.Async
public import Std.Internal.Parsec
public import Std.Internal.UV
public import Std.Internal.SSL
@[expose] public section

View File

@@ -10,6 +10,7 @@ public import Std.Internal.Async.Basic
public import Std.Internal.Async.ContextAsync
public import Std.Internal.Async.Timer
public import Std.Internal.Async.TCP
public import Std.Internal.Async.TCP.SSL
public import Std.Internal.Async.UDP
public import Std.Internal.Async.DNS
public import Std.Internal.Async.Select
@@ -17,3 +18,4 @@ public import Std.Internal.Async.Process
public import Std.Internal.Async.System
public import Std.Internal.Async.Signal
public import Std.Internal.Async.IO
public import Std.Internal.SSL

View File

@@ -0,0 +1,417 @@
/-
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.Time
public import Std.Internal.UV.TCP
public import Std.Internal.Async.Timer
public import Std.Internal.Async.Select
public import Std.Internal.SSL
public section
namespace Std
namespace Internal
namespace IO
namespace Async
namespace TCP
namespace SSL
open Std.Net
/--
Default chunk size used by TLS I/O loops.
-/
def ioChunkSize : UInt64 := 16 * 1024
/--
Represents a TLS-enabled TCP server socket.
-/
structure Server where
private ofNative ::
native : Internal.UV.TCP.Socket
/--
Represents a TLS-enabled TCP client socket.
-/
structure Client where
private ofNative ::
native : Internal.UV.TCP.Socket
ssl : Std.Internal.SSL.Session
@[inline]
private def feedEncryptedChunk (ssl : Std.Internal.SSL.Session) (encrypted : ByteArray) : Async Unit := do
if encrypted.size == 0 then
return ()
let consumed ssl.feedEncrypted encrypted
if consumed.toNat != encrypted.size then
throw <| IO.userError s!"TLS input short write: consumed {consumed} / {encrypted.size} bytes"
@[inline]
private partial def flushEncrypted (native : Internal.UV.TCP.Socket) (ssl : Std.Internal.SSL.Session) : Async Unit := do
let out ssl.drainEncrypted
if out.size == 0 then
return ()
Async.ofPromise <| native.send #[out]
flushEncrypted native ssl
/--
Runs the TLS handshake loop until the handshake is established.
-/
private partial def handshake (native : Internal.UV.TCP.Socket) (ssl : Std.Internal.SSL.Session) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
let done ssl.handshake
flushEncrypted native ssl
if done then
return ()
let encrypted? Async.ofPromise <| native.recv? chunkSize
match encrypted? with
| none =>
throw <| IO.userError "peer closed connection before TLS handshake completed"
| some encrypted =>
feedEncryptedChunk ssl encrypted
handshake native ssl chunkSize
namespace Server
/--
Configures the shared TLS server context with PEM certificate and private key files.
-/
@[inline]
def configureContext (certFile keyFile : String) : IO Unit :=
Std.Internal.SSL.configureServerContext certFile keyFile
/--
Creates a new TLS-enabled TCP server socket.
-/
@[inline]
def mk : IO Server := do
let native Internal.UV.TCP.Socket.new
return Server.ofNative native
/--
Binds the server socket to the specified address.
-/
@[inline]
def bind (s : Server) (addr : SocketAddress) : IO Unit :=
s.native.bind addr
/--
Listens for incoming connections with the given backlog.
-/
@[inline]
def listen (s : Server) (backlog : UInt32) : IO Unit :=
s.native.listen backlog
@[inline] private def mkServerClient (native : Internal.UV.TCP.Socket) : IO Client := do
let ssl Std.Internal.SSL.Session.mkServer
return Client.ofNative native ssl
/--
Accepts an incoming TLS client connection and performs the TLS handshake.
-/
@[inline]
def accept (s : Server) (chunkSize : UInt64 := ioChunkSize) : Async Client := do
let native Async.ofPromise <| s.native.accept
let client mkServerClient native
SSL.handshake client.native client.ssl chunkSize
return client
/--
Tries to accept an incoming TLS client connection.
-/
@[inline]
def tryAccept (s : Server) : IO (Option Client) := do
let res s.native.tryAccept
let socket IO.ofExcept res
match socket with
| none => return none
| some native => return some ( mkServerClient native)
/--
Creates a `Selector` that resolves once `s` has a connection available.
-/
def acceptSelector (s : TCP.SSL.Server) : Selector Client :=
{
tryFn :=
s.tryAccept
registerFn waiter := do
let task s.native.accept
-- If we get cancelled the promise will be dropped so prepare for that
IO.chainTask (t := task.result?) fun res => do
match res with
| none => return ()
| some res =>
let lose := return ()
let win promise := do
try
let native IO.ofExcept res
let ssl Std.Internal.SSL.Session.mkServer
promise.resolve (.ok (Client.ofNative native ssl))
catch e =>
promise.resolve (.error e)
waiter.race lose win
unregisterFn := s.native.cancelAccept
}
/--
Gets the local address of the server socket.
-/
@[inline]
def getSockName (s : Server) : IO SocketAddress :=
s.native.getSockName
/--
Enables the Nagle algorithm for all client sockets accepted by this server socket.
-/
@[inline]
def noDelay (s : Server) : IO Unit :=
s.native.noDelay
/--
Enables TCP keep-alive for all client sockets accepted by this server socket.
-/
@[inline]
def keepAlive (s : Server) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val 1 := by decide) : IO Unit :=
s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
end Server
namespace Client
/--
Configures the shared TLS client context.
`caFile` may be empty to use default trust settings.
-/
@[inline]
def configureContext (caFile := "") (verifyPeer := true) : IO Unit :=
Std.Internal.SSL.configureClientContext caFile verifyPeer
/--
Creates a new TLS-enabled TCP client socket with a client-side TLS session.
-/
@[inline]
def mk : IO Client := do
let native Internal.UV.TCP.Socket.new
let ssl Std.Internal.SSL.Session.mkClient
return Client.ofNative native ssl
/--
Binds the client socket to the specified address.
-/
@[inline]
def bind (s : Client) (addr : SocketAddress) : IO Unit :=
s.native.bind addr
/--
Sets SNI server name used during the TLS handshake.
-/
@[inline]
def setServerName (s : Client) (host : String) : IO Unit :=
s.ssl.setServerName host
/--
Performs the TLS handshake on an established TCP connection.
-/
@[inline]
def handshake (s : Client) (chunkSize : UInt64 := ioChunkSize) : Async Unit :=
SSL.handshake s.native s.ssl chunkSize
/--
Connects the client socket to the given address and performs the TLS handshake.
-/
@[inline]
def connect (s : Client) (addr : SocketAddress) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
Async.ofPromise <| s.native.connect addr
s.handshake chunkSize
/--
Attempts to write plaintext data into TLS. Returns true when accepted.
Any encrypted TLS output generated is flushed to the socket.
-/
@[inline]
def write (s : Client) (data : ByteArray) : Async Bool := do
let accepted s.ssl.write data
flushEncrypted s.native s.ssl
return accepted
/--
Sends data through a TLS-enabled socket.
Fails if OpenSSL reports the write as pending additional I/O.
-/
@[inline]
def send (s : Client) (data : ByteArray) : Async Unit := do
if s.write data then
return ()
else
throw <| IO.userError "TLS write is pending additional I/O; call `recv?` or retry later"
/--
Sends multiple data buffers through the TLS-enabled socket.
-/
@[inline]
def sendAll (s : Client) (data : Array ByteArray) : Async Unit :=
data.forM (s.send ·)
/--
Receives decrypted plaintext data from TLS.
If no plaintext is immediately available, this function pulls encrypted data from TCP first.
-/
partial def recv? (s : Client) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option ByteArray) := do
match s.ssl.read? size with
| some plain =>
flushEncrypted s.native s.ssl
return some plain
| none =>
flushEncrypted s.native s.ssl
let encrypted? Async.ofPromise <| s.native.recv? chunkSize
match encrypted? with
| none =>
return none
| some encrypted =>
feedEncryptedChunk s.ssl encrypted
recv? s size chunkSize
/--
Tries to receive decrypted plaintext data without blocking.
Returns `some (some data)` if plaintext is available, `some none` if the peer closed,
or `none` if no data is ready yet.
-/
partial def tryRecv (s : Client) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option (Option ByteArray)) := do
let pending s.ssl.pendingPlaintext
if pending > 0 then
let res s.recv? size
return some res
else
let readableWaiter s.native.waitReadable
flushEncrypted s.native s.ssl
if readableWaiter.isResolved then
let encrypted? Async.ofPromise <| s.native.recv? ioChunkSize
match encrypted? with
| none =>
return none
| some encrypted =>
feedEncryptedChunk s.ssl encrypted
tryRecv s size chunkSize
else
s.native.cancelRecv
return none
/--
Feeds encrypted socket data into SSL until plaintext is pending.
Resolves the returned promise once plaintext is available. If no more socket data
is available (or the promise gets dropped), it exits without resolving.
-/
partial def waitReadable (s : Client) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
if ( s.ssl.pendingPlaintext) > 0 then
return ()
let rec go : Async Unit := do
let readable Async.ofPromise <| s.native.waitReadable
if !readable then
return ()
let encrypted? Async.ofPromise <| s.native.recv? chunkSize
match encrypted? with
| none =>
return ()
| some encrypted =>
feedEncryptedChunk s.ssl encrypted
flushEncrypted s.native s.ssl
if ( s.ssl.pendingPlaintext) > 0 then
return ()
else
go
go
/--
Creates a `Selector` that resolves once `s` has plaintext data available.
-/
def recvSelector (s : TCP.SSL.Client) (size : UInt64) : Selector (Option ByteArray) :=
{
tryFn := s.tryRecv size
registerFn waiter := do
let readableWaiter s.waitReadable.asTask
-- If we get cancelled the promise will be dropped so prepare for that
discard <| IO.mapTask (t := readableWaiter) fun res => do
match res with
| .error _ => return ()
| .ok _ =>
let lose := return ()
let win promise := do
try
-- We know that this read should not block.
let result (s.recv? size).block
promise.resolve (.ok result)
catch e =>
promise.resolve (.error e)
waiter.race lose win
unregisterFn := s.native.cancelRecv
}
/--
Shuts down the write side of the client socket.
-/
@[inline]
def shutdown (s : Client) : Async Unit :=
Async.ofPromise <| s.native.shutdown
/--
Gets the remote address of the client socket.
-/
@[inline]
def getPeerName (s : Client) : IO SocketAddress :=
s.native.getPeerName
/--
Gets the local address of the client socket.
-/
@[inline]
def getSockName (s : Client) : IO SocketAddress :=
s.native.getSockName
/--
Returns the X.509 verification result code for this TLS session.
-/
@[inline]
def verifyResult (s : Client) : IO UInt64 :=
s.ssl.verifyResult
/--
Enables the Nagle algorithm for the client socket.
-/
@[inline]
def noDelay (s : Client) : IO Unit :=
s.native.noDelay
/--
Enables TCP keep-alive with a specified delay for the client socket.
-/
@[inline]
def keepAlive (s : Client) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val 0 := by decide) : IO Unit :=
s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
end Client
end SSL
end TCP
end Async
end IO
end Internal
end Std

117
src/Std/Internal/SSL.lean Normal file
View File

@@ -0,0 +1,117 @@
/-
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.Promise
public section
namespace Std
namespace Internal
namespace SSL
private opaque SessionImpl : NonemptyType.{0}
/--
Represents an OpenSSL session backed by memory BIOs.
-/
def Session : Type := SessionImpl.type
instance : Nonempty Session := by exact SessionImpl.property
/--
Configures the shared server context with a certificate and key in PEM format.
-/
@[extern "lean_uv_ssl_configure_server_ctx"]
opaque configureServerContext (certFile : @& String) (keyFile : @& String) : IO Unit
/--
Configures the shared client context.
`caFile` may be empty to keep default trust configuration.
-/
@[extern "lean_uv_ssl_configure_client_ctx"]
opaque configureClientContext (caFile : @& String) (verifyPeer : Bool) : IO Unit
namespace Session
/--
Creates a new SSL session. Set `isServer := true` for server-side handshakes.
-/
@[extern "lean_uv_ssl_mk"]
opaque mk (isServer : Bool) : IO Session
/--
Creates a server-side SSL session.
-/
@[extern "lean_uv_ssl_mk_server"]
opaque mkServer : IO Session
/--
Creates a client-side SSL session.
-/
@[extern "lean_uv_ssl_mk_client"]
opaque mkClient : IO Session
/--
Sets SNI host name for client-side handshakes.
-/
@[extern "lean_uv_ssl_set_server_name"]
opaque setServerName (ssl : @& Session) (host : @& String) : IO Unit
/--
Gets the X.509 verify result code after handshake.
-/
@[extern "lean_uv_ssl_verify_result"]
opaque verifyResult (ssl : @& Session) : IO UInt64
/--
Runs one handshake step. Returns true when handshake is complete.
-/
@[extern "lean_uv_ssl_handshake"]
opaque handshake (ssl : @& Session) : IO Bool
/--
Attempts to write plaintext application data into SSL.
Returns true when accepted, false when OpenSSL needs more I/O first.
-/
@[extern "lean_uv_ssl_write"]
opaque write (ssl : @& Session) (data : @& ByteArray) : IO Bool
/--
Attempts to read decrypted plaintext data. Returns none when OpenSSL needs more I/O.
-/
@[extern "lean_uv_ssl_read"]
opaque read? (ssl : @& Session) (maxBytes : UInt64) : IO (Option ByteArray)
/--
Feeds encrypted TLS bytes into the SSL input BIO.
-/
@[extern "lean_uv_ssl_feed_encrypted"]
opaque feedEncrypted (ssl : @& Session) (data : @& ByteArray) : IO UInt64
/--
Drains encrypted TLS bytes from the SSL output BIO.
-/
@[extern "lean_uv_ssl_drain_encrypted"]
opaque drainEncrypted (ssl : @& Session) : IO ByteArray
/--
Returns the amount of encrypted TLS bytes currently pending in the output BIO.
-/
@[extern "lean_uv_ssl_pending_encrypted"]
opaque pendingEncrypted (ssl : @& Session) : IO UInt64
/--
Returns the amount of decrypted plaintext bytes currently buffered inside the SSL object.
-/
@[extern "lean_uv_ssl_pending_plaintext"]
opaque pendingPlaintext (ssl : @& Session) : IO UInt64
end Session
end SSL
end Internal
end Std

View File

@@ -33,6 +33,8 @@ set(
uv/dns.cpp
uv/system.cpp
uv/signal.cpp
openssl.cpp
openssl/session.cpp
)
if(USE_MIMALLOC)
list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c)

View File

@@ -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/session.h"
namespace lean {
extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -25,6 +27,8 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
initialize_mutex();
initialize_process();
initialize_stack_overflow();
initialize_openssl();
initialize_openssl_session();
initialize_libuv();
}
void initialize_runtime_module() {
@@ -32,6 +36,7 @@ void initialize_runtime_module() {
}
void finalize_runtime_module() {
finalize_stack_overflow();
finalize_openssl();
finalize_process();
finalize_mutex();
finalize_thread();

96
src/runtime/openssl.cpp Normal file
View File

@@ -0,0 +1,96 @@
/*
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues
*/
#include "runtime/openssl.h"
#include "runtime/io.h"
#include <mutex>
#ifndef LEAN_EMSCRIPTEN
#include <openssl/opensslv.h>
#include <openssl/err.h>
namespace lean {
static std::once_flag g_openssl_init_once;
static SSL_CTX * g_ssl_server_ctx = nullptr;
static SSL_CTX * g_ssl_client_ctx = nullptr;
static void configure_ctx_common(SSL_CTX * ctx) {
SSL_CTX_set_mode(ctx, SSL_MODE_AUTO_RETRY);
#ifdef SSL_OP_NO_RENEGOTIATION
SSL_CTX_clear_options(ctx, SSL_OP_NO_RENEGOTIATION);
#endif
#ifdef SSL_OP_ALLOW_CLIENT_RENEGOTIATION
SSL_CTX_set_options(ctx, SSL_OP_ALLOW_CLIENT_RENEGOTIATION);
#endif
}
static void initialize_openssl_once() {
if (OPENSSL_init_ssl(0, nullptr) != 1) {
lean_internal_panic("failed to initialize OpenSSL");
}
g_ssl_server_ctx = SSL_CTX_new(TLS_server_method());
g_ssl_client_ctx = SSL_CTX_new(TLS_client_method());
if (g_ssl_server_ctx == nullptr || g_ssl_client_ctx == nullptr) {
if (g_ssl_server_ctx != nullptr) SSL_CTX_free(g_ssl_server_ctx);
if (g_ssl_client_ctx != nullptr) SSL_CTX_free(g_ssl_client_ctx);
g_ssl_server_ctx = nullptr;
g_ssl_client_ctx = nullptr;
lean_internal_panic("failed to create OpenSSL SSL_CTX pair");
}
configure_ctx_common(g_ssl_server_ctx);
configure_ctx_common(g_ssl_client_ctx);
}
void initialize_openssl() {
std::call_once(g_openssl_init_once, initialize_openssl_once);
}
void finalize_openssl() {
if (g_ssl_server_ctx != nullptr) {
SSL_CTX_free(g_ssl_server_ctx);
g_ssl_server_ctx = nullptr;
}
if (g_ssl_client_ctx != nullptr) {
SSL_CTX_free(g_ssl_client_ctx);
g_ssl_client_ctx = nullptr;
}
}
SSL_CTX * get_openssl_server_ctx() {
initialize_openssl();
return g_ssl_server_ctx;
}
SSL_CTX * get_openssl_client_ctx() {
initialize_openssl();
return g_ssl_client_ctx;
}
}
extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
return lean_unsigned_to_nat(OPENSSL_VERSION_NUMBER);
}
#else
namespace lean {
void initialize_openssl() {}
void finalize_openssl() {}
}
extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
return lean_box(0);
}
#endif

25
src/runtime/openssl.h Normal file
View File

@@ -0,0 +1,25 @@
/*
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues
*/
#pragma once
#include <lean/lean.h>
#ifndef LEAN_EMSCRIPTEN
#include <openssl/ssl.h>
#endif
namespace lean {
void initialize_openssl();
void finalize_openssl();
#ifndef LEAN_EMSCRIPTEN
SSL_CTX * get_openssl_server_ctx();
SSL_CTX * get_openssl_client_ctx();
#endif
}
extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);

View File

@@ -0,0 +1,561 @@
/*
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues
*/
#include "runtime/openssl/session.h"
#include <climits>
#include <cstdlib>
#include <cstring>
#include <string>
#ifndef LEAN_EMSCRIPTEN
#include <openssl/err.h>
#endif
namespace lean {
#ifndef LEAN_EMSCRIPTEN
static inline lean_object * mk_ssl_error(char const * where, int ssl_err = 0) {
unsigned long err = ERR_get_error();
char err_buf[256];
err_buf[0] = '\0';
if (err != 0) {
ERR_error_string_n(err, err_buf, sizeof(err_buf));
}
// Drain remaining errors so they don't pollute future calls.
ERR_clear_error();
std::string msg(where);
if (ssl_err != 0) {
msg += " (ssl_error=" + std::to_string(ssl_err) + ")";
}
if (err_buf[0] != '\0') {
msg += ": ";
msg += err_buf;
}
return lean_mk_io_user_error(mk_string(msg.c_str()));
}
static inline lean_obj_res mk_ssl_io_error(char const * where, int ssl_err = 0) {
return lean_io_result_mk_error(mk_ssl_error(where, ssl_err));
}
static inline lean_object * mk_empty_byte_array() {
lean_object * arr = lean_alloc_sarray(1, 0, 0);
lean_sarray_set_size(arr, 0);
return arr;
}
static void free_pending_writes(lean_ssl_session_object * obj) {
if (obj->pending_writes != nullptr) {
for (size_t i = 0; i < obj->pending_writes_count; i++) {
free(obj->pending_writes[i].data);
}
free(obj->pending_writes);
obj->pending_writes = nullptr;
}
obj->pending_writes_count = 0;
}
static bool append_pending_write(lean_ssl_session_object * obj, char const * data, size_t size) {
char * copy = (char*)malloc(size);
if (copy == nullptr) return false;
std::memcpy(copy, data, size);
size_t new_count = obj->pending_writes_count + 1;
lean_ssl_pending_write * new_arr = (lean_ssl_pending_write*)realloc(
obj->pending_writes, sizeof(lean_ssl_pending_write) * new_count
);
if (new_arr == nullptr) {
free(copy);
return false;
}
obj->pending_writes = new_arr;
obj->pending_writes[obj->pending_writes_count].data = copy;
obj->pending_writes[obj->pending_writes_count].size = size;
obj->pending_writes_count = new_count;
return true;
}
/*
Return values:
1 -> write completed
0 -> write blocked (WANT_READ / WANT_WRITE / ZERO_RETURN)
-1 -> fatal error
*/
static int ssl_write_step(lean_ssl_session_object * obj, char const * data, size_t size, int * out_err) {
if (size > INT_MAX) {
*out_err = SSL_ERROR_SSL;
return -1;
}
int rc = SSL_write(obj->ssl, data, (int)size);
if (rc > 0) {
return 1;
}
int err = SSL_get_error(obj->ssl, rc);
*out_err = err;
if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
return 0;
}
return -1;
}
/*
Return values:
1 -> all pending writes flushed
0 -> still blocked by renegotiation
-1 -> fatal error, *out_err filled
*/
static int try_flush_pending_writes(lean_ssl_session_object * obj, int * out_err) {
if (obj->pending_writes_count == 0) return 1;
size_t completed = 0;
for (size_t i = 0; i < obj->pending_writes_count; i++) {
lean_ssl_pending_write * pw = &obj->pending_writes[i];
while (pw->size > 0) {
int err = 0;
int step = ssl_write_step(obj, pw->data, pw->size, &err);
if (step == 1) {
// We do not enable partial writes, so a successful SSL_write consumes the full buffer.
pw->size = 0;
continue;
}
if (step == 0) {
goto done;
}
*out_err = err;
return -1;
}
free(pw->data);
pw->data = nullptr;
completed++;
}
done:
if (completed > 0) {
obj->pending_writes_count -= completed;
if (obj->pending_writes_count == 0) {
free(obj->pending_writes);
obj->pending_writes = nullptr;
} else {
std::memmove(
obj->pending_writes,
obj->pending_writes + completed,
sizeof(lean_ssl_pending_write) * obj->pending_writes_count
);
// Keep memory usage proportional to currently queued writes.
lean_ssl_pending_write * shrunk = (lean_ssl_pending_write*)realloc(
obj->pending_writes,
sizeof(lean_ssl_pending_write) * obj->pending_writes_count
);
if (shrunk != nullptr) {
obj->pending_writes = shrunk;
}
}
}
return obj->pending_writes_count == 0 ? 1 : 0;
}
void lean_ssl_session_finalizer(void * ptr) {
lean_ssl_session_object * obj = (lean_ssl_session_object*)ptr;
if (obj->ssl != nullptr) {
SSL_free(obj->ssl);
}
free_pending_writes(obj);
free(obj);
}
void initialize_openssl_session() {
g_ssl_session_external_class = lean_register_external_class(lean_ssl_session_finalizer, [](void * obj, lean_object * f) {
(void)obj;
(void)f;
});
}
static lean_obj_res mk_ssl_session(uint8_t is_server) {
SSL_CTX * ctx = is_server ? get_openssl_server_ctx() : get_openssl_client_ctx();
if (ctx == nullptr) {
return mk_ssl_io_error("failed to initialize OpenSSL context");
}
SSL * ssl = SSL_new(ctx);
if (ssl == nullptr) {
return mk_ssl_io_error("SSL_new failed");
}
BIO * read_bio = BIO_new(BIO_s_mem());
BIO * write_bio = BIO_new(BIO_s_mem());
if (read_bio == nullptr || write_bio == nullptr) {
if (read_bio != nullptr) BIO_free(read_bio);
if (write_bio != nullptr) BIO_free(write_bio);
SSL_free(ssl);
return mk_ssl_io_error("BIO_new failed");
}
BIO_set_nbio(read_bio, 1);
BIO_set_nbio(write_bio, 1);
SSL_set_bio(ssl, read_bio, write_bio);
SSL_set_mode(ssl, SSL_MODE_AUTO_RETRY);
if (is_server) {
SSL_set_accept_state(ssl);
} else {
SSL_set_connect_state(ssl);
}
lean_ssl_session_object * ssl_obj = (lean_ssl_session_object*)malloc(sizeof(lean_ssl_session_object));
if (ssl_obj == nullptr) {
SSL_free(ssl);
return mk_ssl_io_error("failed to allocate SSL session object");
}
ssl_obj->ssl = ssl;
ssl_obj->read_bio = read_bio;
ssl_obj->write_bio = write_bio;
ssl_obj->pending_writes_count = 0;
ssl_obj->pending_writes = nullptr;
lean_object * obj = lean_ssl_session_object_new(ssl_obj);
lean_mark_mt(obj);
return lean_io_result_mk_ok(obj);
}
/* Std.Internal.SSL.Session.mk (isServer : Bool) : IO Session */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk(uint8_t is_server) {
return mk_ssl_session(is_server);
}
/* Std.Internal.SSL.Session.mkServer : IO Session */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server() {
return mk_ssl_session(1);
}
/* Std.Internal.SSL.Session.mkClient : IO Session */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client() {
return mk_ssl_session(0);
}
/* Std.Internal.SSL.configureServerContext (certFile keyFile : @& String) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_server_ctx(b_obj_arg cert_file, b_obj_arg key_file) {
SSL_CTX * ctx = get_openssl_server_ctx();
if (ctx == nullptr) {
return mk_ssl_io_error("failed to initialize OpenSSL context");
}
const char * cert = lean_string_cstr(cert_file);
const char * key = lean_string_cstr(key_file);
if (SSL_CTX_use_certificate_file(ctx, cert, SSL_FILETYPE_PEM) <= 0) {
return mk_ssl_io_error("SSL_CTX_use_certificate_file failed");
}
if (SSL_CTX_use_PrivateKey_file(ctx, key, SSL_FILETYPE_PEM) <= 0) {
return mk_ssl_io_error("SSL_CTX_use_PrivateKey_file failed");
}
if (SSL_CTX_check_private_key(ctx) != 1) {
return mk_ssl_io_error("SSL_CTX_check_private_key failed");
}
return lean_io_result_mk_ok(lean_box(0));
}
/* Std.Internal.SSL.configureClientContext (caFile : @& String) (verifyPeer : Bool) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_client_ctx(b_obj_arg ca_file, uint8_t verify_peer) {
SSL_CTX * ctx = get_openssl_client_ctx();
if (ctx == nullptr) {
return mk_ssl_io_error("failed to initialize OpenSSL client context");
}
const char * ca = lean_string_cstr(ca_file);
if (ca != nullptr && ca[0] != '\0') {
if (SSL_CTX_load_verify_locations(ctx, ca, nullptr) != 1) {
return mk_ssl_io_error("SSL_CTX_load_verify_locations failed");
}
} else if (verify_peer) {
// Fall back to platform trust anchors when no custom CA file is provided.
if (SSL_CTX_set_default_verify_paths(ctx) != 1) {
return mk_ssl_io_error("SSL_CTX_set_default_verify_paths failed");
}
}
SSL_CTX_set_verify(ctx, verify_peer ? SSL_VERIFY_PEER : SSL_VERIFY_NONE, nullptr);
return lean_io_result_mk_ok(lean_box(0));
}
/* Std.Internal.SSL.Session.setServerName (ssl : @& Session) (host : @& String) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
const char * server_name = lean_string_cstr(host);
if (SSL_set_tlsext_host_name(ssl_obj->ssl, server_name) != 1) {
return mk_ssl_io_error("SSL_set_tlsext_host_name failed");
}
return lean_io_result_mk_ok(lean_box(0));
}
/* Std.Internal.SSL.Session.verifyResult (ssl : @& Session) : IO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg ssl) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
long result = SSL_get_verify_result(ssl_obj->ssl);
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)result));
}
/* Std.Internal.SSL.Session.handshake (ssl : @& Session) : IO Bool */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg ssl) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
int rc = SSL_do_handshake(ssl_obj->ssl);
if (rc == 1) {
return lean_io_result_mk_ok(lean_box(1));
}
int err = SSL_get_error(ssl_obj->ssl, rc);
if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
return lean_io_result_mk_ok(lean_box(0));
}
return mk_ssl_io_error("SSL_do_handshake failed", err);
}
/* Std.Internal.SSL.Session.write (ssl : @& Session) (data : @& ByteArray) : IO Bool */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg ssl, b_obj_arg data) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
size_t data_len = lean_sarray_size(data);
char const * payload = (char const*)lean_sarray_cptr(data);
if (data_len == 0) {
return lean_io_result_mk_ok(lean_box(1));
}
int err = 0;
int step = ssl_write_step(ssl_obj, payload, data_len, &err);
if (step == 1) {
return lean_io_result_mk_ok(lean_box(1));
}
// If renegotiation blocks writes, queue plaintext and retry after subsequent reads.
if (step == 0 && err == SSL_ERROR_WANT_READ) {
if (!append_pending_write(ssl_obj, payload, data_len)) {
return mk_ssl_io_error("failed to append pending SSL write");
}
return lean_io_result_mk_ok(lean_box(0));
}
if (step == 0 && (err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN)) {
return lean_io_result_mk_ok(lean_box(0));
}
return mk_ssl_io_error("SSL_write failed", err);
}
/* Std.Internal.SSL.Session.read? (ssl : @& Session) (maxBytes : UInt64) : IO (Option ByteArray) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg ssl, uint64_t max_bytes) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
if (max_bytes == 0) {
return lean_io_result_mk_ok(mk_option_some(mk_empty_byte_array()));
}
if (max_bytes > INT_MAX) {
max_bytes = INT_MAX;
}
lean_object * out = lean_alloc_sarray(1, 0, max_bytes);
int rc = SSL_read(ssl_obj->ssl, (void*)lean_sarray_cptr(out), (int)max_bytes);
if (rc > 0) {
int flush_err = 0;
if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
lean_dec(out);
return mk_ssl_io_error("pending SSL write flush failed", flush_err);
}
lean_sarray_set_size(out, (size_t)rc);
return lean_io_result_mk_ok(mk_option_some(out));
}
lean_dec(out);
int err = SSL_get_error(ssl_obj->ssl, rc);
if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
int flush_err = 0;
if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
return mk_ssl_io_error("pending SSL write flush failed", flush_err);
}
return lean_io_result_mk_ok(mk_option_none());
}
return mk_ssl_io_error("SSL_read failed", err);
}
/* Std.Internal.SSL.Session.feedEncrypted (ssl : @& Session) (data : @& ByteArray) : IO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg ssl, b_obj_arg data) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
size_t data_len = lean_sarray_size(data);
if (data_len == 0) {
return lean_io_result_mk_ok(lean_box_uint64(0));
}
if (data_len > INT_MAX) {
return mk_ssl_io_error("BIO_write input too large");
}
int rc = BIO_write(ssl_obj->read_bio, lean_sarray_cptr(data), (int)data_len);
if (rc >= 0) {
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)rc));
}
if (BIO_should_retry(ssl_obj->read_bio)) {
return lean_io_result_mk_ok(lean_box_uint64(0));
}
return mk_ssl_io_error("BIO_write failed");
}
/* Std.Internal.SSL.Session.drainEncrypted (ssl : @& Session) : IO ByteArray */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg ssl) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
size_t pending = BIO_ctrl_pending(ssl_obj->write_bio);
if (pending == 0) {
return lean_io_result_mk_ok(mk_empty_byte_array());
}
if (pending > INT_MAX) {
return mk_ssl_io_error("BIO_pending output too large");
}
lean_object * out = lean_alloc_sarray(1, 0, pending);
int rc = BIO_read(ssl_obj->write_bio, (void*)lean_sarray_cptr(out), (int)pending);
if (rc >= 0) {
lean_sarray_set_size(out, (size_t)rc);
return lean_io_result_mk_ok(out);
}
lean_dec(out);
if (BIO_should_retry(ssl_obj->write_bio)) {
return lean_io_result_mk_ok(mk_empty_byte_array());
}
return mk_ssl_io_error("BIO_read failed");
}
/* Std.Internal.SSL.Session.pendingEncrypted (ssl : @& Session) : IO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg ssl) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)BIO_ctrl_pending(ssl_obj->write_bio)));
}
/* Std.Internal.SSL.Session.pendingPlaintext (ssl : @& Session) : IO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg ssl) {
lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)SSL_pending(ssl_obj->ssl)));
}
#else
void initialize_openssl_session() {}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk(uint8_t is_server) {
(void)is_server;
return io_result_mk_error("lean_uv_ssl_mk is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_server_ctx(b_obj_arg cert_file, b_obj_arg key_file) {
(void)cert_file;
(void)key_file;
return io_result_mk_error("lean_uv_ssl_configure_server_ctx is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_client_ctx(b_obj_arg ca_file, uint8_t verify_peer) {
(void)ca_file;
(void)verify_peer;
return io_result_mk_error("lean_uv_ssl_configure_client_ctx is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host) {
(void)ssl;
(void)host;
return io_result_mk_error("lean_uv_ssl_set_server_name is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg ssl) {
(void)ssl;
return io_result_mk_error("lean_uv_ssl_verify_result is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server() {
return io_result_mk_error("lean_uv_ssl_mk_server is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client() {
return io_result_mk_error("lean_uv_ssl_mk_client is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg ssl) {
(void)ssl;
return io_result_mk_error("lean_uv_ssl_handshake is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg ssl, b_obj_arg data) {
(void)ssl;
(void)data;
return io_result_mk_error("lean_uv_ssl_write is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg ssl, uint64_t max_bytes) {
(void)ssl;
(void)max_bytes;
return io_result_mk_error("lean_uv_ssl_read is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg ssl, b_obj_arg data) {
(void)ssl;
(void)data;
return io_result_mk_error("lean_uv_ssl_feed_encrypted is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg ssl) {
(void)ssl;
return io_result_mk_error("lean_uv_ssl_drain_encrypted is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg ssl) {
(void)ssl;
return io_result_mk_error("lean_uv_ssl_pending_encrypted is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg ssl) {
(void)ssl;
return io_result_mk_error("lean_uv_ssl_pending_plaintext is not supported");
}
#endif
}

View File

@@ -0,0 +1,55 @@
/*
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues
*/
#pragma once
#include <lean/lean.h>
#include "runtime/io.h"
#include "runtime/object.h"
#include "runtime/openssl.h"
#ifndef LEAN_EMSCRIPTEN
#include <openssl/ssl.h>
#include <openssl/bio.h>
#endif
namespace lean {
static lean_external_class * g_ssl_session_external_class = nullptr;
void initialize_openssl_session();
#ifndef LEAN_EMSCRIPTEN
typedef struct {
char * data;
size_t size;
} lean_ssl_pending_write;
typedef struct {
SSL * ssl;
BIO * read_bio;
BIO * write_bio;
size_t pending_writes_count;
lean_ssl_pending_write * pending_writes;
} lean_ssl_session_object;
static inline lean_object * lean_ssl_session_object_new(lean_ssl_session_object * s) { return lean_alloc_external(g_ssl_session_external_class, s); }
static inline lean_ssl_session_object * lean_to_ssl_session_object(lean_object * o) { return (lean_ssl_session_object*)(lean_get_external_data(o)); }
#endif
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk(uint8_t is_server);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_server_ctx(b_obj_arg cert_file, b_obj_arg key_file);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_configure_client_ctx(b_obj_arg ca_file, uint8_t verify_peer);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg ssl);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg ssl);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg ssl, b_obj_arg data);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg ssl, uint64_t max_bytes);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg ssl, b_obj_arg data);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg ssl);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg ssl);
}