From 1bda902d60b461db3396c30a9bc8558f6bf165a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Wed, 12 Jan 2022 16:24:33 +0100 Subject: [PATCH 1/7] Add basic bindings --- .gdbinit | 8 + bindings/lean_utils.h | 40 ++++ bindings/openssl-shim.c | 488 +++++++++++++++----------------------- flake.nix | 22 +- src/OpenSSL.lean | 15 +- src/OpenSSL/Bindings.lean | 132 +++++++++++ test/Tests.lean | 8 +- 7 files changed, 392 insertions(+), 321 deletions(-) create mode 100644 .gdbinit create mode 100644 bindings/lean_utils.h create mode 100644 src/OpenSSL/Bindings.lean diff --git a/.gdbinit b/.gdbinit new file mode 100644 index 0000000..46aaa6c --- /dev/null +++ b/.gdbinit @@ -0,0 +1,8 @@ +define nb + shell nix build .#test-debug -L + file result/bin/tests +end +define nbr + nb + run +end diff --git a/bindings/lean_utils.h b/bindings/lean_utils.h new file mode 100644 index 0000000..1f65be5 --- /dev/null +++ b/bindings/lean_utils.h @@ -0,0 +1,40 @@ +#include + +/** + * Unwrap an Option of a lean_object* as data for some + * or NULL (0) for none. Unsafe. + */ +static inline lean_object *lean_option_unwrap(b_lean_obj_arg a) { + if (lean_is_scalar(a)) { + return 0; + } else { + lean_object *some_val = lean_ctor_get(a, 0); + return some_val; + } +} + +inline static void foreach_noop(void *mod, b_lean_obj_arg fn) {} + +/** + * Option.some a + */ +static inline lean_object * lean_mk_option_some(lean_object * a) { + lean_object* tuple = lean_alloc_ctor(1, 1, 0); + lean_ctor_set(tuple, 0, a); + return tuple; +} + +/** + * Option.none. + * Note that this is the same value for Unit and other constant constructors of inductives. + */ +static inline lean_object * lean_mk_option_none() { + return lean_box(0); +} + +static inline lean_object * lean_mk_tuple2(lean_object * a, lean_object * b) { + lean_object* tuple = lean_alloc_ctor(0, 2, 0); + lean_ctor_set(tuple, 0, a); + lean_ctor_set(tuple, 1, b); + return tuple; +} diff --git a/bindings/openssl-shim.c b/bindings/openssl-shim.c index 9c1c25b..a4aa87b 100644 --- a/bindings/openssl-shim.c +++ b/bindings/openssl-shim.c @@ -1,4 +1,5 @@ -#include "lean/lean.h" +#include +#include "lean_utils.h" #include #include @@ -14,368 +15,251 @@ #include #include -/* Global SSL context */ -SSL_CTX *ctx; +/** + * SSL library initialisation + * initLib: Unit → IO Unit + */ +lean_obj_res lean_ssl_lib_init(lean_obj_arg _u) +{ + SSL_library_init(); + OpenSSL_add_all_algorithms(); + SSL_load_error_strings(); + ERR_load_BIO_strings(); + ERR_load_crypto_strings(); + return lean_io_result_mk_ok(lean_box(0)); +} -#define DEFAULT_BUF_SIZE 64 +// Context -void handle_error(const char *file, int lineno, const char *msg) { - fprintf(stderr, "** %s:%i %s\n", file, lineno, msg); - ERR_print_errors_fp(stderr); - exit(-1); +static inline void ssl_ctx_finalize(void *ctx) +{ + SSL_CTX_free(ctx); } -#define int_error(msg) handle_error(__FILE__, __LINE__, msg) +static lean_external_class *g_ssl_ctx_class = 0; -void die(const char *msg) { - perror(msg); - exit(1); +static lean_external_class *get_ssl_ctx_class() { + if (g_ssl_ctx_class == 0) { + g_ssl_ctx_class = lean_register_external_class( + &ssl_ctx_finalize, &foreach_noop + ); + } + return g_ssl_ctx_class; } -void print_unencrypted_data(char *buf, size_t len) { - printf("%.*s", (int)len, buf); +/** + * Create a SSL_CTX* server context. + * Context.init : Unit → IO Context + */ +lean_obj_res lean_ssl_ctx_init(b_lean_obj_arg _a) +{ + /* create the SSL server context */ + SSL_CTX* ctx = SSL_CTX_new(SSLv23_method()); + if (!ctx) { + return lean_io_result_mk_error(lean_mk_string("SSL_CTX_new() failed")); + } + /* Recommended to avoid SSLv2 & SSLv3 */ + SSL_CTX_set_options(ctx, SSL_OP_ALL|SSL_OP_NO_SSLv2|SSL_OP_NO_SSLv3); + return lean_io_result_mk_ok(lean_alloc_external(get_ssl_ctx_class(), ctx)); } -/* An instance of this object is created each time a client connection is - * accepted. It stores the client file descriptor, the SSL objects, and data - * which is waiting to be either written to socket or encrypted. */ -struct ssl_client +/** + * Load certificate file into context. + * Context.useCertificateFile : @& Context → @& String → IO Bool + */ +lean_obj_res lean_ssl_ctx_use_certificate_file(b_lean_obj_arg l_ctx, b_lean_obj_arg certfile) { - int fd; - - SSL *ssl; - - BIO *rbio; /* SSL reads from, we write to. */ - BIO *wbio; /* SSL writes to, we read from. */ - - /* Bytes waiting to be written to socket. This is data that has been generated - * by the SSL object, either due to encryption of user input, or, writes - * requires due to peer-requested SSL renegotiation. */ - char* write_buf; - size_t write_len; - - /* Bytes waiting to be encrypted by the SSL object. */ - char* encrypt_buf; - size_t encrypt_len; - - /* Method to invoke when unencrypted bytes are available. */ - void (*io_on_read)(char *buf, size_t len); -} client; - -/* This enum contols whether the SSL connection needs to initiate the SSL - * handshake. */ -enum ssl_mode { SSLMODE_SERVER, SSLMODE_CLIENT }; + SSL_CTX* ctx = lean_get_external_data(l_ctx); + bool res = SSL_CTX_use_certificate_file(ctx, lean_string_cstr(certfile), SSL_FILETYPE_PEM); + return lean_io_result_mk_ok(lean_box(res)); +} -void ssl_client_init(struct ssl_client *p, - int fd, - enum ssl_mode mode) +/** + * Load private key file into context. + * Context.usePrivateKeyFile : @& Context → @& String → IO Bool + */ +lean_obj_res lean_ssl_ctx_use_private_key_file(b_lean_obj_arg l_ctx, b_lean_obj_arg keyfile) { - memset(p, 0, sizeof(struct ssl_client)); - - p->fd = fd; - - p->rbio = BIO_new(BIO_s_mem()); - p->wbio = BIO_new(BIO_s_mem()); - p->ssl = SSL_new(ctx); - - if (mode == SSLMODE_SERVER) - SSL_set_accept_state(p->ssl); /* ssl server mode */ - else if (mode == SSLMODE_CLIENT) - SSL_set_connect_state(p->ssl); /* ssl client mode */ - - SSL_set_bio(p->ssl, p->rbio, p->wbio); - - p->io_on_read = print_unencrypted_data; + SSL_CTX* ctx = lean_get_external_data(l_ctx); + bool res = SSL_CTX_use_PrivateKey_file(ctx, lean_string_cstr(keyfile), SSL_FILETYPE_PEM); + return lean_io_result_mk_ok(lean_box(res)); } +/** + * Make sure the key and certificate file match. + * Context.checkPrivateKey : @& Context → IO Bool + */ +lean_obj_res lean_ssl_ctx_check_private_key(b_lean_obj_arg l_ctx, b_lean_obj_arg keyfile) +{ + SSL_CTX* ctx = lean_get_external_data(l_ctx); + bool res = SSL_CTX_check_private_key(ctx); + return lean_io_result_mk_ok(lean_box(res)); +} +// SSL -inline static void noop(void *mod, b_lean_obj_arg fn) {} - - -void ssl_client_cleanup(struct ssl_client *p) +void ssl_finalize(void *ssl) { - SSL_free(p->ssl); /* free the SSL object and its BIO's */ - free(p->write_buf); - free(p->encrypt_buf); + SSL_free(ssl); } -static lean_external_class *g_ssl_client_class = NULL; +static lean_external_class *g_ssl_class = 0; -static lean_external_class *get_ssl_client_class() { - if (g_ssl_client_class == NULL) { - g_ssl_client_class = lean_register_external_class( - &ssl_client_cleanup, &noop); +static lean_external_class *get_ssl_class() { + if (g_ssl_class == 0) { + g_ssl_class = lean_register_external_class( + &ssl_finalize, &foreach_noop + ); } - return g_ssl_client_class; + return g_ssl_class; } /** - * Initialize a hasher. + * Create a SSL* struct. + * Context.initSSL : @& Context → IO SSL */ -lean_obj_res lean_ssl_client_init() { - struct ssl_client *a = malloc(sizeof(struct ssl_client)); - int sockfd = socket(AF_INET, SOCK_STREAM, 0); - if (sockfd < 0) - die("socket()"); - - ssl_client_init(a, sockfd, SSLMODE_CLIENT); - return lean_alloc_external(get_ssl_client_class(), a); +lean_obj_res lean_ssl_init(b_lean_obj_arg l_ctx) +{ + SSL_CTX* ctx = lean_get_external_data(l_ctx); + SSL* ssl = SSL_new(ctx); + return lean_io_result_mk_ok(lean_alloc_external(get_ssl_class(), ssl)); } -int ssl_client_want_write(struct ssl_client *cp) { - return (cp->write_len>0); +/** + * SSL.isInitFinished : @& SSL → IO Bool + */ +lean_obj_res lean_ssl_is_init_finished(b_lean_obj_arg l_ssl) +{ + SSL* ssl = lean_get_external_data(l_ssl); + bool b = SSL_is_init_finished(ssl); + return lean_io_result_mk_ok(lean_box(b)); } -/* Obtain the return value of an SSL operation and convert into a simplified - * error code, which is easier to examine for failure. */ -enum sslstatus { SSLSTATUS_OK, SSLSTATUS_WANT_IO, SSLSTATUS_FAIL}; - -static enum sslstatus get_sslstatus(SSL* ssl, int n) +/** + * SSL.isServer : @& SSL → IO Bool + */ +lean_obj_res lean_ssl_is_server(b_lean_obj_arg l_ssl) { - switch (SSL_get_error(ssl, n)) - { - case SSL_ERROR_NONE: - return SSLSTATUS_OK; - case SSL_ERROR_WANT_WRITE: - case SSL_ERROR_WANT_READ: - return SSLSTATUS_WANT_IO; - case SSL_ERROR_ZERO_RETURN: - case SSL_ERROR_SYSCALL: - default: - return SSLSTATUS_FAIL; - } + SSL* ssl = lean_get_external_data(l_ssl); + bool b = SSL_is_server(ssl); + return lean_io_result_mk_ok(lean_box(b)); } -/* Handle request to send unencrypted data to the SSL. All we do here is just - * queue the data into the encrypt_buf for later processing by the SSL - * object. */ -void send_unencrypted_bytes(const char *buf, size_t len) +/** + * SSL.setConectState : @& SSL → IO Unit + */ +lean_obj_res lean_ssl_set_connect_state(b_lean_obj_arg l_ssl) { - client.encrypt_buf = (char*)realloc(client.encrypt_buf, client.encrypt_len + len); - memcpy(client.encrypt_buf+client.encrypt_len, buf, len); - client.encrypt_len += len; + SSL* ssl = lean_get_external_data(l_ssl); + SSL_set_connect_state(ssl); + return lean_io_result_mk_ok(lean_box(0)); } -/* Queue encrypted bytes. Should only be used when the SSL object has requested a - * write operation. */ -void queue_encrypted_bytes(const char *buf, size_t len) +/** + * SSL.setAcceptState : @& SSL → IO Unit + */ +lean_obj_res lean_ssl_set_accept_state(b_lean_obj_arg l_ssl) { - client.write_buf = (char*)realloc(client.write_buf, client.write_len + len); - memcpy(client.write_buf+client.write_len, buf, len); - client.write_len += len; + SSL* ssl = lean_get_external_data(l_ssl); + SSL_set_accept_state(ssl); + return lean_io_result_mk_ok(lean_box(0)); } -enum sslstatus do_ssl_handshake() +/** + * SSL.write : @& SSL → @& ByteArray → IO Unit + */ +lean_obj_res lean_ssl_write(b_lean_obj_arg l_ssl, b_lean_obj_arg bs) { - char buf[DEFAULT_BUF_SIZE]; - enum sslstatus status; - - int n = SSL_do_handshake(client.ssl); - status = get_sslstatus(client.ssl, n); - - /* Did SSL request to write bytes? */ - if (status == SSLSTATUS_WANT_IO) - do { - n = BIO_read(client.wbio, buf, sizeof(buf)); - if (n > 0) - queue_encrypted_bytes(buf, n); - else if (!BIO_should_retry(client.wbio)) - return SSLSTATUS_FAIL; - } while (n>0); - - return status; + SSL* ssl = lean_get_external_data(l_ssl); + uint8_t* buf = lean_sarray_cptr(bs); + size_t len = lean_sarray_size(bs); + bool b = SSL_write(ssl, buf, len); + return lean_io_result_mk_ok(lean_box(b)); } -/* Process SSL bytes received from the peer. The data needs to be fed into the - SSL object to be unencrypted. On success, returns 0, on SSL error -1. */ -int on_read_cb(char* src, size_t len) +/** + * SSL.read : @& SSL → USize → IO (Bool × ByteArray) + */ +lean_obj_res lean_ssl_read(b_lean_obj_arg l_ssl, size_t len) { - char buf[DEFAULT_BUF_SIZE]; - enum sslstatus status; - int n; - - while (len > 0) { - n = BIO_write(client.rbio, src, len); - - if (n<=0) - return -1; /* assume bio write failure is unrecoverable */ - - src += n; - len -= n; - - if (!SSL_is_init_finished(client.ssl)) { - if (do_ssl_handshake() == SSLSTATUS_FAIL) - return -1; - if (!SSL_is_init_finished(client.ssl)) - return 0; - } - - /* The encrypted data is now in the input bio so now we can perform actual - * read of unencrypted data. */ - - do { - n = SSL_read(client.ssl, buf, sizeof(buf)); - if (n > 0) - client.io_on_read(buf, (size_t)n); - } while (n > 0); - - status = get_sslstatus(client.ssl, n); - - /* Did SSL request to write bytes? This can happen if peer has requested SSL - * renegotiation. */ - if (status == SSLSTATUS_WANT_IO) - do { - n = BIO_read(client.wbio, buf, sizeof(buf)); - if (n > 0) - queue_encrypted_bytes(buf, n); - else if (!BIO_should_retry(client.wbio)) - return -1; - } while (n>0); - - if (status == SSLSTATUS_FAIL) - return -1; - } - - return 0; + SSL* ssl = lean_get_external_data(l_ssl); + lean_object* bs = lean_alloc_sarray(1, len, len); + uint8_t* buf = lean_sarray_cptr(bs); + bool b = SSL_read(ssl, buf, len); + return lean_io_result_mk_ok(lean_mk_tuple2(lean_box(b), bs)); } -/* Process outbound unencrypted data that is waiting to be encrypted. The - * waiting data resides in encrypt_buf. It needs to be passed into the SSL - * object for encryption, which in turn generates the encrypted bytes that then - * will be queued for later socket write. */ -int do_encrypt() +/** + * SSL.setReadBIO : @& SSL → @& BIO → IO Unit + */ +lean_obj_res lean_ssl_set_rbio(b_lean_obj_arg l_ssl, b_lean_obj_arg l_bio) { - char buf[DEFAULT_BUF_SIZE]; - enum sslstatus status; - - if (!SSL_is_init_finished(client.ssl)) - return 0; - - while (client.encrypt_len>0) { - int n = SSL_write(client.ssl, client.encrypt_buf, client.encrypt_len); - status = get_sslstatus(client.ssl, n); - - if (n>0) { - /* consume the waiting bytes that have been used by SSL */ - if ((size_t)n 0) - queue_encrypted_bytes(buf, n); - else if (!BIO_should_retry(client.wbio)) - return -1; - } while (n>0); - } - - if (status == SSLSTATUS_FAIL) - return -1; - - if (n==0) - break; - } - return 0; + SSL* ssl = lean_get_external_data(l_ssl); + BIO* rbio = lean_get_external_data(l_bio); + SSL_set0_rbio(ssl, rbio); + return lean_io_result_mk_ok(lean_box(0)); } -/* Read bytes from stdin and queue for later encryption. */ -void do_stdin_read() +/** + * SSL.setWriteBIO : @& SSL → @& BIO → IO Unit + */ +lean_obj_res lean_ssl_set_wbio(b_lean_obj_arg l_ssl, b_lean_obj_arg l_bio) { - char buf[DEFAULT_BUF_SIZE]; - ssize_t n = read(STDIN_FILENO, buf, sizeof(buf)); - if (n>0) - send_unencrypted_bytes(buf, (size_t)n); + SSL* ssl = lean_get_external_data(l_ssl); + BIO* wbio = lean_get_external_data(l_bio); + SSL_set0_wbio(ssl, wbio); + return lean_io_result_mk_ok(lean_box(0)); } -/* Read encrypted bytes from socket. */ -int do_sock_read() -{ - char buf[DEFAULT_BUF_SIZE]; - ssize_t n = read(client.fd, buf, sizeof(buf)); +// BIO - if (n>0) - return on_read_cb(buf, (size_t)n); - else - return -1; +static inline void bio_finalize(void *bio) +{ + BIO_free(bio); } -/* Write encrypted bytes to the socket. */ -int do_sock_write() -{ - ssize_t n = write(client.fd, client.write_buf, client.write_len); - if (n>0) { - if ((size_t)n IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..." From 9923e37f4865eca2f0ac58d5aa24f5a23130be8c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Sat, 29 Jan 2022 20:45:57 +0100 Subject: [PATCH 2/7] Add getError and IO r/w --- bindings/openssl-shim.c | 10 ++++++++++ src/OpenSSL/Bindings.lean | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/bindings/openssl-shim.c b/bindings/openssl-shim.c index a4aa87b..b6b3a05 100644 --- a/bindings/openssl-shim.c +++ b/bindings/openssl-shim.c @@ -211,6 +211,16 @@ lean_obj_res lean_ssl_set_wbio(b_lean_obj_arg l_ssl, b_lean_obj_arg l_bio) return lean_io_result_mk_ok(lean_box(0)); } +/** + * SSL.getError : @& SSL → UInt32 → IO Unit + */ +lean_obj_res lean_ssl_get_error(b_lean_obj_arg l_ssl, uint32_t ret) +{ + SSL* ssl = lean_get_external_data(l_ssl); + int code = SSL_get_error(ssl, ret); + return lean_io_result_mk_ok(lean_box(code)); +} + // BIO static inline void bio_finalize(void *bio) diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index 5de5014..cb3b8fc 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -94,6 +94,12 @@ Read from connection. @[extern "lean_ssl_read"] constant read: @& SSL → USize → IO (Bool × ByteArray) +/- +Get error. +-/ +@[extern "lean_ssl_get_error"] +constant getError: @& SSL → UInt32 → IO UInt32 + end SSL -- BIO @@ -127,6 +133,19 @@ Initialize a BIO struct. @[extern "lean_bio_init"] constant init : Unit → IO BIO +/- +Write to BIO. +-/ +@[extern "lean_bio_write"] +constant write: @& BIO → @& ByteArray → IO Unit + +/- +Read from connection. +-/ +@[extern "lean_bio_read"] +constant read: @& BIO → USize → IO (Bool × ByteArray) + + end BIO end OpenSSL From 00b30ac69404fcc88aa79080c615b03823148c13 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Thu, 10 Feb 2022 00:44:20 +0100 Subject: [PATCH 3/7] Update flake --- flake.nix | 13 +++++++------ src/OpenSSL/Bindings.lean | 4 +++- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/flake.nix b/flake.nix index 307032d..cf436d0 100644 --- a/flake.nix +++ b/flake.nix @@ -15,8 +15,8 @@ outputs = { self, lean, utils, nixpkgs }: let supportedSystems = [ - # "aarch64-linux" - # "aarch64-darwin" + "aarch64-linux" + "aarch64-darwin" "i686-linux" "x86_64-darwin" "x86_64-linux" @@ -77,12 +77,13 @@ deps = [ project-debug ]; }; joinDepsDerivationns = getSubDrv: - pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") ([ project ] ++ project.allExternalDeps)); + pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") (project.allExternalDeps)); in { inherit project test; packages = { ${name} = project.executable; + inherit (project) lean-package; test = test.executable; test-debug = test-debug.executable; }; @@ -93,10 +94,10 @@ devShell = pkgs.mkShell { inputsFrom = [ project.executable ]; buildInputs = with pkgs; [ - leanPkgs.lean + leanPkgs.lean-dev ]; - LEAN_PATH = joinDepsDerivationns (d: d.modRoot); - LEAN_SRC_PATH = joinDepsDerivationns (d: d.src); + LEAN_PATH = "./src:./test:" + joinDepsDerivationns (d: d.modRoot); + LEAN_SRC_PATH = "./src:./test:" + joinDepsDerivationns (d: d.src); C_INCLUDE_PATH = INCLUDE_PATH; CPLUS_INCLUDE_PATH = INCLUDE_PATH; }; diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index cb3b8fc..46ae742 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -5,7 +5,9 @@ namespace OpenSSL Initialize the OpenSSL library. -/ @[extern "lean_ssl_lib_init"] -constant initLib: Unit → IO Unit +private constant initLib: Unit → IO Unit + +builtin_initialize initLib () constant ContextPointed : PointedType From 05bcc9bfcc192fbddb63a5a6aa80af27b3c16317 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Thu, 10 Feb 2022 11:34:10 +0100 Subject: [PATCH 4/7] Update Lean and Cli --- flake.lock | 41 +++++++++++++++++++++++++++------------ flake.nix | 31 ++++++++++++++++------------- src/OpenSSL/Bindings.lean | 12 ++++++------ src/OpenSSL/Cli.lean | 12 ++++++++++++ test/Tests.lean | 3 +-- 5 files changed, 66 insertions(+), 33 deletions(-) create mode 100644 src/OpenSSL/Cli.lean diff --git a/flake.lock b/flake.lock index 609bea7..a117a4e 100644 --- a/flake.lock +++ b/flake.lock @@ -34,17 +34,18 @@ "inputs": { "flake-utils": "flake-utils", "lean-stage0": "lean-stage0", + "lean4-mode": "lean4-mode", "mdBook": "mdBook", "nix": "nix", "nixpkgs": "nixpkgs_2", "temci": "temci" }, "locked": { - "lastModified": 1640275476, - "narHash": "sha256-Z0m/6dHimfA9bIGrCJusbN7x1slY7y8uGaDlWhMjRB4=", + "lastModified": 1644438071, + "narHash": "sha256-pXKTS3kcuEwgD7X6Bni+RIu5qM3joNQ/Vr+8kteh8SU=", "owner": "leanprover", "repo": "lean4", - "rev": "70ef4e529c85eeffa15a9a5eeca290a13f484efd", + "rev": "8cbd7ccf096abcbbc61423752bccc35633a0cd87", "type": "github" }, "original": { @@ -68,6 +69,22 @@ "type": "github" } }, + "lean4-mode": { + "flake": false, + "locked": { + "lastModified": 1642754670, + "narHash": "sha256-SI8a4lIV2GVIt1hyCCiBuZy2xrQSPxzF09iRerXw+0M=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "1838a2baeb6f7858bf5ccf5206c80e695ced6840", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, "lowdown-src": { "flake": false, "locked": { @@ -170,11 +187,11 @@ }, "nixpkgs_3": { "locked": { - "lastModified": 1640169700, - "narHash": "sha256-Y+WR7cpiUTroEtoGR8Q3KMbFARvOiACLLmNQ+/iEz2E=", + "lastModified": 1642244250, + "narHash": "sha256-vWpUEqQdVP4srj+/YLJRTN9vjpTs4je0cdWKXPbDItc=", "owner": "nixos", "repo": "nixpkgs", - "rev": "3f0e4de0c2d2c85d7abce260f8c17c8ef5b78e5b", + "rev": "0fd9ee1aa36ce865ad273f4f07fdc093adeb5c00", "type": "github" }, "original": { @@ -186,11 +203,11 @@ }, "nixpkgs_4": { "locked": { - "lastModified": 1640234302, - "narHash": "sha256-dALA+cOam5jQ2KOYdWiv6H6Y2stcYG6eclWQQVGx/FI=", + "lastModified": 1644420267, + "narHash": "sha256-rFJuctggkjM412OC6OGPdXogFp7czGDW05ueWqpJbj8=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "81cbfc8f2a1e218249b7bff74013b63150171496", + "rev": "98bb5b77c8c6666824a4c13d23befa1e07210ef1", "type": "github" }, "original": { @@ -230,11 +247,11 @@ ] }, "locked": { - "lastModified": 1638966113, - "narHash": "sha256-0xH1+2FxKm02tny4AsArtN2xHdjN637spCsar7ks7ZM=", + "lastModified": 1644320798, + "narHash": "sha256-8LdcVelSpuP+dnWseW58RHWrDfEzuhWtfHUFjnrLJs0=", "owner": "yatima-inc", "repo": "nix-utils", - "rev": "8dc43e9ede4af7d9f25512a453a9631fb4259ef0", + "rev": "45c72bfe49924bb9da76bcad3eeb089f6eda6148", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index cf436d0..1994251 100644 --- a/flake.nix +++ b/flake.nix @@ -53,22 +53,27 @@ updateCCOptions = d: d ++ (map (i: "-I${i}") includes) ++ [ "-O0" ]; }; name = "OpenSSL"; # must match the name of the top-level .lean file - project = leanPkgs.buildLeanPackage + OpenSSL = leanPkgs.buildLeanPackage { inherit name; - # deps = [ lean-ipld.project.${system} ]; # Where the lean files are located nativeSharedLibs = [ libssl c-shim ]; src = ./src; }; - project-debug = project.override { + Cli = leanPkgs.buildLeanPackage + { + name = "OpenSSL.Cli"; + deps = [ OpenSSL ]; + src = ./src; + }; + project-debug = OpenSSL.override { debug = true; nativeSharedLibs = [ libssl c-shim-debug ]; }; test = leanPkgs.buildLeanPackage { name = "Tests"; - deps = [ project ]; + deps = [ OpenSSL ]; # Where the lean files are located src = ./test; }; @@ -76,28 +81,28 @@ debug = true; deps = [ project-debug ]; }; - joinDepsDerivationns = getSubDrv: - pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") (project.allExternalDeps)); + joinDepsDerivations = getSubDrv: + pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") (OpenSSL.allExternalDeps)); in { - inherit project test; + project = OpenSSL; packages = { - ${name} = project.executable; - inherit (project) lean-package; + inherit OpenSSL Cli; + inherit (OpenSSL) lean-package; test = test.executable; test-debug = test-debug.executable; }; checks.test = test.executable; - defaultPackage = self.packages.${system}.${name}; + defaultPackage = self.packages.${system}.Cli.executable; devShell = pkgs.mkShell { - inputsFrom = [ project.executable ]; + inputsFrom = [ OpenSSL.executable ]; buildInputs = with pkgs; [ leanPkgs.lean-dev ]; - LEAN_PATH = "./src:./test:" + joinDepsDerivationns (d: d.modRoot); - LEAN_SRC_PATH = "./src:./test:" + joinDepsDerivationns (d: d.src); + LEAN_PATH = "./src:./test:" + joinDepsDerivations (d: d.modRoot); + LEAN_SRC_PATH = "./src:./test:" + joinDepsDerivations (d: d.src); C_INCLUDE_PATH = INCLUDE_PATH; CPLUS_INCLUDE_PATH = INCLUDE_PATH; }; diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index 46ae742..90865ea 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -9,11 +9,11 @@ private constant initLib: Unit → IO Unit builtin_initialize initLib () -constant ContextPointed : PointedType +constant ContextPointed : NonemptyType def Context : Type := ContextPointed.type -instance : Inhabited Context := ⟨ContextPointed.val⟩ +instance : Nonempty Context := ContextPointed.property /- Initialize a SSL context. @@ -39,11 +39,11 @@ Check private key for SSL Context assuming it has been loaded. @[extern "lean_ssl_ctx_check_private_key"] constant Context.checkPrivateKey : @& Context → @& String → IO Bool -constant SSLPointed : PointedType +constant SSLPointed : NonemptyType def SSL : Type := SSLPointed.type -instance : Inhabited SSL := ⟨SSLPointed.val⟩ +instance : Nonempty SSL := SSLPointed.property /- Initialize a SSL struct. @@ -106,14 +106,14 @@ end SSL -- BIO -constant BIOPointed : PointedType +constant BIOPointed : NonemptyType /- Binary IO buffer -/ def BIO : Type := BIOPointed.type -instance : Inhabited BIO := ⟨BIOPointed.val⟩ +instance : Nonempty BIO := BIOPointed.property /- Set read BIO diff --git a/src/OpenSSL/Cli.lean b/src/OpenSSL/Cli.lean new file mode 100644 index 0000000..052ef4e --- /dev/null +++ b/src/OpenSSL/Cli.lean @@ -0,0 +1,12 @@ +import OpenSSL + +open OpenSSL + +def main (args : List String) : IO UInt32 := do + try + let ctx ← Context.init () + let ssl ← ctx.initSSL + pure 0 + catch e => + IO.eprintln <| "error: " ++ toString e + pure 1 diff --git a/test/Tests.lean b/test/Tests.lean index cda0fc0..61a5f5c 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -4,11 +4,10 @@ open OpenSSL def main (args : List String) : IO UInt32 := do try - OpenSSL.initLib () let ctx ← Context.init () let ssl ← ctx.initSSL pure 0 catch e => - IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..." + IO.eprintln <| "error: " ++ toString e pure 1 From 8b9960d306dac7c7d4ba823d0c5ae2f2e0163217 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Tue, 21 Feb 2023 23:23:47 +0100 Subject: [PATCH 5/7] fix: Lake test and bindings --- OpenSSL.lean | 14 ------------- lakefile.lean | 13 +++++++++--- src/OpenSSL/Bindings.lean | 42 +++++++++++++++++++-------------------- 3 files changed, 31 insertions(+), 38 deletions(-) delete mode 100644 OpenSSL.lean diff --git a/OpenSSL.lean b/OpenSSL.lean deleted file mode 100644 index 095c75e..0000000 --- a/OpenSSL.lean +++ /dev/null @@ -1,14 +0,0 @@ -namespace OpenSSL - -opaque SslClientPointed : NonemptyType - -def SslClient := SslClientPointed.type - -noncomputable instance : Inhabited SslClient := - ⟨Classical.choice SslClientPointed.property⟩ - -@[extern "ssl_init"] -opaque sslInit : (certfile : @& String) → (keyfile : @& String) → IO Unit - -@[extern "ssl_client_init"] -opaque sslClientInit : IO SslClient diff --git a/lakefile.lean b/lakefile.lean index 48ec0dd..dce2e58 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,12 +2,15 @@ import Lake open Lake DSL package OpenSSL { - precompileModules := true - moreLinkArgs := #["-L", "./build/lib", "-lssl"] + precompileModules := false + moreLinkArgs := #["-L", "./build/lib", "-lssl", "-lcrypto", "-lffi"] + extraDepTargets := #["ffi"] } @[defaultTarget] -lean_lib OpenSSL +lean_lib OpenSSL { + srcDir := "src" +} def cDir := "native" def ffiSrc := "native.c" @@ -26,3 +29,7 @@ target ffi (pkg : Package) : FilePath := do let name := nameToStaticLib ffiLib let ffiO ← fetch <| pkg.target ``ffi.o buildStaticLib (pkg.buildDir / "lib" / name) #[ffiO] + +lean_exe test { + root := `test.Tests +} diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index 90865ea..f200c48 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -5,11 +5,11 @@ namespace OpenSSL Initialize the OpenSSL library. -/ @[extern "lean_ssl_lib_init"] -private constant initLib: Unit → IO Unit +private opaque initLib: Unit → IO Unit builtin_initialize initLib () -constant ContextPointed : NonemptyType +opaque ContextPointed : NonemptyType def Context : Type := ContextPointed.type @@ -19,27 +19,27 @@ instance : Nonempty Context := ContextPointed.property Initialize a SSL context. -/ @[extern "lean_ssl_ctx_init"] -constant Context.init : Unit → IO Context +opaque Context.init : Unit → IO Context /- Use certificate file for SSL Context. -/ @[extern "lean_ssl_ctx_use_certificate_file"] -constant Context.useCertificateFile : @& Context → @& String → IO Bool +opaque Context.useCertificateFile : @& Context → @& String → IO Bool /- Use private key file for SSL Context. -/ @[extern "lean_ssl_ctx_use_private_key_file"] -constant Context.usePrivateKeyFile : @& Context → @& String → IO Bool +opaque Context.usePrivateKeyFile : @& Context → @& String → IO Bool /- Check private key for SSL Context assuming it has been loaded. -/ @[extern "lean_ssl_ctx_check_private_key"] -constant Context.checkPrivateKey : @& Context → @& String → IO Bool +opaque Context.checkPrivateKey : @& Context → @& String → IO Bool -constant SSLPointed : NonemptyType +opaque SSLPointed : NonemptyType def SSL : Type := SSLPointed.type @@ -49,7 +49,7 @@ instance : Nonempty SSL := SSLPointed.property Initialize a SSL struct. -/ @[extern "lean_ssl_init"] -constant Context.initSSL : @& Context → IO SSL +opaque Context.initSSL : @& Context → IO SSL namespace SSL @@ -64,49 +64,49 @@ SSL_is_init_finished() returns 1 if the SSL/TLS connection is in a state where fully protected application data can be transferred or 0 otherwise. -/ @[extern "lean_ssl_is_init_finished"] -constant isInitFinished: @& SSL → IO Bool +opaque isInitFinished: @& SSL → IO Bool /- Is the SSL connection set to be used as a server. -/ @[extern "lean_ssl_is_server"] -constant isServer: @& SSL → IO Bool +opaque isServer: @& SSL → IO Bool /- Use as a server. -/ @[extern "lean_ssl_set_accept_state"] -constant setAcceptState: @& SSL → IO Unit +opaque setAcceptState: @& SSL → IO Unit /- Use as a client. -/ @[extern "lean_ssl_set_connect_state"] -constant setConnectState: @& SSL → IO Unit +opaque setConnectState: @& SSL → IO Unit /- Write to connection. -/ @[extern "lean_ssl_write"] -constant write: @& SSL → @& ByteArray → IO Unit +opaque write: @& SSL → @& ByteArray → IO Unit /- Read from connection. -/ @[extern "lean_ssl_read"] -constant read: @& SSL → USize → IO (Bool × ByteArray) +opaque read: @& SSL → USize → IO (Bool × ByteArray) /- Get error. -/ @[extern "lean_ssl_get_error"] -constant getError: @& SSL → UInt32 → IO UInt32 +opaque getError: @& SSL → UInt32 → IO UInt32 end SSL -- BIO -constant BIOPointed : NonemptyType +opaque BIOPointed : NonemptyType /- Binary IO buffer @@ -119,13 +119,13 @@ instance : Nonempty BIO := BIOPointed.property Set read BIO -/ @[extern "lean_ssl_set_rbio"] -constant SSL.setReadBIO : @& SSL → @& BIO → IO Unit +opaque SSL.setReadBIO : @& SSL → @& BIO → IO Unit /- Set write BIO -/ @[extern "lean_ssl_set_wbio"] -constant SSL.setWriteBIO : @& SSL → @& BIO → IO Unit +opaque SSL.setWriteBIO : @& SSL → @& BIO → IO Unit namespace BIO @@ -133,19 +133,19 @@ namespace BIO Initialize a BIO struct. -/ @[extern "lean_bio_init"] -constant init : Unit → IO BIO +opaque init : Unit → IO BIO /- Write to BIO. -/ @[extern "lean_bio_write"] -constant write: @& BIO → @& ByteArray → IO Unit +opaque write: @& BIO → @& ByteArray → IO Unit /- Read from connection. -/ @[extern "lean_bio_read"] -constant read: @& BIO → USize → IO (Bool × ByteArray) +opaque read: @& BIO → USize → IO (Bool × ByteArray) end BIO From 737e6c5373f8802f1fa73f1a6d0285014492f933 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Sat, 25 Feb 2023 23:27:39 +0100 Subject: [PATCH 6/7] feat: Add bindings for Addr and Socket --- native/native.c | 63 ++++++++++++++++++++++++++++- src/OpenSSL/Bindings.lean | 85 ++++++++++++++++++++++++++++----------- src/OpenSSL/Cli.lean | 7 ++++ test/Tests.lean | 12 +++++- 4 files changed, 140 insertions(+), 27 deletions(-) diff --git a/native/native.c b/native/native.c index b6b3a05..4e163ae 100644 --- a/native/native.c +++ b/native/native.c @@ -241,9 +241,9 @@ static lean_external_class *get_bio_class() { /** * Create a BIO* struct. - * BIO.init : Unit → IO BIO + * BIO.init : IO BIO */ -lean_obj_res lean_bio_init(lean_obj_arg _a) +lean_obj_res lean_bio_init() { BIO* bio = BIO_new(BIO_s_mem()); return lean_io_result_mk_ok(lean_alloc_external(get_bio_class(), bio)); @@ -273,3 +273,62 @@ lean_obj_res lean_bio_write(b_lean_obj_arg l_bio, b_lean_obj_arg bs) return lean_io_result_mk_ok(lean_box(b)); } +// BIO ADDR + +static inline void bio_addr_finalize(void *bio) +{ + BIO_ADDR_free(bio); +} + +static lean_external_class *g_bio_addr_class = 0; + +static lean_external_class *get_bio_addr_class() { + if (g_bio_addr_class == 0) { + g_bio_addr_class = lean_register_external_class( + &bio_addr_finalize, &foreach_noop + ); + } + return g_bio_addr_class; +} + +/** + * Create a BIO_ADDR* struct. + * BIO.init : IO BIO + */ +lean_obj_res lean_bio_addr_init() +{ + BIO_ADDR * addr = BIO_ADDR_new(); + return lean_io_result_mk_ok(lean_alloc_external(get_bio_addr_class(), addr)); +} + +/** + * BIO.socket : UInt32 -> UInt32 -> UInt32 -> IO UInt32 + */ +lean_obj_res lean_bio_socket(uint32_t domain, uint32_t socktype, uint32_t protocol) +{ + int i = BIO_socket(domain, socktype, protocol, 0); + if (i == BIO_R_INVALID_SOCKET) { + return lean_io_result_mk_error(lean_mk_string("Invalid socket")); + } else { + return lean_io_result_mk_ok(lean_box(i)); + } +} + + +/** + * Socket.connect (sock : Socket) (addr : Addr) : IO UInt32 + */ +lean_obj_res lean_bio_connect(uint32_t sock, b_lean_obj_arg addr) +{ + uint32_t res = BIO_connect(sock, lean_get_external_data(addr), BIO_SOCK_KEEPALIVE | BIO_SOCK_NONBLOCK); + return lean_io_result_mk_ok(lean_box(res)); +} + +/** + * Socket.close (socket : Socket) : IO UInt32 + */ +lean_obj_res lean_bio_closesocket(uint32_t sock) +{ + uint32_t res = BIO_closesocket(sock); + return lean_io_result_mk_ok(lean_box(res)); +} diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index f200c48..0284e12 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -1,7 +1,7 @@ namespace OpenSSL -/- +/-- Initialize the OpenSSL library. -/ @[extern "lean_ssl_lib_init"] @@ -15,25 +15,25 @@ def Context : Type := ContextPointed.type instance : Nonempty Context := ContextPointed.property -/- +/-- Initialize a SSL context. -/ @[extern "lean_ssl_ctx_init"] -opaque Context.init : Unit → IO Context +opaque Context.init : IO Context -/- +/-- Use certificate file for SSL Context. -/ @[extern "lean_ssl_ctx_use_certificate_file"] opaque Context.useCertificateFile : @& Context → @& String → IO Bool -/- +/-- Use private key file for SSL Context. -/ @[extern "lean_ssl_ctx_use_private_key_file"] opaque Context.usePrivateKeyFile : @& Context → @& String → IO Bool -/- +/-- Check private key for SSL Context assuming it has been loaded. -/ @[extern "lean_ssl_ctx_check_private_key"] @@ -45,7 +45,7 @@ def SSL : Type := SSLPointed.type instance : Nonempty SSL := SSLPointed.property -/- +/-- Initialize a SSL struct. -/ @[extern "lean_ssl_init"] @@ -59,44 +59,44 @@ inductive Status | fail deriving BEq, Hashable -/- +/-- SSL_is_init_finished() returns 1 if the SSL/TLS connection is in a state where fully protected application data can be transferred or 0 otherwise. -/ @[extern "lean_ssl_is_init_finished"] opaque isInitFinished: @& SSL → IO Bool -/- +/-- Is the SSL connection set to be used as a server. -/ @[extern "lean_ssl_is_server"] opaque isServer: @& SSL → IO Bool -/- +/-- Use as a server. -/ @[extern "lean_ssl_set_accept_state"] opaque setAcceptState: @& SSL → IO Unit -/- +/-- Use as a client. -/ @[extern "lean_ssl_set_connect_state"] opaque setConnectState: @& SSL → IO Unit -/- +/-- Write to connection. -/ @[extern "lean_ssl_write"] opaque write: @& SSL → @& ByteArray → IO Unit -/- +/-- Read from connection. -/ @[extern "lean_ssl_read"] opaque read: @& SSL → USize → IO (Bool × ByteArray) -/- +/-- Get error. -/ @[extern "lean_ssl_get_error"] @@ -108,20 +108,20 @@ end SSL opaque BIOPointed : NonemptyType -/- -Binary IO buffer +/-- +Basic IO buffer -/ def BIO : Type := BIOPointed.type instance : Nonempty BIO := BIOPointed.property -/- +/-- Set read BIO -/ @[extern "lean_ssl_set_rbio"] opaque SSL.setReadBIO : @& SSL → @& BIO → IO Unit -/- +/-- Set write BIO -/ @[extern "lean_ssl_set_wbio"] @@ -129,24 +129,61 @@ opaque SSL.setWriteBIO : @& SSL → @& BIO → IO Unit namespace BIO -/- -Initialize a BIO struct. +opaque AddrPointed : NonemptyType + +/-- +BIO Address type wrapper around all socket addresses used by OpenSSL. +-/ +def Addr : Type := AddrPointed.type + +instance : Nonempty Addr := AddrPointed.property + +namespace Addr + +/-- +Initialize an Addr struct with no information. -/ -@[extern "lean_bio_init"] -opaque init : Unit → IO BIO +@[extern "lean_bio_addr_init"] +opaque init : IO Addr + +end Addr -/- +/-- Write to BIO. -/ @[extern "lean_bio_write"] opaque write: @& BIO → @& ByteArray → IO Unit -/- +/-- Read from connection. -/ @[extern "lean_bio_read"] opaque read: @& BIO → USize → IO (Bool × ByteArray) +def Socket := UInt32 + +/-- +Open a socket. +-/ +@[extern "lean_bio_socket"] +opaque socket : (domain : UInt32) → (socktype : UInt32) → (protocol : UInt32) → IO Socket + +namespace Socket + +/-- +Connect a socket. +-/ +@[extern "lean_bio_connect"] +opaque connect : (socket : Socket) → (addr : Addr) → IO UInt32 + +/-- +Close a socket. +-/ +@[extern "lean_bio_closesocket"] +opaque close : (socket : Socket) → IO UInt32 + + +end Socket end BIO diff --git a/src/OpenSSL/Cli.lean b/src/OpenSSL/Cli.lean index 052ef4e..9e47d34 100644 --- a/src/OpenSSL/Cli.lean +++ b/src/OpenSSL/Cli.lean @@ -6,6 +6,13 @@ def main (args : List String) : IO UInt32 := do try let ctx ← Context.init () let ssl ← ctx.initSSL + if ← ssl.initFinished then + println! "SSL init finished" + else + println! "SSL init not finished" + ssl.setConnectState + let bio ← BIO.init + pure 0 catch e => IO.eprintln <| "error: " ++ toString e diff --git a/test/Tests.lean b/test/Tests.lean index 61a5f5c..e053203 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -4,8 +4,18 @@ open OpenSSL def main (args : List String) : IO UInt32 := do try - let ctx ← Context.init () + let ctx ← Context.init let ssl ← ctx.initSSL + ssl.setConnectState + let wbio ← BIO.init + let rbio ← BIO.init + ssl.setReadBIO rbio + ssl.setWriteBIO wbio + if ← ssl.isInitFinished then + println! "SSL init finished" + else + println! "SSL init not finished" + pure 0 catch e => IO.eprintln <| "error: " ++ toString e From 901550e0a0772f70ebd9481b4d629bcafa973236 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Sun, 26 Feb 2023 17:07:20 +0100 Subject: [PATCH 7/7] feat: Add connection example --- README.md | 5 ++- lakefile.lean | 2 +- native/native.c | 77 +++++++++++++++++++++++++++++++++++++-- src/OpenSSL/Bindings.lean | 58 +++++++++++++++++++++++++---- test/Tests.lean | 42 ++++++++++++++++++++- 5 files changed, 170 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index aafd55b..9969dc7 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,9 @@ # OpenSSL bindings for lean (unfinished) -Build with `nix build .` +Build with `nix build .` or `nix develop --command lake build`. + +The bindings are mostly imperative and low level. +See the [OpenSSL manpages](https://www.openssl.org/docs/man3.1/) for more details. ## Dev env diff --git a/lakefile.lean b/lakefile.lean index dce2e58..72cc3b3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -22,7 +22,7 @@ target ffi.o (pkg : Package) : FilePath := do let srcJob ← inputFile <| pkg.dir / cDir / ffiSrc buildFileAfterDep oFile srcJob fun srcFile => do let flags := #["-I", (← getLeanIncludeDir).toString, - "-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC"] + "-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC", "-g"] compileO ffiSrc oFile srcFile flags target ffi (pkg : Package) : FilePath := do diff --git a/native/native.c b/native/native.c index 4e163ae..d31d49f 100644 --- a/native/native.c +++ b/native/native.c @@ -24,7 +24,6 @@ lean_obj_res lean_ssl_lib_init(lean_obj_arg _u) SSL_library_init(); OpenSSL_add_all_algorithms(); SSL_load_error_strings(); - ERR_load_BIO_strings(); ERR_load_crypto_strings(); return lean_io_result_mk_ok(lean_box(0)); } @@ -56,7 +55,7 @@ lean_obj_res lean_ssl_ctx_init(b_lean_obj_arg _a) /* create the SSL server context */ SSL_CTX* ctx = SSL_CTX_new(SSLv23_method()); if (!ctx) { - return lean_io_result_mk_error(lean_mk_string("SSL_CTX_new() failed")); + return lean_io_result_mk_error(lean_mk_io_error_other_error(0, lean_mk_string("SSL_CTX_new() failed"))); } /* Recommended to avoid SSLv2 & SSLv3 */ SSL_CTX_set_options(ctx, SSL_OP_ALL|SSL_OP_NO_SSLv2|SSL_OP_NO_SSLv3); @@ -96,6 +95,16 @@ lean_obj_res lean_ssl_ctx_check_private_key(b_lean_obj_arg l_ctx, b_lean_obj_arg return lean_io_result_mk_ok(lean_box(res)); } +/** + * Context.loadVerifyLocations : @& Context → @& String → @& String → IO Bool + */ +lean_obj_res lean_ssl_ctx_load_verify_locations(b_lean_obj_arg l_ctx, b_lean_obj_arg cafile, b_lean_obj_arg capath) +{ + SSL_CTX* ctx = lean_get_external_data(l_ctx); + bool res = SSL_CTX_load_verify_locations(ctx, lean_string_cstr(cafile), lean_string_cstr(capath)); + return lean_io_result_mk_ok(lean_box(res)); +} + // SSL void ssl_finalize(void *ssl) @@ -221,11 +230,21 @@ lean_obj_res lean_ssl_get_error(b_lean_obj_arg l_ssl, uint32_t ret) return lean_io_result_mk_ok(lean_box(code)); } +/** + * SSL.verifyResult : SSL → IO UInt64 + */ +lean_obj_res lean_ssl_verify_result(lean_obj_arg l_ssl) +{ + SSL* ssl = lean_get_external_data(l_ssl); + long code = SSL_get_verify_result(ssl); + return lean_io_result_mk_ok(lean_box(code)); +} + // BIO static inline void bio_finalize(void *bio) { - BIO_free(bio); + BIO_free_all(bio); } static lean_external_class *g_bio_class = 0; @@ -246,6 +265,9 @@ static lean_external_class *get_bio_class() { lean_obj_res lean_bio_init() { BIO* bio = BIO_new(BIO_s_mem()); + if (bio == NULL) { + return lean_io_result_mk_error(lean_mk_string("BIO_new() failed")); + } return lean_io_result_mk_ok(lean_alloc_external(get_bio_class(), bio)); } @@ -273,6 +295,21 @@ lean_obj_res lean_bio_write(b_lean_obj_arg l_bio, b_lean_obj_arg bs) return lean_io_result_mk_ok(lean_box(b)); } +/** + * BIO.getSSL : @& BIO → IO SSL + */ +lean_obj_res lean_bio_get_ssl(lean_obj_arg l_bio) +{ + BIO* bio = lean_get_external_data(l_bio); + SSL* ssl = NULL; + BIO_get_ssl(bio, &ssl); + if (ssl == NULL) { + return lean_io_result_mk_error(lean_mk_io_error_other_error(0, lean_mk_string("BIO_get_ssl() is null"))); + } + return lean_io_result_mk_ok(lean_alloc_external(get_ssl_class(), ssl)); +} + + // BIO ADDR static inline void bio_addr_finalize(void *bio) @@ -298,6 +335,9 @@ static lean_external_class *get_bio_addr_class() { lean_obj_res lean_bio_addr_init() { BIO_ADDR * addr = BIO_ADDR_new(); + if (addr == NULL) { + return lean_io_result_mk_error(lean_mk_string("BIO_ADDR_new() failed")); + } return lean_io_result_mk_ok(lean_alloc_external(get_bio_addr_class(), addr)); } @@ -314,7 +354,6 @@ lean_obj_res lean_bio_socket(uint32_t domain, uint32_t socktype, uint32_t protoc } } - /** * Socket.connect (sock : Socket) (addr : Addr) : IO UInt32 */ @@ -324,6 +363,18 @@ lean_obj_res lean_bio_connect(uint32_t sock, b_lean_obj_arg addr) return lean_io_result_mk_ok(lean_box(res)); } +/** + * BIO.newSSLConnect (ctx : Context) : IO BIO + */ +lean_obj_res lean_bio_new_ssl_connect(lean_obj_arg context) +{ + BIO* bio = BIO_new_ssl_connect(lean_get_external_data(context)); + if (bio == NULL) { + return lean_io_result_mk_error(lean_mk_io_error_other_error(0, lean_mk_string("BIO_new_ssl_connect() failed"))); + } + return lean_io_result_mk_ok(lean_alloc_external(get_bio_class(), bio)); +} + /** * Socket.close (socket : Socket) : IO UInt32 */ @@ -332,3 +383,21 @@ lean_obj_res lean_bio_closesocket(uint32_t sock) uint32_t res = BIO_closesocket(sock); return lean_io_result_mk_ok(lean_box(res)); } + +/** + * BIO.setConnHostname (bio : BIO) (hostname : String) : IO UInt32 + */ +lean_obj_res lean_bio_set_conn_hostname(lean_obj_arg bio, lean_obj_arg hostname) +{ + uint32_t res = BIO_set_conn_hostname(lean_get_external_data(bio), lean_string_cstr(hostname)); + return lean_io_result_mk_ok(lean_box(res)); +} + +/** + * BIO.doConnect : IO UInt32 + */ +lean_obj_res lean_bio_do_connect(lean_obj_arg bio) +{ + uint32_t res = BIO_do_connect(lean_get_external_data(bio)); + return lean_io_result_mk_ok(lean_box(res)); +} diff --git a/src/OpenSSL/Bindings.lean b/src/OpenSSL/Bindings.lean index 0284e12..02b03ef 100644 --- a/src/OpenSSL/Bindings.lean +++ b/src/OpenSSL/Bindings.lean @@ -15,29 +15,39 @@ def Context : Type := ContextPointed.type instance : Nonempty Context := ContextPointed.property +namespace Context + /-- Initialize a SSL context. -/ @[extern "lean_ssl_ctx_init"] -opaque Context.init : IO Context +opaque init : IO Context /-- Use certificate file for SSL Context. -/ @[extern "lean_ssl_ctx_use_certificate_file"] -opaque Context.useCertificateFile : @& Context → @& String → IO Bool +opaque useCertificateFile : @& Context → @& String → IO Bool /-- Use private key file for SSL Context. -/ @[extern "lean_ssl_ctx_use_private_key_file"] -opaque Context.usePrivateKeyFile : @& Context → @& String → IO Bool +opaque usePrivateKeyFile : @& Context → @& String → IO Bool /-- Check private key for SSL Context assuming it has been loaded. -/ @[extern "lean_ssl_ctx_check_private_key"] -opaque Context.checkPrivateKey : @& Context → @& String → IO Bool +opaque checkPrivateKey : @& Context → @& String → IO Bool + +/-- +Set default locations for trusted CA certificates. +-/ +@[extern "lean_ssl_ctx_load_verify_locations"] +opaque loadVerifyLocations : @& Context → @& String → @& String → IO Bool + +end Context opaque SSLPointed : NonemptyType @@ -96,6 +106,12 @@ Read from connection. @[extern "lean_ssl_read"] opaque read: @& SSL → USize → IO (Bool × ByteArray) +/-- +Read from connection. +-/ +@[extern "lean_ssl_verify_result"] +opaque verifyResult: @& SSL → IO UInt64 + /-- Get error. -/ @@ -121,12 +137,17 @@ Set read BIO @[extern "lean_ssl_set_rbio"] opaque SSL.setReadBIO : @& SSL → @& BIO → IO Unit -/-- -Set write BIO +/--Set write BIO -/ @[extern "lean_ssl_set_wbio"] opaque SSL.setWriteBIO : @& SSL → @& BIO → IO Unit +/-- +Create a new SSL connection BIO +-/ +@[extern "lean_bio_new_ssl_connect"] +opaque Context.newSSLConnect: @& Context → IO BIO + namespace BIO opaque AddrPointed : NonemptyType @@ -138,6 +159,11 @@ def Addr : Type := AddrPointed.type instance : Nonempty Addr := AddrPointed.property +/-- Initialize an empty BIO +-/ +@[extern "lean_bio_init"] +opaque init : IO BIO + namespace Addr /-- @@ -160,6 +186,18 @@ Read from connection. @[extern "lean_bio_read"] opaque read: @& BIO → USize → IO (Bool × ByteArray) +/-- +Get SSL from BIO. +-/ +@[extern "lean_bio_get_ssl"] +opaque getSSL: BIO → IO SSL + +/-- +Set hostname and optionally the port. +-/ +@[extern "lean_bio_set_conn_hostname"] +opaque setConnHostname: @& BIO → String → IO UInt32 + def Socket := UInt32 /-- @@ -182,9 +220,15 @@ Close a socket. @[extern "lean_bio_closesocket"] opaque close : (socket : Socket) → IO UInt32 - end Socket +/-- +Start the connection. +-/ +@[extern "lean_bio_do_connect"] +opaque doConnect : (bio : @& BIO) → IO UInt32 + + end BIO end OpenSSL diff --git a/test/Tests.lean b/test/Tests.lean index e053203..d616c48 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -2,7 +2,47 @@ import OpenSSL open OpenSSL -def main (args : List String) : IO UInt32 := do +partial def main (args : List String) : IO UInt32 := do + try + println! "Start" + let ctx ← Context.init + let host := "www.google.com" + let bio ← ctx.newSSLConnect + println! "ssl connect" + let res ← bio.setConnHostname s!"{host}:443" + let res ← bio.doConnect + println! "connection started {res}" + let res ← ctx.loadVerifyLocations "/etc/ssl/certs/ca-certificates.crt" "/etc/ssl/certs/" + println! "verify locations {res}" + let ssl ← bio.getSSL + println! "load ssl" + let res ← ssl.verifyResult + println! "verify result {res}" + let req := s!"GET / HTTP/1.1\r\n Host: {host}" + bio.write req.toUTF8 + println! "Request sent: {req}" + let rec read : ByteArray -> IO ByteArray := fun s => do + let (b, ba) ← bio.read 1024 + -- println! "{String.fromUTF8Unchecked ba}" + println! "Read line" + let res := s ++ ba + if b then + read res + else + pure res + + let res ← read ByteArray.empty + -- if ← ssl.isInitFinished then + -- println! "SSL init finished" + -- else + -- println! "SSL init not finished" + + pure 0 + catch e => + IO.eprintln <| "error: " ++ toString e + pure 1 + +def test2 (args : List String) : IO UInt32 := do try let ctx ← Context.init let ssl ← ctx.initSSL