aboutsummaryrefslogtreecommitdiffstats
path: root/lib/ssl/test/property_test/ssl_eqc_handshake.erl
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ssl/test/property_test/ssl_eqc_handshake.erl')
-rw-r--r--lib/ssl/test/property_test/ssl_eqc_handshake.erl534
1 files changed, 534 insertions, 0 deletions
diff --git a/lib/ssl/test/property_test/ssl_eqc_handshake.erl b/lib/ssl/test/property_test/ssl_eqc_handshake.erl
new file mode 100644
index 0000000000..99c6554f15
--- /dev/null
+++ b/lib/ssl/test/property_test/ssl_eqc_handshake.erl
@@ -0,0 +1,534 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2018-2018. All Rights Reserved.
+%%
+%% The contents of this file are subject to the Erlang Public License,
+%% Version 1.1, (the "License"); you may not use this file except in
+%% compliance with the License. You should have received a copy of the
+%% Erlang Public License along with this software. If not, it can be
+%% retrieved online at http://www.erlang.org/.
+%%
+%% Software distributed under the License is distributed on an "AS IS"
+%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
+%% the License for the specific language governing rights and limitations
+%% under the License.
+%%
+%% %CopyrightEnd%
+%%
+%%
+
+-module(ssl_eqc_handshake).
+
+-compile(export_all).
+
+-proptest(eqc).
+-proptest([triq,proper]).
+
+-ifndef(EQC).
+-ifndef(PROPER).
+-ifndef(TRIQ).
+-define(EQC,true).
+-endif.
+-endif.
+-endif.
+
+-ifdef(EQC).
+-include_lib("eqc/include/eqc.hrl").
+-define(MOD_eqc,eqc).
+
+-else.
+-ifdef(PROPER).
+-include_lib("proper/include/proper.hrl").
+-define(MOD_eqc,proper).
+
+-else.
+-ifdef(TRIQ).
+-define(MOD_eqc,triq).
+-include_lib("triq/include/triq.hrl").
+
+-endif.
+-endif.
+-endif.
+
+-include_lib("kernel/include/inet.hrl").
+-include_lib("ssl/src/tls_handshake_1_3.hrl").
+-include_lib("ssl/src/tls_handshake.hrl").
+-include_lib("ssl/src/ssl_handshake.hrl").
+-include_lib("ssl/src/ssl_alert.hrl").
+-include_lib("ssl/src/ssl_internal.hrl").
+
+-define('TLS_v1.3', {3,4}).
+-define('TLS_v1.2', {3,3}).
+-define('TLS_v1.1', {3,2}).
+-define('TLS_v1', {3,1}).
+-define('SSL_v3', {3,0}).
+
+%%--------------------------------------------------------------------
+%% Properties --------------------------------------------------------
+%%--------------------------------------------------------------------
+
+prop_tls_hs_encode_decode() ->
+ ?FORALL({Handshake, TLSVersion}, ?LET(Version, tls_version(), {tls_msg(Version), Version}),
+ try
+ [Type, _Length, Data] = tls_handshake:encode_handshake(Handshake, TLSVersion),
+ case tls_handshake:decode_handshake(TLSVersion, Type, Data) of
+ Handshake ->
+ true;
+ _ ->
+ false
+ end
+ catch
+ throw:#alert{} ->
+ true
+ end
+ ).
+
+%%--------------------------------------------------------------------
+%% Message Generators --------------------------------------------------
+%%--------------------------------------------------------------------
+
+tls_version() ->
+ oneof([?'TLS_v1.3', ?'TLS_v1.2', ?'TLS_v1.1', ?'TLS_v1', ?'SSL_v3']).
+
+tls_msg(?'TLS_v1.3'= Version) ->
+ oneof([client_hello(Version),
+ server_hello(Version),
+ %%new_session_ticket()
+ #end_of_early_data{},
+ encrypted_extensions(),
+ certificate_1_3(),
+ %%certificate_request_1_3,
+ %%certificate_verify()
+ finished(),
+ key_update()
+ ]);
+tls_msg(Version) ->
+ oneof([#hello_request{},
+ client_hello(Version),
+ server_hello(Version),
+ certificate(),
+ %%server_key_exchange()
+ certificate_request(Version),
+ #server_hello_done{},
+ %%certificate_verify()
+ %%client_key_exchange()
+ finished()
+ ]).
+
+client_hello(?'TLS_v1.3' = Version) ->
+ #client_hello{session_id = session_id(),
+ client_version = ?'TLS_v1.2',
+ cipher_suites = cipher_suites(Version),
+ compression_methods = compressions(Version),
+ random = client_random(Version),
+ extensions = client_hello_extensions(Version)
+ };
+client_hello(Version) ->
+ #client_hello{session_id = session_id(),
+ client_version = Version,
+ cipher_suites = cipher_suites(Version),
+ compression_methods = compressions(Version),
+ random = client_random(Version),
+ extensions = client_hello_extensions(Version)
+ }.
+
+server_hello(?'TLS_v1.3' = Version) ->
+ #server_hello{server_version = ?'TLS_v1.2',
+ session_id = session_id(),
+ random = server_random(Version),
+ cipher_suite = cipher_suite(Version),
+ compression_method = compression(Version),
+ extensions = server_hello_extensions(Version)
+ };
+server_hello(Version) ->
+ #server_hello{server_version = Version,
+ session_id = session_id(),
+ random = server_random(Version),
+ cipher_suite = cipher_suite(Version),
+ compression_method = compression(Version),
+ extensions = server_hello_extensions(Version)
+ }.
+
+encrypted_extensions() ->
+ ?LET(Exts, extensions(?'TLS_v1.3'),
+ #encrypted_extensions{extensions = Exts}).
+
+certificate() ->
+ #certificate{
+ asn1_certificates = certificate_chain()
+ }.
+
+certificate_1_3() ->
+ ?LET(Certs, certificate_chain(),
+ #certificate_1_3{
+ certificate_request_context = certificate_request_context(),
+ entries = certificate_entries(Certs, [])
+ }).
+
+key_update() ->
+ #key_update{request_update = request_update()}.
+
+finished() ->
+ ?LET(Size, digest_size(),
+ #finished{verify_data = crypto:strong_rand_bytes(Size)}).
+
+%%--------------------------------------------------------------------
+%% Messge Data Generators -------------------------------------------
+%%--------------------------------------------------------------------
+
+
+cipher_suite(Version) ->
+ oneof(cipher_suites(Version)).
+
+cipher_suites(Version) ->
+ ssl_cipher:suites(Version).
+
+session_id() ->
+ crypto:strong_rand_bytes(?NUM_OF_SESSION_ID_BYTES).
+
+compression(Version) ->
+ oneof(compressions(Version)).
+
+compressions(_) ->
+ ssl_record:compressions().
+
+client_random(_) ->
+ crypto:strong_rand_bytes(32).
+
+server_random(_) ->
+ crypto:strong_rand_bytes(32).
+
+
+client_hello_extensions(?'TLS_v1.3' = Version) ->
+ ?LET({Versions, Ext}, {supported_versions(Version), c_hello_extensions(Version)},
+ maps:merge(Ext, #{client_hello_versions => client_hello_versions(Versions)})
+ );
+client_hello_extensions(?'TLS_v1.2' = Version) ->
+ ?LET({Versions, Exts}, {supported_versions(Version), c_hello_extensions(Version)},
+ maps:merge(Exts, #{client_hello_versions => client_hello_versions(Versions)})
+ );
+client_hello_extensions(Version) ->
+ ?LET(Exts,
+ c_hello_extensions(Version),
+ maps:merge(empty_hello_extensions(Version, client), Exts)).
+
+server_hello_extensions(?'TLS_v1.3' = Version) ->
+ ?LET(Exts,
+ s_hello_extensions(Version),
+ maps:merge(Exts, #{server_hello_selected_version => server_hello_selected_version(Version)}));
+server_hello_extensions(Version) ->
+ ?LET(Exts,
+ s_hello_extensions(Version),
+ Exts).
+
+c_hello_extensions(?'TLS_v1.3'= Version) ->
+ ?LET({KeyShare, PreShare}, {key_share_client_hello(),
+ pre_shared_keyextension()},
+ maps:merge(empty_hello_extensions(Version, client),
+ #{key_share => KeyShare,
+ pre_shared_key => PreShare
+ })
+ );
+c_hello_extensions(Version) ->
+ ?LET(Exts, extensions(Version),
+ maps:merge(empty_hello_extensions(Version, client),
+ Exts)).
+
+s_hello_extensions(?'TLS_v1.3'= Version) ->
+ ?LET({KeyShare, PreShare}, {key_share_server_hello(),
+ pre_shared_keyextension()},
+ maps:merge(empty_hello_extensions(Version, server),
+ #{key_share => KeyShare,
+ pre_shared_key => PreShare
+ })
+ );
+s_hello_extensions(Version) ->
+ ?LET(Exts, extensions(Version),
+ maps:merge(empty_hello_extensions(Version, server),
+ Exts)).
+
+key_share_client_hello() ->
+ oneof([undefined]).
+ %%oneof([#key_share_client_hello{}, undefined]).
+
+key_share_server_hello() ->
+ oneof([undefined]).
+ %%oneof([#key_share_server_hello{}, undefined]).
+
+pre_shared_keyextension() ->
+ oneof([undefined]).
+ %%oneof([#pre_shared_keyextension{},undefined]).
+
+extensions(?'TLS_v1.3') ->
+ ?LET({Ext_1_3, Exts}, {extensions_1_3(), extensions(?'TLS_v1.2')}, maps:merge(Ext_1_3, Exts));
+extensions(?'SSL_v3') ->
+ #{};
+extensions(Version) ->
+ ?LET({SNI, ECPoitF, ECCurves, ALPN, NextP, SRP},
+ {oneof([sni(), undefined]),
+ oneof([ec_poit_formats(), undefined]),
+ oneof([elliptic_curves(Version), undefined]),
+ oneof([alpn(), undefined]),
+ oneof([next_protocol_negotiation(), undefined]),
+ oneof([srp(), undefined])},
+ maps:filter(fun(_, undefined) ->
+ false;
+ (_,_) ->
+ true
+ end,
+ #{sni => SNI,
+ ec_point_formats => ECPoitF,
+ elliptic_curves => ECCurves,
+ alpn => ALPN,
+ next_protocol_negotiation => NextP,
+ srp => SRP})).
+
+extensions_1_3() ->
+ %% ?LET(Entry, key_share_entry(),
+ %% maps:filter(fun(_, undefined) ->
+ %% false;
+ %% (_,_) ->
+ %% true
+ %% end, #{key_share_entry => Entry})).
+ ?LET({HashSign, SigAlgCert}, {oneof([hash_sign_algos(?'TLS_v1.2')]), oneof([signature_scheme_list()])},
+ #{signature_algs => HashSign,
+ signature_algs_cert => SigAlgCert}).
+
+empty_hello_extensions({3, 4}, server) ->
+ #{server_hello_selected_version => undefined,
+ key_share => undefined,
+ pre_shared_key => undefined,
+ sni => undefined
+ };
+empty_hello_extensions({3, 4}, client) ->
+ #{client_hello_versions => undefined,
+ signature_algs => undefined,
+ signature_algs_cert => undefined,
+ sni => undefined,
+ alpn => undefined,
+ key_share => undefined,
+ pre_shared_key => undefined
+ };
+empty_hello_extensions({3, 3}, client) ->
+ Ext = empty_hello_extensions({3,2}, client),
+ Ext#{client_hello_versions => undefined,
+ signature_algs => undefined,
+ signature_algs_cert => undefined};
+empty_hello_extensions(_, client) ->
+ #{renegotiation_info => undefined,
+ alpn => undefined,
+ next_protocol_negotiation => undefined,
+ srp => undefined,
+ ec_point_formats => undefined,
+ elliptic_curves => undefined,
+ sni => undefined};
+empty_hello_extensions(_, server) ->
+ #{renegotiation_info => undefined,
+ alpn => undefined,
+ next_protocol_negotiation => undefined,
+ ec_point_formats => undefined,
+ sni => undefined}.
+
+signature_algs_cert() ->
+ ?LET(Algs, signature_scheme_list(),
+ Algs).
+
+signature_scheme_list() ->
+ ?LET(List, sig_scheme_list(),
+ #signature_scheme_list{signature_scheme_list = List}).
+
+sig_scheme_list() ->
+ oneof([[rsa_pkcs1_sha256],
+ [rsa_pkcs1_sha256, ecdsa_sha1],
+ [rsa_pkcs1_sha256,
+ rsa_pkcs1_sha384,
+ rsa_pkcs1_sha512,
+ ecdsa_secp256r1_sha256,
+ ecdsa_secp384r1_sha384,
+ ecdsa_secp521r1_sha512,
+ rsa_pss_rsae_sha256,
+ rsa_pss_rsae_sha384,
+ rsa_pss_rsae_sha512,
+ rsa_pss_pss_sha256,
+ rsa_pss_pss_sha384,
+ rsa_pss_pss_sha512,
+ rsa_pkcs1_sha1,
+ ecdsa_sha1]
+ ]).
+
+supported_versions(?'TLS_v1.3') ->
+ oneof([[{3,4}],
+ [{3,3},{3,4}],
+ [{3,4},{3,3},{3,2},{3,1},{3,0}]
+ ]);
+supported_versions(_) ->
+ oneof([[{3,3}],
+ [{3,3},{3,2}],
+ [{3,3},{3,2},{3,1},{3,0}]
+ ]).
+
+request_update() ->
+ oneof([?UPDATE_NOT_REQUESTED, ?UPDATE_REQUESTED]).
+
+certificate_chain()->
+ Conf = cert_conf(),
+ ?LET(Chain,
+ choose_certificate_chain(Conf),
+ Chain).
+
+choose_certificate_chain(#{server_config := ServerConf,
+ client_config := ClientConf}) ->
+ oneof([certificate_chain(ServerConf), certificate_chain(ClientConf)]).
+
+certificate_request_context() ->
+ <<>>.
+certificate_entries([], Acc) ->
+ lists:reverse(Acc);
+certificate_entries([Cert | Rest], Acc) ->
+ certificate_entries(Rest, [certificate_entry(Cert) | Acc]).
+
+certificate_entry(Cert) ->
+ #certificate_entry{data = Cert,
+ extensions = certificate_entry_extensions()
+ }.
+certificate_entry_extensions() ->
+ #{}.
+
+certificate_chain(Conf) ->
+ CAs = proplists:get_value(cacerts, Conf),
+ Cert = proplists:get_value(cert, Conf),
+ %% Middle argument are of correct type but will not be used
+ {ok, _, Chain} = ssl_certificate:certificate_chain(Cert, ets:new(foo, []), make_ref(), CAs),
+ Chain.
+
+cert_conf()->
+ Hostname = net_adm:localhost(),
+ {ok, #hostent{h_addr_list = [_IP |_]}} = inet:gethostbyname(net_adm:localhost()),
+ public_key:pkix_test_data(#{server_chain =>
+ #{root => [{key, ssl_test_lib:hardcode_rsa_key(1)}],
+ intermediates => [[{key, ssl_test_lib:hardcode_rsa_key(2)}]],
+ peer => [{extensions, [#'Extension'{extnID =
+ ?'id-ce-subjectAltName',
+ extnValue = [{dNSName, Hostname}],
+ critical = false}]},
+ {key, ssl_test_lib:hardcode_rsa_key(3)}
+ ]},
+ client_chain =>
+ #{root => [{key, ssl_test_lib:hardcode_rsa_key(4)}],
+ intermediates => [[{key, ssl_test_lib:hardcode_rsa_key(5)}]],
+ peer => [{key, ssl_test_lib:hardcode_rsa_key(6)}]}}).
+
+certificate_request(Version) ->
+ #certificate_request{certificate_types = certificate_types(Version),
+ hashsign_algorithms = hashsign_algorithms(Version),
+ certificate_authorities = certificate_authorities()}.
+
+certificate_types(?'TLS_v1.3') ->
+ iolist_to_binary([<<?BYTE(?ECDSA_SIGN)>>, <<?BYTE(?RSA_SIGN)>>]);
+certificate_types(?'TLS_v1.2') ->
+ iolist_to_binary([<<?BYTE(?ECDSA_SIGN)>>, <<?BYTE(?RSA_SIGN)>>, <<?BYTE(?DSS_SIGN)>>]);
+certificate_types(_) ->
+ iolist_to_binary([<<?BYTE(?ECDSA_SIGN)>>, <<?BYTE(?RSA_SIGN)>>, <<?BYTE(?DSS_SIGN)>>]).
+
+hashsign_algorithms({_, N} = Version) when N >= 3 ->
+ #hash_sign_algos{hash_sign_algos = hash_alg_list(Version)};
+hashsign_algorithms(_) ->
+ undefined.
+
+hash_alg_list(Version) ->
+ ?LET(NumOf, choose(0,15),
+ ?LET(List, [hash_alg(Version) || _ <- lists:seq(1,NumOf)],
+ lists:usort(List)
+ )).
+
+hash_alg(Version) ->
+ ?LET(Alg, sign_algorithm(Version),
+ {hash_algorithm(Version, Alg), Alg}
+ ).
+
+hash_algorithm(?'TLS_v1.3', _) ->
+ oneof([sha, sha224, sha256, sha384, sha512]);
+hash_algorithm(?'TLS_v1.2', rsa) ->
+ oneof([sha, sha224, sha256, sha384, sha512]);
+hash_algorithm(_, rsa) ->
+ oneof([md5, sha, sha224, sha256, sha384, sha512]);
+hash_algorithm(_, ecdsa) ->
+ oneof([sha, sha224, sha256, sha384, sha512]);
+hash_algorithm(_, dsa) ->
+ sha.
+
+sign_algorithm(?'TLS_v1.3') ->
+ oneof([rsa, ecdsa]);
+sign_algorithm(_) ->
+ oneof([rsa, dsa, ecdsa]).
+
+certificate_authorities() ->
+ #{server_config := ServerConf} = cert_conf(),
+ Authorities = proplists:get_value(cacerts, ServerConf),
+ Enc = fun(#'OTPCertificate'{tbsCertificate=TBSCert}) ->
+ OTPSubj = TBSCert#'OTPTBSCertificate'.subject,
+ DNEncodedBin = public_key:pkix_encode('Name', OTPSubj, otp),
+ DNEncodedLen = byte_size(DNEncodedBin),
+ <<?UINT16(DNEncodedLen), DNEncodedBin/binary>>
+ end,
+ list_to_binary([Enc(public_key:pkix_decode_cert(DERCert, otp)) || DERCert <- Authorities]).
+
+digest_size()->
+ oneof([160,224,256,384,512]).
+
+key_share_entry() ->
+ undefined.
+ %%#key_share_entry{}.
+
+client_hello_versions(Versions) ->
+ #client_hello_versions{versions = Versions}.
+
+server_hello_selected_version(Version) ->
+ #server_hello_selected_version{selected_version = Version}.
+
+sni() ->
+ #sni{hostname = net_adm:localhost()}.
+
+ec_poit_formats() ->
+ #ec_point_formats{ec_point_format_list = ec_point_format_list()}.
+
+ec_point_format_list() ->
+ [?ECPOINT_UNCOMPRESSED].
+
+elliptic_curves({_, Minor}) ->
+ Curves = tls_v1:ecc_curves(Minor),
+ #elliptic_curves{elliptic_curve_list = Curves}.
+
+hash_sign_algos(Version) ->
+ #hash_sign_algos{hash_sign_algos = hash_alg_list(Version)}.
+
+alpn() ->
+ ?LET(ExtD, alpn_protocols(), #alpn{extension_data = ExtD}).
+
+alpn_protocols() ->
+ oneof([<<"spdy/2">>, <<"spdy/3">>, <<"http/2">>, <<"http/1.0">>, <<"http/1.1">>]).
+
+next_protocol_negotiation() ->
+ %% Predecessor to APLN
+ ?LET(ExtD, alpn_protocols(), #next_protocol_negotiation{extension_data = ExtD}).
+
+srp() ->
+ ?LET(Name, gen_name(), #srp{username = list_to_binary(Name)}).
+
+renegotiation_info() ->
+ #renegotiation_info{renegotiated_connection = 0}.
+
+gen_name() ->
+ ?LET(Size, choose(0,10), gen_string(Size)).
+
+gen_char() ->
+ choose($a,$z).
+
+gen_string(N) ->
+ gen_string(N, []).
+
+gen_string(0, Acc) ->
+ Acc;
+gen_string(N, Acc) ->
+ ?LET(Char, gen_char(), gen_string(N-1, [Char | Acc])).