0 | module Network.TLS.Certificate

  2 | import Network.TLS.Parse.DER

  3 | import Network.TLS.Parse.PEM

  4 | import Network.TLS.Parsing

  5 | import Network.TLS.Signature

  6 | import Utils.Misc

  7 | import Utils.Bytes

  8 | import Utils.IPAddr

  9 | import Data.List

 10 | import Data.Vect

 11 | import Data.Bits

 12 | import Data.String.Parser

 13 | import Data.String.Extra

 14 | import Crypto.Hash

 15 | import Decidable.Equality

 16 | import Derive.Prelude

 17 | import Generics.Derive

 19 | %hide Generics.Derive.Eq

 20 | %hide Generics.Derive.Ord

 21 | %hide Generics.Derive.Show

 23 | %language ElabReflection

 25 | public export

 26 | data AttributeType : Type where

 27 |   CommonName : AttributeType

 28 |   Organization : AttributeType

 29 |   OrganizationUnit : AttributeType

 30 |   Country : AttributeType

 31 |   StateOrProvince : AttributeType

 32 |   LocalityName : AttributeType

 33 |   SerialNumber : AttributeType

 34 |   UnknownAttr : List Nat -> AttributeType

 36 | %runElab derive "AttributeType" [Generic, Meta, Eq]

 38 | public export

 39 | Show AttributeType where

 40 |   show CommonName       = "CN"

 41 |   show Organization     = "O"

 42 |   show OrganizationUnit = "OU"

 43 |   show Country          = "C"

 44 |   show StateOrProvince  = "ST"

 45 |   show LocalityName     = "L"

 46 |   show SerialNumber     = "SERIALNUMBER"

 47 |   show (UnknownAttr x)  = show x

 50 | from_oid_attr : List Nat -> AttributeType

 51 | from_oid_attr oid =

 52 |   case map natToInteger oid of

 53 |     [ 2, 5, 4, 3 ]  => CommonName

 54 |     [ 2, 5, 4, 10 ] => Organization

 55 |     [ 2, 5, 4, 11 ] => OrganizationUnit

 56 |     [ 2, 5, 4, 6 ]  => Country

 57 |     [ 2, 5, 4, 8 ]  => StateOrProvince

 58 |     [ 2, 5, 4, 7 ]  => LocalityName

 59 |     [ 2, 5, 4, 5 ]  => SerialNumber 

 60 |     _ => UnknownAttr oid

 62 | public export

 63 | record RelativeDistinguishedName where

 64 |   constructor MkRDN

 65 |   attributes : List (AttributeType, String)

 67 | public export

 68 | record DistinguishedName where

 69 |   constructor MkDN

 70 |   rdns : List RelativeDistinguishedName

 72 | public export

 73 | Eq RelativeDistinguishedName where

 74 |   a == b = (length a.attributes == length b.attributes) && ((a.attributes \\ b.attributes) == [])

 76 | public export

 77 | Eq DistinguishedName where

 78 |   a == b = a.rdns == b.rdns

 81 | dn_attributes : DistinguishedName -> List (AttributeType, String)

 82 | dn_attributes dn = dn.rdns >>= attributes

 84 | public export

 85 | Show DistinguishedName where

 86 |   show dn = join "," $ go <$> dn_attributes dn

 87 |     where

 88 |       go : (AttributeType, String) -> String

 89 |       go (attribute, content) = show attribute <+> "=" <+> content

 91 | extract_attr : ASN1Token -> Maybe (AttributeType, String)

 92 | extract_attr (Universal ** 16 ** Sequence [ (Universal ** 6 ** OID oid), string ]) = (from_oid_attr oid,) <$> extract_string string

 93 | extract_attr _ = Nothing

 95 | extract_rdn : ASN1Token -> Maybe RelativeDistinguishedName

 96 | extract_rdn (Universal ** 17 ** Set attributes) = MkRDN <$> traverse extract_attr attributes

 97 | extract_rdn _ = Nothing

 99 | extract_dn : ASN1Token -> Maybe DistinguishedName

