1 import Base 2 import ./proxy.bend as P 3 4 # Net 5 # === 6 # 7 # A TLS connection is a Socket handle wrapped in Tls, so code typed against 8 # Tls can never hand it to the raw TCP effects. The effects (effs/tls.c on 9 # native builds, effs/tls.js on the JavaScript lane) only dial, handshake 10 # and move bytes; every decision about proxies is proxy.bend's, here. 11 12 type Tls is Type: 13 Tls{sock: Socket} 14 15 type Bytes is Data: 16 Bytes{list: List<&2, U32>} 17 18 def Res(-A: Type) -> Type: 19 Result<&1, &1, U32 & String, A> 20 21 # Effects 22 # ------- 23 24 # A plain TCP connection: host may be a name (resolved, IPv4 or IPv6) or an 25 # IP literal; ms bounds the connect (0 for 30s). Until Tls.secure, Tls.send 26 # and Tls.recv carry its bytes as they are. 27 def Tls.dial(host: String, port: U32, ms: U32) -> IO(Res(Socket)): 28 import "./effs/tls.c" 29 import "./effs/tls.js" 30 31 # Handshakes on a connection from Tls.dial and verifies the server as host 32 # (a name, or an IP literal), always: ca is a PEM bundle of trusted roots 33 # ("" for the system's), cert and key a PEM client certificate and key ("" 34 # for none), ms the handshake's deadline (0 for 30s). TLS 1.2 or later. A 35 # failure closes the connection. 36 def Tls.secure(sock: Socket, host: String, ca: String, cert: String, key: String, ms: U32) -> 37 IO(Res(Socket)): 38 import "./effs/tls.c" 39 import "./effs/tls.js" 40 41 # Sends text as UTF-8; ms bounds the whole send (0: no deadline). 42 def Tls.send(sock: Socket, text: String, ms: U32) -> IO(Socket & Res(Unit)): 43 import "./effs/tls.c" 44 import "./effs/tls.js" 45 46 # Up to max bytes (0: 16KiB); an empty list is the end of the stream. ms 47 # bounds the wait (0: none), past which it fails with ETIMEDOUT (60). 48 def Tls.recv(sock: Socket, max: U32, ms: U32) -> IO(Socket & Res(List<&2, U32>)): 49 import "./effs/tls.c" 50 import "./effs/tls.js" 51 52 def Tls.close(sock: Socket) -> IO(Unit): 53 import "./effs/tls.c" 54 import "./effs/tls.js" 55 56 # Opening 57 # ------- 58 59 def Tls.fail(s: Socket, e: U32 & String) -> IO(Res(Socket)): 60 IO.bind(Unit, Res(Socket), Tls.close(s), u => IO.pure(Res(Socket), Fail{e})) 61 62 # What the CONNECT exchange just saw. 63 type TunEv is Type: 64 TGot{sock: Socket, r: Res(List<&2, U32>), st: P.Tunnel} 65 TStep{sock: Socket, st: P.Tunnel} 66 67 def TunEv.got(p: Socket & Res(List<&2, U32>), st: P.Tunnel) -> TunEv: 68 match p: 69 case (s, r): 70 TGot{s, r, st} 71 72 # Reads the proxy's answer to CONNECT; once it opens the tunnel, secures 73 # the connection end to end with the API server. 74 def Tls.tunnel(fuel: Nat, ev: TunEv, +host: String, ca: String, cert: String, key: String, 75 +ms: U32) -> IO(Res(Socket)): 76 match fuel ev: 77 case 0n TGot{s, r, st}: 78 Tls.fail(s, (0, "proxy: answer too long")) 79 case 0n TStep{s, st}: 80 Tls.fail(s, (0, "proxy: answer too long")) 81 case 1n+f TGot{s, Done{bs}, st}: 82 Tls.tunnel(f, TStep{s, P.Tunnel.feed(st, bs)}, host, ca, cert, key, ms) 83 case 1n+f TGot{s, Fail{(c, m)}, st}: 84 Tls.fail(s, (c, "proxy: " ++ m)) 85 case 1n+f TStep{s, P.TMore{h}}: 86 IO.bind(Socket & Res(List<&2, U32>), Res(Socket), Tls.recv(s, 4096, ms), 87 p => Tls.tunnel(f, TunEv.got(p, P.TMore{h}), host, ca, cert, key, ms)) 88 case 1n+f TStep{s, P.TOpen{}}: 89 Tls.secure(s, host, ca, cert, key, ms) 90 case 1n+f TStep{s, P.TFail{why}}: 91 Tls.fail(s, (0, why)) 92 93 def Tls.open.sent(p: Socket & Res(Unit), +host: String, ca: String, cert: String, key: String, 94 +ms: U32) -> IO(Res(Socket)): 95 match p: 96 case (s, Done{u}): 97 Tls.tunnel(4294967295n, TStep{s, P.Tunnel.init()}, host, ca, cert, key, ms) 98 case (s, Fail{(c, m)}): 99 Tls.fail(s, (c, "proxy: " ++ m)) 100 101 def Tls.open.proxied(d: Res(Socket), req: String, +host: String, ca: String, cert: String, 102 key: String, +ms: U32) -> IO(Res(Socket)): 103 match d: 104 case Done{s}: 105 IO.bind(Socket & Res(Unit), Res(Socket), Tls.send(s, req, ms), 106 p => Tls.open.sent(p, host, ca, cert, key, ms)) 107 case Fail{(c, m)}: 108 IO.pure(Res(Socket), Fail{(c, "proxy: " ++ m)}) 109 110 def Tls.open.direct(d: Res(Socket), +host: String, ca: String, cert: String, key: String, 111 +ms: U32) -> IO(Res(Socket)): 112 match d: 113 case Done{s}: 114 Tls.secure(s, host, ca, cert, key, ms) 115 case Fail{e}: 116 IO.pure(Res(Socket), Fail{e}) 117 118 def Tls.open.route(r: P.Route, +host: String, +port: U32, ca: String, cert: String, 119 key: String, +ms: U32) -> IO(Res(Socket)): 120 match r: 121 case P.Direct{}: 122 IO.bind(Res(Socket), Res(Socket), Tls.dial(host, port, ms), 123 d => Tls.open.direct(d, host, ca, cert, key, ms)) 124 case P.Via{P.Proxy{ph, pp, auth}}: 125 IO.bind(Res(Socket), Res(Socket), Tls.dial(ph, pp, ms), 126 d => Tls.open.proxied(d, P.Proxy.connect(host, port, auth), host, ca, cert, key, ms)) 127 case P.NoRoute{why}: 128 IO.pure(Res(Socket), Fail{(22, why)}) 129 130 def Tls.env.or(r: Res(String), alt: Res(String)) -> String: 131 match r alt: 132 case Done{SCon{c, t}} a: 133 SCon{c, t} 134 case _ Done{v}: 135 v 136 case _ _: 137 "" 138 139 # The first of two environment variables that is set and not empty, as Go 140 # reads HTTPS_PROXY then https_proxy. 141 def Tls.env(name: String, alt: String) -> IO(String): 142 IO.bind(Res(String), String, IO.get_env(name), 143 r => IO.bind(Res(String), String, IO.get_env(alt), a => IO.pure(String, Tls.env.or(r, a)))) 144 145 # Opens a verified TLS connection to host:port (see Tls.secure), through 146 # the CONNECT tunnel of HTTPS_PROXY unless NO_PROXY or a loopback host 147 # says otherwise (proxy.bend). 148 def Tls.open(+host: String, +port: U32, ca: String, cert: String, key: String, +ms: U32) -> 149 IO(Res(Socket)): 150 IO.bind(String, Res(Socket), Tls.env("HTTPS_PROXY", "https_proxy"), 151 url => IO.bind(String, Res(Socket), Tls.env("NO_PROXY", "no_proxy"), 152 no => Tls.open.route(P.Proxy.route(url, no, host, port), host, port, ca, cert, key, ms)))