0 | module Network.TLS.Verify
  1 |
  2 | import Network.TLS.Core
  3 | import Network.TLS.Certificate
  4 | import Network.TLS.Signature
  5 | import Network.TLS.Handshake
  6 | import Network.TLS.Parse.DER
  7 | import Utils.Misc
  8 | import Utils.Bytes
  9 | import Data.String
 10 | import Data.List
 11 | import Data.List.Lazy
 12 | import Data.List1
 13 | import Data.Vect
 14 | import Utils.IPAddr
 15 | import Data.Either
 16 | import System
 17 | import Control.Monad.Error.Either
 18 | import Control.Monad.Trans
 19 |
 20 | %hide Network.TLS.Handshake.Message.Certificate
 21 |
 22 | ||| Takes a wildcard domain like "*.google.com" and creates
 23 | ||| a function to check if a string matches the wildcard domain
 24 | domain_predicate : String -> Maybe (String -> Bool)
 25 | domain_predicate predicate = do
 26 |   let parts = split ('.' ==) predicate
 27 |   guard $ verify_predicate parts
 28 |   Just (apply_predicate parts . split ('.' == ))
 29 |   where
 30 |     str_eq : String -> String -> Lazy Bool
 31 |     str_eq "*" _ = delay True
 32 |     str_eq _ "*" = delay True
 33 |     str_eq a b = delay (a == b)
 34 |     apply_predicate : List1 String -> List1 String -> Bool
 35 |     apply_predicate a b = (length a == length b) && (and $ zipWith str_eq a b)
 36 |     verify_predicate : List1 String -> Bool
 37 |     verify_predicate ("*" ::: []) = False
 38 |     verify_predicate ("*" ::: [_]) = False
 39 |     verify_predicate ("*" ::: [_, ""]) = False
 40 |     verify_predicate ("*" ::: xs) = and $ map (delay . not . isInfixOf "*") xs
 41 |     verify_predicate xs = and $ map (delay . not . isInfixOf "*") (toList xs)
 42 |
 43 | domain_predicate' : String -> (String -> Bool)
 44 | domain_predicate' predicate =
 45 |   case domain_predicate predicate of
 46 |     Nothing => const False
 47 |     Just f => f
 48 |
 49 | ||| Type of identifier that will be used to check if a certificate's common name matches
 50 | ||| the supplied hostname
 51 | Identifier : Type
 52 | Identifier = Eithers [IPv4Addr, IPv6Addr, String]
 53 |
 54 | check_ipv4_address : List GeneralName -> IPv4Addr -> Bool
 55 | check_ipv4_address (IPv4Addr addr' :: xs) addr = if addr == addr' then True else check_ipv4_address xs addr
 56 | check_ipv4_address (x :: xs) addr = check_ipv4_address xs addr
 57 | check_ipv4_address [] _ = False
 58 |
 59 | check_ipv6_address : List GeneralName -> IPv6Addr -> Bool
 60 | check_ipv6_address (IPv6Addr addr' :: xs) addr = if addr == addr' then True else check_ipv6_address xs addr
 61 | check_ipv6_address (x :: xs) addr = check_ipv6_address xs addr
 62 | check_ipv6_address [] _ = False
 63 |
 64 | check_dns_name : List GeneralName -> String -> Bool
 65 | check_dns_name (DNSName predicate :: xs) name = if (domain_predicate' predicate) name then True else check_dns_name xs name
 66 | check_dns_name (x :: xs) name = check_dns_name xs name
 67 | check_dns_name [] _ = False
 68 |
 69 | ||| Check if the certificate has expired
 70 | check_cert_timestamp : HasIO io => Certificate -> io Bool
 71 | check_cert_timestamp cert = (\t => t > cert.valid_not_before && t < cert.valid_not_after) <$> time
 72 |
 73 | ||| Find a certificate with matching common name given an identifier
 74 | find_certificate : Identifier -> List Certificate -> Maybe Certificate
 75 | find_certificate identifier certs = choice $ map (delay . is_certificate identifier) certs
 76 |   where
 77 |     is_certificate : Identifier -> Certificate -> Maybe Certificate
 78 |     is_certificate (Left x)          cert = guard (check_ipv4_address (certificate_subject_names cert) x) $> cert
 79 |     is_certificate (Right (Left x))  cert = guard (check_ipv6_address (certificate_subject_names cert) x) $> cert
 80 |     is_certificate (Right (Right x)) cert = guard (check_dns_name (certificate_subject_names cert) x) $> cert
 81 |
 82 | ||| Convert a string of hostname into an identifier, such as DNSName, IPv4 and IPv6 address
 83 | to_identifier : String -> Identifier
 84 | to_identifier hostname =
 85 |   case parse_ipv4 hostname of
 86 |     Right x => Left x
 87 |     Left _ =>
 88 |       case parse_ipv6 hostname of
 89 |         Right x => Right (Left x)
 90 |         Left _ => Right (Right hostname)
 91 |
 92 | ||| Check if the server's certificate is valid
 93 | check_leaf_certificate : HasIO io => Certificate -> EitherT String io ()
 94 | check_leaf_certificate cert = do
 95 |   True <- check_cert_timestamp cert
 96 |   | False => throwE $ "expired certificate: " <+> show cert
 97 |   let Just key_usage = extract_extension KeyUsage cert
 98 |   | Nothing => throwE $ "certificate does not specify key usage: " <+> show cert
 99 |   let True = key_usage.digital_signature
100 |   | False => throwE $ "certificate key usage does not allow digital signature: " <+> show cert
101 |   pure ()
102 |
103 | ||| Check if the server's certificate's ca and intermediate ca's are valid
104 | ||| depth refers to how deep you are in the certificate chain, needed since
105 | ||| some intermediate ca's specify a constraint on the maximum depth
106 | check_branch_certificate : HasIO io => Nat -> Certificate -> EitherT String io ()
107 | check_branch_certificate depth cert = do
108 |   True <- check_cert_timestamp cert
109 |   | False => throwE $ "expired certificate: " <+> show cert
110 |   let Just key_usage = extract_extension KeyUsage cert
111 |   | Nothing => throwE $ "certificate does not specify key usage: " <+> show cert
112 |   let Just basic_constraint = extract_extension BasicConstraint cert
113 |   | Nothing => throwE $ "certificate does not specify basic constraint: " <+> show cert
114 |   let True = basic_constraint.ca
115 |   | False => throwE $ "certificate is not a CA: " <+> show cert
116 |   let True = basic_constraint.path_len `cmp` depth
117 |   | False => throwE $ "certificate CA depth reached: " <+> show cert
118 |   let True = key_usage.key_cert_sign
119 |   | False => throwE $ "certificate key usage does not allow signing certificates: " <+> show cert
120 |   pure ()
121 |   where
122 |     cmp : Maybe Nat -> Nat -> Bool
123 |     cmp Nothing _ = True
124 |     cmp (Just a) b = b <= a
125 |
126 | ||| Given a certificate and its issuer's certificate, verify if the certificate's signature is correct
127 | verify_certificate_signature : Certificate -> Certificate -> Either String ()
128 | verify_certificate_signature subject issuer = bimap ("error at \{show subject}: " <+>) id $
129 |   verify_signature' subject.sig_parameter issuer.cert_public_key subject.tbs_raw_bytes subject.signature_value
130 |
131 | ||| True if there is intersecting elements in both list
132 | has_intersect : Eq a => List a -> List a -> Bool
133 | has_intersect [] y = False
134 | has_intersect x [] = False
135 | has_intersect (x :: xs) y = if any (x ==) y then True else has_intersect xs y
136 |
137 | ||| Given an Authority Key Identifier extension, verifies if another certificate matches the constraint
138 | ||| This is needed since in the case that a certificate is cross signed by another CA, issuer and subject
139 | ||| distinguished names are not sufficient to find a subject's issuer.
140 | auth_key_id_predicate : ExtAuthorityKeyIdentifier -> (Certificate -> Bool)
141 | auth_key_id_predicate (MkExtAuthorityKeyIdentifier Nothing [] Nothing) = const False
142 | auth_key_id_predicate auth_key_id = go auth_key_id
143 |   where
144 |     def : Maybe Bool -> Bool
145 |     def Nothing = True
146 |     def (Just a) = a
147 |     -- Check if the SHA1 hash of public keys match
148 |     go0 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
149 |     go0 auth_key_id cert = def (map (\i => i == cert.cert_public_key_id) auth_key_id.key_identifier)
150 |     -- Check if the serial number matches
151 |     go1 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
152 |     go1 auth_key_id cert = def (map (\i => i == cert.serial_number) auth_key_id.serial_number)
153 |     -- Check if the subject distinguished names match
154 |     go2 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
155 |     go2 auth_key_id cert =
156 |       case auth_key_id.general_names of
157 |         [] => True
158 |         gn => has_intersect gn $ certificate_subject_names cert
159 |     go : ExtAuthorityKeyIdentifier -> Certificate -> Bool
160 |     go a b = go0 a b && go1 a b && go2 a b
161 |
162 | flatten : Maybe (LazyList a) -> LazyList a
163 | flatten Nothing = []
164 | flatten (Just a) = a
165 |
166 | liftE : Monad m => Either a b -> EitherT a m b
167 | liftE x = MkEitherT $ pure x
168 |
169 | verify_certificate_chain : HasIO io => Nat -> List Certificate -> List Certificate -> Certificate -> EitherT String io ()
170 | verify_certificate_chain depth trusted untrusted current = do
171 |   -- Constructs a lazy list of ca's which have cross signed the current certificate
172 |   -- Won't be used if the certificate has a valid issuer which is in the chain
173 |   let alternate = map (True,) $ flatten $ do
174 |     ext <- extract_extension AuthorityKeyIdentifier current
175 |     let predicate = auth_key_id_predicate ext
176 |     pure $ filter predicate $ Lazy.fromList trusted
177 |
178 |   -- List of certificates which subject name matches the current certificate's issuser name
179 |   let in_chain = filter (\(_,c) => c.subject == current.issuer) (map (False,) untrusted <+> map (True,) trusted)
180 |   let all_candidates = fromList in_chain <+> alternate
181 |
182 |   case all_candidates of
183 |     [] => throwE $ "cannot find issuer for: " <+> show current
184 |     all => Lazy.choice $ map (\(should_trust,next) => go should_trust next current) all
185 |   where
186 |     -- Verify the issuer certificate and the subject's signature
187 |     go : Bool -> Certificate -> Certificate -> EitherT String io ()
188 |     go should_trust next current =
189 |       case should_trust of
190 |         False => do
191 |           check_branch_certificate depth next
192 |           let Right () = verify_certificate_signature current next
193 |           | Left err => throwE $ "certificate failed for subject: " <+> show current <+> ", issuer: " <+> show next <+> ", reason " <+> err
194 |           verify_certificate_chain (S depth) trusted untrusted next
195 |         True => do
196 |           -- replace the self signed certificate with the one in the trusted certificate list
197 |           -- this should works since they are the same
198 |           -- this prevents an attacker modifying the content of the certificate chain, changing the
199 |           -- root ca's certificate with their own, with the same subject name but different public key
200 |           let Just next = find (\c => c.subject == next.subject) trusted
201 |           | Nothing => throwE $ "root certificate not trusted: " <+> show next
202 |           check_branch_certificate depth next
203 |           let Right () = verify_certificate_signature current next
204 |           | Left err => throwE $ "certificate failed for subject: " <+> show current <+> ", issuer: " <+> show next <+> ", reason " <+> err
205 |           pure ()
206 |
207 | ||| Given a list of trusted certificate, hostname of the server, verify the certificate chain
208 | ||| and return a public key to be used to verify TLS handshake
209 | export
210 | certificate_check : List Certificate -> String -> CertificateCheck IO
211 | certificate_check trusted hostname cert = runEitherT $ do
212 |   let certificates = body <$> cert.certificates
213 |   ok <- liftE $ the _ $ traverse parse_certificate certificates
214 |   let identifer = to_identifier hostname
215 |   let Just cert = find_certificate identifer ok
216 |   | Nothing => throwE "cannot find certificate"
217 |   check_leaf_certificate cert
218 |   verify_certificate_chain Z trusted ok cert
219 |   pure cert.cert_public_key
220 |
221 | ||| A CertificateCheck function that always trusts the certificate unless it's malformed
222 | export
223 | certificate_ignore_check : String -> CertificateCheck IO
224 | certificate_ignore_check hostname cert = runEitherT $ do
225 |   let certificates = body <$> cert.certificates
226 |   ok <- liftE $ the _ $ traverse parse_certificate certificates
227 |   let identifer = to_identifier hostname
228 |   let Just cert = find_certificate identifer ok
229 |   | Nothing => throwE "cannot find certificate"
230 |   pure cert.cert_public_key
231 |