100 | extract_dn (Universal ** 16 ** Sequence rdns) = MkDN <$> traverse extract_rdn rdns

101 | extract_dn _ = Nothing

103 | public export

104 | data ExtensionType : Type where

105 |   BasicConstraint : ExtensionType

106 |   KeyUsage : ExtensionType

107 |   SubjectAltName : ExtensionType

108 |   AuthorityKeyIdentifier : ExtensionType

109 |   UnknownExt : List Nat -> ExtensionType

111 | %runElab derive "ExtensionType" [Generic, Meta, Eq, DecEq, Show]

113 | from_oid_ext : List Nat -> ExtensionType

114 | from_oid_ext oid =

115 |   case map natToInteger oid of

116 |     [ 2, 5, 29, 15 ] => KeyUsage

117 |     [ 2, 5, 29, 19 ] => BasicConstraint

118 |     [ 2, 5, 29, 17 ] => SubjectAltName

119 |     [ 2, 5, 29, 35 ] => AuthorityKeyIdentifier

120 |     _ => UnknownExt oid

122 | public export

123 | record ExtBasicConstraint where

124 |   constructor MkExtBasicConstraint

125 |   ca : Bool

126 |   path_len : Maybe Nat

128 | public export

129 | record ExtKeyUsage where

130 |   constructor MkExtKeyUsage

131 |   digital_signature : Bool

132 |   non_repudiation   : Bool

133 |   key_encipherment  : Bool

134 |   data_encipherment : Bool

135 |   key_agreement     : Bool

136 |   key_cert_sign     : Bool

137 |   crl_sign          : Bool

138 |   encipher_only     : Bool

139 |   decipher_only     : Bool

141 | public export

142 | data GeneralName : Type where

143 |   DNSName : String -> GeneralName

144 |   IPv4Addr : IPv4Addr -> GeneralName

145 |   IPv6Addr : IPv6Addr -> GeneralName

146 |   UnknownGN : ASN1Token -> GeneralName

148 | public export

149 | Show GeneralName where

150 |   show (DNSName dns_name) = "DNS: " <+> dns_name

151 |   show (IPv4Addr addr) = "IP Address: " <+> show addr

152 |   show (IPv6Addr addr) = "IP Address: " <+> show addr

153 |   show (UnknownGN _) = "<unknown>"

155 | public export

156 | Eq GeneralName where

157 |   (DNSName a)  == (DNSName b) = a == b

158 |   (IPv4Addr a) == (IPv4Addr b) = a == b

159 |   (IPv6Addr a) == (IPv6Addr b) = a == b

160 |   _ == _ = False

162 | extract_general_name : ASN1Token -> Either String GeneralName

163 | extract_general_name (ContextSpecific ** 2 ** UnknownPrimitive _ _ str) = Right $ DNSName $ ascii_to_string str

164 | extract_general_name (ContextSpecific ** 7 ** UnknownPrimitive _ _ str) =

165 |   let vec = fromList str

166 |       gn = (IPv4Addr . MkIPv4Addr <$> exactLength 4 vec) <|> (IPv6Addr . MkIPv6Addr <$> exactLength 16 vec)

167 |   in maybe_to_either gn "invalid IP address"

168 | extract_general_name x = Right $ UnknownGN x

170 | public export

171 | record ExtSubjectAltName where

172 |   constructor MkExtSubjectAltName

173 |   general_names : List GeneralName

175 | public export

176 | record ExtAuthorityKeyIdentifier where

177 |   constructor MkExtAuthorityKeyIdentifier

178 |   key_identifier : Maybe (Vect 20 Bits8)

179 |   general_names : List GeneralName

180 |   serial_number : Maybe Integer

