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/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/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/flake.lock b/flake.lock index 609bea7..de02264 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "flake-utils": { "locked": { - "lastModified": 1638122382, - "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", "owner": "numtide", "repo": "flake-utils", - "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", "type": "github" }, "original": { @@ -33,18 +33,16 @@ "lean": { "inputs": { "flake-utils": "flake-utils", - "lean-stage0": "lean-stage0", - "mdBook": "mdBook", + "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": "nixpkgs_2", - "temci": "temci" + "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1640275476, - "narHash": "sha256-Z0m/6dHimfA9bIGrCJusbN7x1slY7y8uGaDlWhMjRB4=", + "lastModified": 1676133667, + "narHash": "sha256-vD5dUMRYcgdQTHiRtR+HaTyR/1HhSIF5UZzIHSBgAyk=", "owner": "leanprover", "repo": "lean4", - "rev": "70ef4e529c85eeffa15a9a5eeca290a13f484efd", + "rev": "c826168cfa79d421c0723d5fbdd840595c29fe3a", "type": "github" }, "original": { @@ -53,18 +51,19 @@ "type": "github" } }, - "lean-stage0": { + "lean4-mode": { + "flake": false, "locked": { - "lastModified": 0, - "narHash": "sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=", + "lastModified": 1659020985, + "narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=", "owner": "leanprover", - "repo": "lean4", - "rev": "0000000000000000000000000000000000000000", + "repo": "lean4-mode", + "rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6", "type": "github" }, "original": { "owner": "leanprover", - "repo": "lean4", + "repo": "lean4-mode", "type": "github" } }, @@ -84,25 +83,12 @@ "type": "github" } }, - "mdBook": { - "flake": false, - "locked": { - "lastModified": 1637318029, - "narHash": "sha256-XU6oQY46mLqLdMp9ONR9WSEBVaA3627cGfzB218Wul0=", - "owner": "leanprover", - "repo": "mdBook", - "rev": "45de7509526f09915b19e4eaeec99c8c2031f1ce", - "type": "github" - }, - "original": { - "owner": "leanprover", - "repo": "mdBook", - "type": "github" - } - }, "naersk": { "inputs": { - "nixpkgs": "nixpkgs_4" + "nixpkgs": [ + "utils", + "nixpkgs" + ] }, "locked": { "lastModified": 1618844365, @@ -121,14 +107,15 @@ "nix": { "inputs": { "lowdown-src": "lowdown-src", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs", + "nixpkgs-regression": "nixpkgs-regression" }, "locked": { - "lastModified": 1638447470, - "narHash": "sha256-DREkiGilBlNzBqonvVrIBNSsYWv1PZuvfXFhaSGeXsM=", + "lastModified": 1657097207, + "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", "owner": "NixOS", "repo": "nix", - "rev": "2ff71b021379a2c9bbdcb789a93cdc585b3520ca", + "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", "type": "github" }, "original": { @@ -139,63 +126,66 @@ }, "nixpkgs": { "locked": { - "lastModified": 1632864508, - "narHash": "sha256-d127FIvGR41XbVRDPVvozUPQ/uRHbHwvfyKHwEt5xFM=", + "lastModified": 1653988320, + "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "82891b5e2c2359d7e58d08849e4c89511ab94234", + "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", "type": "github" }, "original": { - "id": "nixpkgs", - "ref": "nixos-21.05-small", - "type": "indirect" + "owner": "NixOS", + "ref": "nixos-22.05-small", + "repo": "nixpkgs", + "type": "github" } }, - "nixpkgs_2": { + "nixpkgs-regression": { "locked": { - "lastModified": 1638397275, - "narHash": "sha256-2Jos1CJFTMO9IbulbM4PTKn24nISIDQCAG/AqYQ8rmg=", + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "391f93a83c3a486475d60eb4a569bb6afbf306ad", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixpkgs-unstable", "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", "type": "github" } }, - "nixpkgs_3": { + "nixpkgs_2": { "locked": { - "lastModified": 1640169700, - "narHash": "sha256-Y+WR7cpiUTroEtoGR8Q3KMbFARvOiACLLmNQ+/iEz2E=", - "owner": "nixos", + "lastModified": 1657208011, + "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "3f0e4de0c2d2c85d7abce260f8c17c8ef5b78e5b", + "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2", "type": "github" }, "original": { - "owner": "nixos", - "ref": "nixos-21.05", + "owner": "NixOS", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", "type": "github" } }, - "nixpkgs_4": { + "nixpkgs_3": { "locked": { - "lastModified": 1640234302, - "narHash": "sha256-dALA+cOam5jQ2KOYdWiv6H6Y2stcYG6eclWQQVGx/FI=", - "owner": "NixOS", + "lastModified": 1676973346, + "narHash": "sha256-rft8oGMocTAhUVqG3LW6I8K/Fo9ICGmNjRqaWTJwav0=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "81cbfc8f2a1e218249b7bff74013b63150171496", + "rev": "d0d55259081f0b97c828f38559cad899d351cad1", "type": "github" }, "original": { - "id": "nixpkgs", - "type": "indirect" + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" } }, "root": { @@ -205,22 +195,6 @@ "utils": "utils" } }, - "temci": { - "flake": false, - "locked": { - "lastModified": 1638195132, - "narHash": "sha256-1DSg4Qr5h54wLrKpZfpkArhFXDFLdO57PiYUMk+7FSc=", - "owner": "parttimenerd", - "repo": "temci", - "rev": "a8d78cb52c248f1ae3f2469bbd0916b14ac9ea84", - "type": "github" - }, - "original": { - "owner": "parttimenerd", - "repo": "temci", - "type": "github" - } - }, "utils": { "inputs": { "flake-utils": "flake-utils_2", @@ -230,11 +204,11 @@ ] }, "locked": { - "lastModified": 1638966113, - "narHash": "sha256-0xH1+2FxKm02tny4AsArtN2xHdjN637spCsar7ks7ZM=", + "lastModified": 1648465689, + "narHash": "sha256-uLj4w3Fed3cEC3tLvYOi869/n0+bkHLiNpAuZO+ozjY=", "owner": "yatima-inc", "repo": "nix-utils", - "rev": "8dc43e9ede4af7d9f25512a453a9631fb4259ef0", + "rev": "f946f004282a29e83778135de1c2e54ffb60a97d", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index fafc166..1eab075 100644 --- a/flake.nix +++ b/flake.nix @@ -1,11 +1,11 @@ { - description = "Openssl bindings for Lean"; + description = "OpenSSL bindings for Lean"; inputs = { lean = { url = github:leanprover/lean4; }; - nixpkgs.url = github:nixos/nixpkgs/nixos-21.05; + nixpkgs.url = github:nixos/nixpkgs/nixos-unstable; utils = { url = github:yatima-inc/nix-utils; inputs.nixpkgs.follows = "nixpkgs"; @@ -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" @@ -28,12 +28,14 @@ leanPkgs = lean.packages.${system}; pkgs = nixpkgs.legacyPackages.${system}; inherit (lib.${system}) buildCLib concatStringsSep; - includes = [ "${pkgs.openssl.dev}/include" "${leanPkgs.lean-bin-tools-unwrapped}/include" ]; + includes = + [ "${pkgs.openssl.dev}/include" "${leanPkgs.lean-bin-tools-unwrapped}/include" ./native ]; INCLUDE_PATH = concatStringsSep ":" includes; libssl = (pkgs.openssl.out // { name = "lib/libssl.so"; linkName = "ssl"; libName = "libssl.so"; + __toString = d: "${d.out}/lib"; }); c-shim = buildCLib { updateCCOptions = d: d ++ (map (i: "-I${i}") includes); @@ -41,46 +43,70 @@ sharedLibDeps = [ libssl ]; - src = ./bindings; + src = ./native; extraDrvArgs = { linkName = "lean-openssl-bindings"; }; }; + c-shim-debug = c-shim.override { + debug = true; + 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 // { __toString = d: "${libssl}/lib"; }) c-shim ]; + nativeSharedLibs = [ libssl c-shim ]; src = ./src; }; + Cli = leanPkgs.buildLeanPackage + { + name = "Main"; + deps = [ OpenSSL ]; + 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; }; - joinDepsDerivationns = getSubDrv: - pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") ([ project ] ++ project.allExternalDeps)); + test-debug = test.override { + debug = true; + deps = [ project-debug ]; + }; + joinDepsDerivations = getSubDrv: + pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") (OpenSSL.allExternalDeps)); in { - inherit project test; + project = OpenSSL; packages = { - ${name} = project.executable; + inherit OpenSSL Cli; + inherit (OpenSSL) lean-package; + test = test.executable; + test-debug = test-debug.executable; }; checks.test = test.executable; - defaultPackage = self.packages.${system}.${name}; - devShell = pkgs.mkShell { - inputsFrom = [ project.executable ]; + defaultPackage = self.packages.${system}.Cli.executable; + devShells.default = pkgs.mkShell { + # inputsFrom = [ OpenSSL.executable ]; buildInputs = with pkgs; [ - leanPkgs.lean + elan + openssl + pkg-config + # leanPkgs.lean-dev ]; - LEAN_PATH = joinDepsDerivationns (d: d.modRoot); - LEAN_SRC_PATH = joinDepsDerivationns (d: d.src); + OPENSSL_DIR = "${pkgs.openssl.out}"; + # 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/lakefile.lean b/lakefile.lean index 25e7d3f..72cc3b3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,12 +2,15 @@ import Lake open Lake DSL package OpenSSL { - precompileModules := true - moreLinkArgs := #["-L", "-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" @@ -19,10 +22,14 @@ 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, - "/usr/include/openssl", "-fPIC"] + "-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC", "-g"] compileO ffiSrc oFile srcFile flags -extern_lib ffi (pkg : Package) := do +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/native/lean_utils.h b/native/lean_utils.h new file mode 100644 index 0000000..1f65be5 --- /dev/null +++ b/native/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/native/native.c b/native/native.c index 9c1c25b..d31d49f 100644 --- a/native/native.c +++ b/native/native.c @@ -1,4 +1,5 @@ -#include "lean/lean.h" +#include +#include "lean_utils.h" #include #include @@ -14,368 +15,389 @@ #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_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_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); + 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)); +} +/** + * 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)); +} -inline static void noop(void *mod, b_lean_obj_arg fn) {} - +// SSL -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; + 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)); +} - while (len > 0) { - n = BIO_write(client.rbio, src, len); +/** + * 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) +{ + 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)); +} - if (n<=0) - return -1; /* assume bio write failure is unrecoverable */ +/** + * 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) +{ + 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)); +} - src += n; - len -= n; +/** + * 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)); +} - if (!SSL_is_init_finished(client.ssl)) { - if (do_ssl_handshake() == SSLSTATUS_FAIL) - return -1; - if (!SSL_is_init_finished(client.ssl)) - return 0; - } +/** + * 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)); +} - /* The encrypted data is now in the input bio so now we can perform actual - * read of unencrypted data. */ +// BIO - do { - n = SSL_read(client.ssl, buf, sizeof(buf)); - if (n > 0) - client.io_on_read(buf, (size_t)n); - } while (n > 0); +static inline void bio_finalize(void *bio) +{ + BIO_free_all(bio); +} - status = get_sslstatus(client.ssl, n); +static lean_external_class *g_bio_class = 0; - /* 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); +static lean_external_class *get_bio_class() { + if (g_bio_class == 0) { + g_bio_class = lean_register_external_class( + &bio_finalize, &foreach_noop + ); + } + return g_bio_class; +} - if (status == SSLSTATUS_FAIL) - return -1; +/** + * Create a BIO* struct. + * BIO.init : IO BIO + */ +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)); +} - return 0; +/** + * BIO.read : @& BIO → USize → IO (Bool × ByteArray) + */ +lean_obj_res lean_bio_read(b_lean_obj_arg l_bio, size_t len) +{ + BIO* bio = lean_get_external_data(l_bio); + lean_object* bs = lean_alloc_sarray(1, len, len); + uint8_t* buf = lean_sarray_cptr(bs); + bool b = BIO_read(bio, 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() +/** + * BIO.write : @& BIO → @& ByteArray → IO Unit + */ +lean_obj_res lean_bio_write(b_lean_obj_arg l_bio, b_lean_obj_arg bs) { - char buf[DEFAULT_BUF_SIZE]; - enum sslstatus status; + BIO* bio = lean_get_external_data(l_bio); + uint8_t* buf = lean_sarray_cptr(bs); + size_t len = lean_sarray_size(bs); + bool b = BIO_write(bio, buf, len); + return lean_io_result_mk_ok(lean_box(b)); +} - if (!SSL_is_init_finished(client.ssl)) - return 0; +/** + * 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)); +} - 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); - } +static inline void bio_addr_finalize(void *bio) +{ + BIO_ADDR_free(bio); +} - if (status == SSLSTATUS_FAIL) - return -1; +static lean_external_class *g_bio_addr_class = 0; - if (n==0) - break; +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 0; + return g_bio_addr_class; } -/* Read bytes from stdin and queue for later encryption. */ -void do_stdin_read() +/** + * Create a BIO_ADDR* struct. + * BIO.init : IO BIO + */ +lean_obj_res lean_bio_addr_init() { - char buf[DEFAULT_BUF_SIZE]; - ssize_t n = read(STDIN_FILENO, buf, sizeof(buf)); - if (n>0) - send_unencrypted_bytes(buf, (size_t)n); + 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)); } -/* Read encrypted bytes from socket. */ -int do_sock_read() +/** + * BIO.socket : UInt32 -> UInt32 -> UInt32 -> IO UInt32 + */ +lean_obj_res lean_bio_socket(uint32_t domain, uint32_t socktype, uint32_t protocol) { - char buf[DEFAULT_BUF_SIZE]; - ssize_t n = read(client.fd, buf, sizeof(buf)); + 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)); + } +} - if (n>0) - return on_read_cb(buf, (size_t)n); - else - return -1; +/** + * 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)); } -/* Write encrypted bytes to the socket. */ -int do_sock_write() +/** + * BIO.newSSLConnect (ctx : Context) : IO BIO + */ +lean_obj_res lean_bio_new_ssl_connect(lean_obj_arg context) { - ssize_t n = write(client.fd, client.write_buf, client.write_len); - if (n>0) { - if ((size_t)n + IO.eprintln <| "error: " ++ toString e + pure 1 diff --git a/test/Tests.lean b/test/Tests.lean new file mode 100644 index 0000000..d616c48 --- /dev/null +++ b/test/Tests.lean @@ -0,0 +1,63 @@ +import OpenSSL + +open OpenSSL + +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 + 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 + pure 1 +