mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-22 21:04:07 +00:00
Compare commits
6 Commits
fix-nightl
...
sofia/open
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
48293bb323 | ||
|
|
adab6fefa0 | ||
|
|
12796e60bf | ||
|
|
9e27f77a45 | ||
|
|
4a26fe317d | ||
|
|
23797245eb |
@@ -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
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
417
src/Std/Internal/Async/TCP/SSL.lean
Normal file
417
src/Std/Internal/Async/TCP/SSL.lean
Normal 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
117
src/Std/Internal/SSL.lean
Normal 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
|
||||
@@ -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)
|
||||
|
||||
@@ -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
96
src/runtime/openssl.cpp
Normal 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
25
src/runtime/openssl.h
Normal 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);
|
||||
561
src/runtime/openssl/session.cpp
Normal file
561
src/runtime/openssl/session.cpp
Normal 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
|
||||
|
||||
}
|
||||
55
src/runtime/openssl/session.h
Normal file
55
src/runtime/openssl/session.h
Normal 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);
|
||||
|
||||
}
|
||||
Reference in New Issue
Block a user