182 | extract_auth_key_id : List ASN1Token -> Either String (List ASN1Token, Maybe (Vect 20 Bits8))

183 | extract_auth_key_id [] = Right ([], Nothing)

184 | extract_auth_key_id ((ContextSpecific ** 0 ** UnknownPrimitive _ _ key) :: xs) =

185 |   (\c => (xs, Just c)) <$> (maybe_to_either (exactLength 20 $ fromList key) "invalid key id length")

186 | extract_auth_key_id (x :: xs) = Right ((x :: xs), Nothing)

188 | extract_auth_general_names : List ASN1Token -> Either String (List ASN1Token, List GeneralName)

189 | extract_auth_general_names [] = Right ([], [])

190 | extract_auth_general_names ((ContextSpecific ** 1 ** UnknownConstructed _ _ gns) :: xs) =

191 |   (xs,) <$> traverse extract_general_name gns

192 | extract_auth_general_names (x :: xs) = Right ((x :: xs), [])

194 | extract_auth_serial_no : List ASN1Token -> Either String (Maybe Integer)

195 | extract_auth_serial_no [] = Right Nothing

196 | extract_auth_serial_no ((ContextSpecific ** 2 ** UnknownPrimitive _ _ serial_no) :: []) = do

197 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z serial_no) (parse_integer $ length serial_no)

198 |   | (Pure leftover _) => Left $ "malformed serial number: leftover: " <+> (xxd $ map get leftover)

199 |   | (Fail err) => Left $ show err

200 |   | _ => Left "malformed serial number: underfed"

201 |   pure $ Just ok

202 | extract_auth_serial_no (x :: []) = Right Nothing

203 | extract_auth_serial_no (x :: (y :: ys)) = Left "serial number is followed by unrecognized field"

205 | public export

206 | extension_type : ExtensionType -> Type

207 | extension_type BasicConstraint = ExtBasicConstraint

208 | extension_type KeyUsage = ExtKeyUsage

209 | extension_type SubjectAltName = ExtSubjectAltName

210 | extension_type AuthorityKeyIdentifier = ExtAuthorityKeyIdentifier

211 | extension_type _ = List Bits8

213 | parse_to_extension_type : (t : ExtensionType) -> List Bits8 -> Either String (extension_type t)

214 | parse_to_extension_type BasicConstraint body = do

215 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1

216 |   | (Pure leftover _) => Left $ "malformed basic constraint ext: leftover: " <+> (xxd $ map get leftover)

217 |   | (Fail err) => Left $ show err

218 |   | _ => Left "malformed basic constraint: underfed"

219 |   let ( Universal ** 16 ** Sequence content ) = ok

220 |   | _ => Left "malformed basic constraint: structure error"

221 |   case content of

222 |     [] =>

223 |       Right (MkExtBasicConstraint False Nothing)

224 |     [ (Universal ** 1 ** Boolean ca) ] =>

225 |       Right (MkExtBasicConstraint ca Nothing)

226 |     [ (Universal ** 1 ** Boolean ca), (Universal ** 2 ** IntVal depth) ] =>

227 |       Right (MkExtBasicConstraint ca $ Just $ integerToNat depth)

228 |     _ =>

229 |       Left "malformed basic constraint: structure error"

230 | parse_to_extension_type KeyUsage body = do

231 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1

232 |   | (Pure leftover _) => Left $ "malformed key usage ext: leftover: " <+> (xxd $ map get leftover)

233 |   | (Fail err) => Left $ show err

234 |   | _ => Left "malformed key usage: underfed"

235 |   let (Universal ** 3 ** Bitstring content) = ok

236 |   | _ => Left "malformed key usage: structure error"

237 |   case take 9 ((content.bytes >>= (toList . to_bools_be)) <+> replicate 9 False) of

238 |     [a, b, c, d, e, f, g, h, i] => Right $ MkExtKeyUsage a b c d e f g h i

239 |     _ => Left "impossible"

