ssl: Add property tests framework

3 files changed, 206 insertions, 1 deletions

diff --git a/lib/ssl/test/Makefile b/lib/ssl/test/Makefile
index 9dfb2eba53..d5ba105478 100644
--- a/lib/ssl/test/Makefile
+++ b/lib/ssl/test/Makefile
@@ -61,6 +61,7 @@ MODULES = \
 	ssl_ECC\
 	ssl_upgrade_SUITE\
 	ssl_sni_SUITE \
+	ssl_eqc_SUITE \
 	make_certs\
         x509_test
 
@@ -144,7 +145,7 @@ release_tests_spec: opt
 	$(INSTALL_DATA)  $(ERL_FILES) $(HRL_FILES) $(HRL_FILES_NEEDED_IN_TEST) $(COVER_FILE) "$(RELSYSDIR)"
 	$(INSTALL_DATA) ssl.spec ssl_bench.spec ssl.cover "$(RELSYSDIR)"
 	chmod -R u+w "$(RELSYSDIR)"
-	@tar cf - *_SUITE_data | (cd "$(RELSYSDIR)"; tar xf -)
+	@tar cf - *_SUITE_data property_test | (cd "$(RELSYSDIR)"; tar xf -)
 
 release_docs_spec:
 
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..5303785b17
--- /dev/null
+++ b/lib/ssl/test/property_test/ssl_eqc_handshake.erl
@@ -0,0 +1,146 @@
+%%
+%% %CopyrightBegin%
+%% 
+%% Copyright Ericsson AB 2004-2015. 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("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
+	   ).
+
+tls_version() ->
+    oneof([?'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()
+           %%certificate_verify()
+           %%finished()
+           key_update()
+           %%message_hash()
+          ]);
+tls_msg(Version) ->
+    oneof([#hello_request{},
+           client_hello(Version),
+           %%server_hello(Version)
+           %%certificate(),
+           %%server_key_exchange()
+           %%certificate_request()
+           #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 = ssl_cipher:suites(Version), 
+		  compression_methods = compressions(Version),
+		  random = client_random(Version),
+		  extensions = client_extensions(Version)    
+                 };
+client_hello(Version) ->
+    #client_hello{session_id = session_id(),
+		  client_version = Version,
+		  cipher_suites = ssl_cipher:suites(Version), 
+		  compression_methods = compressions(Version),
+		  random = client_random(Version),
+		  extensions = client_extensions(Version)    
+                 }.
+session_id() ->
+    crypto:strong_rand_bytes(?NUM_OF_SESSION_ID_BYTES).
+ 
+compressions(_) -> 
+    ssl_record:compressions().
+client_random(_) ->
+    crypto:strong_rand_bytes(32).
+       
+client_extensions(_) ->
+    #hello_extensions{}.
+
+key_update() ->
+    #key_update{request_update = request_update()}.
+
+request_update() ->
+     oneof([?UPDATE_NOT_REQUESTED, ?UPDATE_REQUESTED]).
diff --git a/lib/ssl/test/ssl_eqc_SUITE.erl b/lib/ssl/test/ssl_eqc_SUITE.erl
new file mode 100644
index 0000000000..bd36d35c02
--- /dev/null
+++ b/lib/ssl/test/ssl_eqc_SUITE.erl
@@ -0,0 +1,58 @@
+%%
+%% %CopyrightBegin%
+%% 
+%% Copyright Ericsson AB 2015-2015. 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_SUITE).
+
+-compile(export_all).
+%%--------------------------------------------------------------------
+%% Common Test interface functions -----------------------------------
+%%--------------------------------------------------------------------
+
+all() -> 
+    [
+     tls_handshake_encoding
+    ].
+
+%%--------------------------------------------------------------------
+init_per_suite(Config) ->
+    ct_property_test:init_per_suite(Config).
+end_per_suite(Config) ->
+    Config.
+
+init_per_group(_GroupName, Config) ->
+    Config.
+
+end_per_group(_,Config) ->
+    Config.
+
+init_per_testcase(_, Config0) ->
+    Config0.
+
+end_per_testcase(_TestCase, Config) ->
+    Config.
+
+%%--------------------------------------------------------------------
+%% Test Cases --------------------------------------------------------
+%%--------------------------------------------------------------------
+
+tls_handshake_encoding(Config) when is_list(Config) ->
+    %% manual test:  proper:quickcheck(ssl_eqc_handshake:prop_tls_hs_encode_decode()).
+    true =  ct_property_test:quickcheck(ssl_eqc_handshake:prop_tls_hs_encode_decode(),
+                                        Config).