Ssh algorithms

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
use "../ssh_error"

primitive SshAlgorithmDefaults
  """
  The per-category default algorithm lists. These back both the constructor
  defaults of SshAlgorithmPreferences and SshDefaultAlgorithms.preferences, so
  the two never drift, and they list only algorithms the transport implements.
  """
  fun kex(): Array[String val] val =>
    recover val let a = Array[String val]; a.push("curve25519-sha256"); a end

  fun host_key(): Array[String val] val =>
    recover val let a = Array[String val]; a.push("ssh-ed25519"); a end

  fun ciphers(): Array[String val] val =>
    recover val
      let a = Array[String val]
      a.push("chacha20-poly1305@openssh.com")
      a.push("aes256-gcm@openssh.com")
      a.push("aes128-gcm@openssh.com")
      a.push("aes256-ctr")
      a
    end

  fun macs(): Array[String val] val =>
    recover val
      let a = Array[String val]
      a.push("hmac-sha2-256")
      a.push("hmac-sha2-512")
      a
    end

class val SshAlgorithmPreferences
  """
  Per-category algorithm preference lists. Every parameter defaults to the
  implemented set, so construct with named arguments and override only what
  differs — e.g. `SshAlgorithmPreferences(where cipher_client_to_server' =
  my_ciphers, cipher_server_to_client' = my_ciphers)`. Passing all six lists
  positionally is error-prone (they share a type, so a transposition compiles
  silently); prefer named arguments.
  """
  let kex: Array[String val] val
  let host_key: Array[String val] val
  let cipher_client_to_server: Array[String val] val
  let cipher_server_to_client: Array[String val] val
  let mac_client_to_server: Array[String val] val
  let mac_server_to_client: Array[String val] val

  new val create(
    kex': Array[String val] val = SshAlgorithmDefaults.kex(),
    host_key': Array[String val] val = SshAlgorithmDefaults.host_key(),
    cipher_client_to_server': Array[String val] val =
      SshAlgorithmDefaults.ciphers(),
    cipher_server_to_client': Array[String val] val =
      SshAlgorithmDefaults.ciphers(),
    mac_client_to_server': Array[String val] val = SshAlgorithmDefaults.macs(),
    mac_server_to_client': Array[String val] val = SshAlgorithmDefaults.macs())
  =>
    kex = kex'
    host_key = host_key'
    cipher_client_to_server = cipher_client_to_server'
    cipher_server_to_client = cipher_server_to_client'
    mac_client_to_server = mac_client_to_server'
    mac_server_to_client = mac_server_to_client'

class val SshNegotiatedAlgorithms
  """The single algorithm chosen per category once negotiation completes."""
  let kex: String val
  let host_key: String val
  let cipher_c2s: String val
  let cipher_s2c: String val
  let mac_c2s: String val
  let mac_s2c: String val

  new val create(
    kex': String val, host_key': String val,
    cipher_c2s': String val, cipher_s2c': String val,
    mac_c2s': String val, mac_s2c': String val)
  =>
    kex = kex'; host_key = host_key'
    cipher_c2s = cipher_c2s'; cipher_s2c = cipher_s2c'
    mac_c2s = mac_c2s'; mac_s2c = mac_s2c'

primitive SshAlgorithmNegotiation
  fun negotiate(client: SshAlgorithmPreferences val,
    server: SshAlgorithmPreferences val):
    (SshNegotiatedAlgorithms val | SshAlgorithmNegotiationFailed)
  =>
    """First client preference that server also supports, per category (RFC 4253 §7.1)."""
    let k = _negotiate_one(client.kex, server.kex)
    let hk = _negotiate_one(client.host_key, server.host_key)
    let cc2s = _negotiate_one(client.cipher_client_to_server, server.cipher_client_to_server)
    let cs2c = _negotiate_one(client.cipher_server_to_client, server.cipher_server_to_client)
    let mc2s = _negotiate_one(client.mac_client_to_server, server.mac_client_to_server)
    let ms2c = _negotiate_one(client.mac_server_to_client, server.mac_server_to_client)

    match (k, hk, cc2s, cs2c, mc2s, ms2c)
    | (let k': String val, let hk': String val,
       let cc': String val, let cs': String val,
       let mc': String val, let ms': String val) =>
      SshNegotiatedAlgorithms(k', hk', cc', cs', mc', ms')
    else
      SshAlgorithmNegotiationFailed
    end

  fun _negotiate_one(client_prefs: Array[String val] val,
    server_prefs: Array[String val] val): (String val | None)
  =>
    for c in client_prefs.values() do
      for s in server_prefs.values() do
        if c == s then return c end
      end
    end
    None

primitive SshSupportedAlgorithms
  """
  The algorithms this transport can actually perform. Negotiation must not
  commit to anything outside these sets: the key-exchange code runs X25519
  unconditionally and the cipher code dispatches on these exact names, so a
  negotiated name we cannot run would either die mid-handshake or, worse, leave
  the negotiated name in the exchange hash disagreeing with the math performed.
  """
  fun kex(name: String val): Bool =>
    (name == "curve25519-sha256")
      or (name == "curve25519-sha256@libssh.org")

  fun host_key(name: String val): Bool =>
    name == "ssh-ed25519"

  fun cipher(name: String val): Bool =>
    // aes128-cbc is deliberately absent: CBC (encrypt-and-MAC over plaintext)
    // is the construction the Terrapin / CBC-padding-oracle attacks target, so
    // it is not negotiable even if a consumer lists it in their preferences.
    (name == "chacha20-poly1305@openssh.com")
      or (name == "aes256-gcm@openssh.com")
      or (name == "aes128-gcm@openssh.com")
      or (name == "aes256-ctr")

  fun mac(name: String val): Bool =>
    (name == "hmac-sha2-256") or (name == "hmac-sha2-512")

  fun supports_all(n: SshNegotiatedAlgorithms val): Bool =>
    """True only when every negotiated algorithm is one this transport runs."""
    kex(n.kex) and host_key(n.host_key)
      and cipher(n.cipher_c2s) and cipher(n.cipher_s2c)
      and mac(n.mac_c2s) and mac(n.mac_s2c)

primitive SshStrictKex
  """
  The OpenSSH strict key-exchange extension (Terrapin / CVE-2023-48795
  mitigation). Each side advertises a role-specific marker as a pseudo
  key-exchange algorithm in its first KEXINIT only. When both sides advertise
  it, strict KEX is in effect: the packet sequence number is reset to zero at
  every NEWKEYS, and no non-key-exchange packets are tolerated during the
  initial key exchange. The marker is appended last so it never wins
  negotiation against a real algorithm.
  """
  fun client_marker(): String val => "kex-strict-c-v00@openssh.com"
  fun server_marker(): String val => "kex-strict-s-v00@openssh.com"

  fun our_marker(role: SshRole): String val =>
    """The marker this side advertises, by role."""
    match role
    | SshRoleClient => client_marker()
    | SshRoleServer => server_marker()
    end

  fun initial_kexinit_position_ok(reader_sequence_after_read: U32): Bool =>
    """
    Under strict KEX the peer's KEXINIT must be the very first binary packet of
    the connection. The reader increments its sequence number as each packet is
    read, so when we process that KEXINIT the reader's sequence number is exactly
    1 if nothing preceded it. A larger value means a packet was injected before
    the KEXINIT (e.g. an SSH_MSG_IGNORE) — the pre-KEXINIT half of the Terrapin
    attack (CVE-2023-48795) — and the connection must abort.
    """
    reader_sequence_after_read == 1

  fun peer_advertised(their_kexinit: Array[U8] val, our_role: SshRole): Bool =>
    """
    True if the peer's KEXINIT advertised the strict-KEX marker for its role.
    We always advertise ours, so — since strict KEX requires both sides — this
    is exactly whether strict KEX is in effect for the connection.
    """
    let peer_marker =
      match our_role
      | SshRoleClient => server_marker()
      | SshRoleServer => client_marker()
      end
    try
      match SshMessages.decode_kexinit(their_kexinit)?
      | let prefs: SshAlgorithmPreferences val =>
        for name in prefs.kex.values() do
          if name == peer_marker then return true end
        end
        false
      | None => false
      end
    else
      false
    end

primitive SshDefaultAlgorithms
  fun preferences(): SshAlgorithmPreferences val =>
    """
    The default preferences: only algorithms the transport implements, in
    descending preference. Identical to a default-constructed
    SshAlgorithmPreferences; both draw from SshAlgorithmDefaults.
    """
    SshAlgorithmPreferences