240 | parse_to_extension_type SubjectAltName body = do

241 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1

242 |   | (Pure leftover _) => Left $ "malformed subject alt name ext: leftover: " <+> (xxd $ map get leftover)

243 |   | (Fail err) => Left $ show err

244 |   | _ => Left "malformed subject alt name: underfed"

245 |   let (Universal ** 16 ** Sequence content) = ok

246 |   | _ => Left "malformed subject alt name: structure error"

247 |   MkExtSubjectAltName <$> traverse extract_general_name content

248 | parse_to_extension_type AuthorityKeyIdentifier body = do

249 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1

250 |   | (Pure leftover _) => Left $ "malformed subject authority key id ext: leftover: " <+> (xxd $ map get leftover)

251 |   | (Fail err) => Left $ show err

252 |   | _ => Left "malformed subject authority key id: underfed"

253 |   let (Universal ** 16 ** Sequence content) = ok

254 |   | _ => Left "malformed subject authority key id: structure error"

256 |   (content, key_id) <- extract_auth_key_id content

257 |   (content, gns) <- extract_auth_general_names content

258 |   sn <- extract_auth_serial_no content

259 |   pure $ MkExtAuthorityKeyIdentifier key_id gns sn

261 | parse_to_extension_type (UnknownExt x) body = Right body

263 | public export

264 | record Extension where

265 |   constructor MkExt

266 |   extension_id : ExtensionType

267 |   critical : Bool

268 |   value : extension_type extension_id

270 | extract_extensions : List ASN1Token -> Either String (List Extension)

271 | extract_extensions [] = Right []

272 | extract_extensions (x :: xs) =

273 |   case last (x :: xs) of

274 |     (ContextSpecific ** 3 ** UnknownConstructed _ _ [ (Universal ** 16 ** Sequence extensions) ]) => traverse extract_ext extensions

275 |     _ => Left "malformed extension list field"

276 |   where

277 |     extract_ext : ASN1Token -> Either String Extension

278 |     extract_ext (Universal ** 16 ** Sequence

279 |                 [ (Universal ** 6 ** OID oid)

280 |                 , (Universal ** 1 ** Boolean critical)

281 |                 , (Universal ** 4 ** OctetString value)

282 |                 ]) = let ext_id = from_oid_ext oid in (MkExt ext_id critical) <$> parse_to_extension_type ext_id value

283 |     extract_ext (Universal ** 16 ** Sequence

284 |                 [ (Universal ** 6 ** OID oid)

285 |                 , (Universal ** 4 ** OctetString value)

286 |                 ]) = let ext_id = from_oid_ext oid in (MkExt ext_id False) <$> parse_to_extension_type ext_id value

287 |     extract_ext _ = Left "malformed extension field"

290 | public export

291 | record Certificate where

292 |   constructor MkCertificate

293 |   serial_number : Integer

294 |   issuer : DistinguishedName

295 |   valid_not_before : Integer

296 |   valid_not_after : Integer

297 |   subject : DistinguishedName

298 |   cert_public_key : PublicKey

299 |   cert_public_key_id : Vect 20 Bits8

300 |   sig_parameter : SignatureParameter 

301 |   signature_value : BitArray

302 |   extensions : List Extension

303 |   tbs_raw_bytes : List Bits8

305 | public export

306 | Show Certificate where

307 |   show cert = "Subject: " <+> show cert.subject <+> " Issuer: " <+> show cert.issuer

310 | certificate_subject_names : Certificate -> List GeneralName

311 | certificate_subject_names cert = go (toList (DNSName <$> common_name)) cert.extensions

312 |   where

313 |     go : List GeneralName -> List Extension -> List GeneralName

314 |     go acc [] = acc

315 |     go acc (x :: xs) =

316 |       case x of

317 |         MkExt SubjectAltName _ ext => go (acc <+> ext.general_names) xs

318 |         _ => go acc xs

319 |     common_name : Maybe String

320 |     common_name = lookup CommonName $ dn_attributes cert.subject

323 | is_self_signed : Certificate -> Bool

324 | is_self_signed cert = cert.issuer == cert.subject

327 | extract_extension : (type : ExtensionType) -> Certificate -> Maybe (extension_type type)

328 | extract_extension type cert = go type cert.extensions

329 |   where

330 |     go : (type : ExtensionType) -> List Extension -> Maybe (extension_type type)

331 |     go type (extension :: xs) =

332 |       case decEq type extension.extension_id of

333 |         Yes ok => Just $ rewrite ok in extension.value

334 |         No _ => go type xs

335 |     go type [] = Nothing

337 | extract_tbs_raw_bytes : List Bits8 -> Either String (List Bits8)

338 | extract_tbs_raw_bytes blob = do

339 |   -- trim outer most layer

340 |   let (Pure outer _) = feed (map (uncurry MkPosed) $ enumerate Z blob) (parse_tag_id *> parse_length)

341 |   | (Fail err) => Left $ show err

342 |   | _ => Left "malformed certificate: underfed"

343 |   -- get the inner information

344 |   let (Pure inner len) = feed outer (parse_tag_id *> parse_length)

345 |   | (Fail err) => Left $ show err

346 |   | _ => Left "malformed tbs certificate: underfed"

348 |   let metadata = take (minus (length outer) (length inner)) outer

349 |   pure (map get metadata <+> map get (take len inner))

352 | parse_certificate : List Bits8 -> Either String Certificate

353 | parse_certificate blob = do

354 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z blob) parse_asn1

355 |   | (Pure leftover _) => Left $ "malformed certificate: leftover: " <+> (xxd $ map get leftover)

356 |   | (Fail err) => Left $ show err

357 |   | _ => Left "malformed certificate: underfed"

359 |   let (Universal ** 16 ** Sequence

360 |         [ (Universal ** 16 ** Sequence

361 |           ( (ContextSpecific ** 0 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal 2) ])

362 |           :: (Universal ** 2 ** IntVal serial_number)

363 |           :: crt_algorithm

364 |           :: issuer

365 |           :: (Universal ** 16 ** Sequence valid_period)

366 |           :: subject

367 |           :: certificate_public_key

368 |           :: optional_fields

369 |           ))

370 |         , crt_signature_algorithm

371 |         , (Universal ** 3 ** Bitstring signature_value)

372 |         ]

373 |       ) = ok

374 |   | _ => Left "malformed certificate"

376 |   let Just [ valid_not_before, valid_not_after ] = traverse {f=Maybe} extract_epoch valid_period

377 |   | _ => Left "malformed validity timestamp"

379 |   (key_id, key) <- extract_key' certificate_public_key

381 |   crt_algorithm <- maybe_to_either (extract_algorithm crt_algorithm) "malformed certificate algorithm"

382 |   crt_signature_algorithm <- maybe_to_either (extract_algorithm crt_signature_algorithm) "malformed certificate signature algorithm"

384 |   let True = fst crt_algorithm == fst crt_signature_algorithm

385 |   | False => Left "tbsCertificate signature field does not match signature algorithm"

387 |   sig_param <- uncurry extract_signature_parameter crt_algorithm

389 |   issuer <- maybe_to_either (extract_dn issuer) "malformed issuer"

390 |   subject <- maybe_to_either (extract_dn subject) "malformed subject"

392 |   extensions <- extract_extensions optional_fields

394 |   raw_tbs_bytes <- extract_tbs_raw_bytes blob

396 |   pure $

397 |     MkCertificate

398 |       serial_number

399 |       issuer

400 |       valid_not_before

401 |       valid_not_after

402 |       subject

403 |       key

404 |       key_id

405 |       sig_param

406 |       signature_value

407 |       extensions

408 |       raw_tbs_bytes