Library POLAR_parse_client_hello
Require Import ssreflect ssrbool eqtype.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Require Import POLAR_library_functions.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Module PolarSSL.
Include POLAR_library_functions.PolarSSL.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Require Import POLAR_library_functions.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Module PolarSSL.
Include POLAR_library_functions.PolarSSL.
NB: it has been tested by retrofitting the generated code to PolarSSL
that the interpretation of return as skip is ok
Definition return_ (e : exp) : @while.cmd cmd0 bexp := skip.
Definition ret := skip.
Require Import rfc5246.
Import RFC5246.
Definition POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO := cst32 (Z2s _ (-38912)).
Definition POLARSSL_ERR_SSL_NO_CIPHER_CHOSEN := cst32 (Z2s _ (-16384)).
Definition ret := skip.
Require Import rfc5246.
Import RFC5246.
Definition POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO := cst32 (Z2s _ (-38912)).
Definition POLARSSL_ERR_SSL_NO_CIPHER_CHOSEN := cst32 (Z2s _ (-16384)).
from inlude/polarssl/ssl.h
Definition SSL_MAJOR_VERSION_3 := cst8 (Z2s _ 3). Definition SSL_MSG_HANDSHAKE := cst8 (Z2s _ 22). Definition SSL_HS_CLIENT_HELLO := cst8 (Z2s _ 1). Definition SSL_MINOR_VERSION_2 := cst8 (Z2s _ 2).
struct _ssl_session {
int cipher; /*!< chosen cipher */
int length; /*!< session id length */
unsigned char id[32]; /*!< session identifier */
// ...
};
typedef struct _ssl_session ssl_session;
Definition ssl_sess := (
("cipher", btyp sint32) ::
("length", btyp sint32) ::
("id", ptyp (btyp uchar)) :: nil)%string.
Definition ssl_session := styp (mkStag "ssl_session") ssl_sess.
Lemma wf_ssl_session : wft ssl_session.
struct _ssl_context {
/*
* Miscellaneous
*/
int state; /*!< SSL handshake: current state */
int major_ver; /*!< equal to SSL_MAJOR_VERSION_3 */
int minor_ver; /*!< either 0 (SSL3) or 1 (TLS1.0) */
int max_major_ver; /*!< max. major version from client */
int max_minor_ver; /*!< max. minor version from client */
/*
* Callbacks (RNG, debug, I/O)
*/
// int ( *f_recv)(void *, unsigned char *, int);
// void *p_recv; /*!< context for reading operations */
/*
* Session layer
*/
ssl_session *session; /*!< current session data */
/*
* Record layer (incoming data)
*/
unsigned char *in_hdr; /*!< 5-byte record header (in_ctr+8) */
unsigned char *in_msg; /*!< the message contents (in_hdr+5) */
int in_left; /*!< amount of data read so far */
/*
* Crypto layer
*/
int *ciphers; /*!< allowed ciphersuites */
unsigned char randbytes[64]; /*!< random bytes */
// ...
}
typedef _ssl_context ssl_context;
Definition ssl_ctxt := (
("state", btyp sint32) ::
("major_ver", btyp sint32) ::
("minor_ver", btyp sint32) ::
("max_major_ver", btyp sint32) ::
("max_minor_ver", btyp sint32) ::
("session", ptyp ssl_session) ::
("in_hdr", ptyp (btyp uchar)) ::
("in_msg", ptyp (btyp uchar)) ::
("in_left", btyp sint32) ::
("ciphers", ptyp (btyp sint32)) ::
("randbytes", ptyp (btyp uchar)) :: nil)%string.
Definition ssl_context := styp (mkStag "ssl_context") ssl_ctxt.
Lemma wf_ssl_context : wft ssl_context.
Local Open Scope string_scope.
ssl_context *ssl;
int ret, i, j, n; int sess_len; unsigned char *buf, *p;
int ret, i, j, n; int sess_len; unsigned char *buf, *p;
if( ( ret = ssl_fetch_input( ssl, 5 ) ) != 0 ) { return( ret ); }
ssl_fetch_input "ret" "ssl" (cst32 (Z2s _ 5)) ;
while.ifte (exp2bexp (var_e "ret" \!=e cst32_0))
ret
(
while.ifte (exp2bexp (var_e "ret" \!=e cst32_0))
ret
(
buf = ssl->in_hdr;
if( ( buf0 & 0x80 ) != 0 ) { ... } { ... }
"_buf0_" <-* var_e "buf" ;
while.ifte (exp2bexp ((var_e "_buf0_" \&e cst8 (Z2s 8 (-128))) \!=e cst8 (Z2s 8 0)))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
if( buf0 != SSL_MSG_HANDSHAKE || buf1 != SSL_MAJOR_VERSION_3 )
{ return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
while.ifte (exp2bexp (var_e "_buf0_" \!=e SSL_MSG_HANDSHAKE))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf1_" <-* add_pe (var_e "buf") cst32_1 ;
while.ifte (exp2bexp (var_e "_buf1_" \!=e SSL_MAJOR_VERSION_3))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf1_" <-* add_pe (var_e "buf") cst32_1 ;
while.ifte (exp2bexp (var_e "_buf1_" \!=e SSL_MAJOR_VERSION_3))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
n = ( buf3 << 8 ) | buf4;
"_buf3_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 3)) ;
"_buf4_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 4)) ;
"n" <- ((c2i) (var_e "_buf3_") \<<e cst32 (Z2s _ 8)) \|e (c2i) (var_e "_buf4_") ;
"_buf4_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 4)) ;
"n" <- ((c2i) (var_e "_buf3_") \<<e cst32 (Z2s _ 8)) \|e (c2i) (var_e "_buf4_") ;
if( n < 45 || n > 512 ) { return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
while.ifte (exp2bexp (var_e "n" \<e cst32 (Z2s _ 45)))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
while.ifte (exp2bexp (var_e "n" \>e cst32 (Z2s _ 512)))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
while.ifte (exp2bexp (var_e "n" \>e cst32 (Z2s _ 512)))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
if( ( ret = ssl_fetch_input( ssl, 5 + n ) ) != 0 ) { return( ret ); }
ssl_fetch_input "ret" "ssl" (cst32 (Z2s _ 5) \+e var_e "n") ;
while.ifte (exp2bexp (var_e "ret" \!=e cst32_0))
ret
(
while.ifte (exp2bexp (var_e "ret" \!=e cst32_0))
ret
(
buf = ssl->in_msg;
"buf" <-* (var_e "ssl" .-> "in_msg") ;
"_n0_" <-* (var_e "ssl" .-> "in_left");
"n" <- var_e "_n0_" \-e cst32 (Z2s _ 5) ;
"_n0_" <-* (var_e "ssl" .-> "in_left");
"n" <- var_e "_n0_" \-e cst32 (Z2s _ 5) ;
md5_update( &ssl->fin_md5 , buf, n );
sha1_update( &ssl->fin_sha1, buf, n );
md5_update (var_e "ssl" .-> "fin_md5") (var_e "buf") (var_e "n") ;
sha1_update (var_e "ssl" .-> "fin_sha1") (var_e "buf") (var_e "n") ;
sha1_update (var_e "ssl" .-> "fin_sha1") (var_e "buf") (var_e "n") ;
if( buf0 != SSL_HS_CLIENT_HELLO || buf4 != SSL_MAJOR_VERSION_3 )
{ return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
"_buf0_" <-* var_e "buf" ;
while.ifte (exp2bexp (var_e "_buf0_" \!=e SSL_HS_CLIENT_HELLO))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf4_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 4));
while.ifte (exp2bexp (var_e "_buf4_" \!=e SSL_MAJOR_VERSION_3))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
while.ifte (exp2bexp (var_e "_buf0_" \!=e SSL_HS_CLIENT_HELLO))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf4_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 4));
while.ifte (exp2bexp (var_e "_buf4_" \!=e SSL_MAJOR_VERSION_3))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
ssl->major_ver = SSL_MAJOR_VERSION_3;
"_buf5_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 5)) ;
(var_e "ssl" .-> "minor_ver") *<- ifte_e (bop_ne le_e (var_e "_buf5_") SSL_MINOR_VERSION_2) (var_e "_buf5_") SSL_MINOR_VERSION_2 ;
(var_e "ssl" .-> "minor_ver") *<- ifte_e (bop_ne le_e (var_e "_buf5_") SSL_MINOR_VERSION_2) (var_e "_buf5_") SSL_MINOR_VERSION_2 ;
var_e "ssl" .-> "max_major_ver" *<- var_e "_buf4_" ;
var_e "ssl" .-> "max_minor_ver" *<- var_e "_buf5_" ;
var_e "ssl" .-> "max_minor_ver" *<- var_e "_buf5_" ;
memcpy( ssl->randbytes, buf + 6, 32 );
memcpy "_it_" (var_e "ssl" .-> "randbytes") (add_pe (var_e "buf") (cst32 (Z2s _ 6))) (cst32 (Z2s _ 32)) ;
if( buf1 != 0 || n != 4 + ( ( buf2 << 8 ) | buf3 ) )
{ return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
"_buf1_" <-* add_pe (var_e "buf") cst32_1 ;
while.ifte (exp2bexp ((var_e "_buf1_") \!=e (cst8 (Z2s 8 0))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf2_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 2)) ;
"_buf3_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 3)) ;
while.ifte (exp2bexp (var_e "n" \!=e (cst32 (Z2s _ 4) \+e ((( (c2i) (var_e "_buf2_") \<<e cst32 (Z2s _ 8)) \|e (c2i) (var_e "_buf3_"))))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
while.ifte (exp2bexp ((var_e "_buf1_") \!=e (cst8 (Z2s 8 0))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
"_buf2_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 2)) ;
"_buf3_" <-* add_pe (var_e "buf") (cst32 (Z2s _ 3)) ;
while.ifte (exp2bexp (var_e "n" \!=e (cst32 (Z2s _ 4) \+e ((( (c2i) (var_e "_buf2_") \<<e cst32 (Z2s _ 8)) \|e (c2i) (var_e "_buf3_"))))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
sess_len = buf38;
if( sess_len < 0 || sess_len > 32 )
{ return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
while.ifte (exp2bexp ((var_e "sess_len" \<e cst32_0) \||e (var_e "sess_len" \>e cst32 (Z2s _ 32))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
ssl->session->length = sess_len;
memset( ssl->session->id, 0, sizeof( ssl->session->id ) ); // sizeof(ssl->session->id) == sizeof(typeof(unsigned char* ))
memcpy( ssl->session->id, buf + 39 , ssl->session->length );
"_ssl_session_0_" <-* (var_e "ssl" .-> "session");
(var_e "_ssl_session_0_" .-> "length") *<- var_e "sess_len";
memset "_it_" (var_e "_ssl_session_0_" .-> "id") cst32_0 (cst32 (Z2s _ 32)) ;
"_ssl_session_0_length_" <-* (var_e "_ssl_session_0_" .-> "length") ;
memcpy "_it_" (var_e "_ssl_session_0_" .-> "id") (add_pe (var_e "buf") (cst32 (Z2s _ 39))) (var_e "_ssl_session_0_length_") ;
"_buf39_plus_sess_len_" <-* var_e "buf" \+e (cst32 (Z2s _ 39) \+e var_e "sess_len") ;
"_buf40_plus_sess_len_" <-* var_e "buf" \+e (cst32 (Z2s _ 40) \+e var_e "sess_len") ;
"ciph_len" <- ((c2i) (var_e "_buf39_plus_sess_len_") \<<e cst32 (Z2s _ 8)) \|e ((c2i) (var_e "_buf40_plus_sess_len_")) ;
(
"_buf40_plus_sess_len_" <-* var_e "buf" \+e (cst32 (Z2s _ 40) \+e var_e "sess_len") ;
"ciph_len" <- ((c2i) (var_e "_buf39_plus_sess_len_") \<<e cst32 (Z2s _ 8)) \|e ((c2i) (var_e "_buf40_plus_sess_len_")) ;
(
if( ciph_len < 2 || ciph_len > 256 || ( ciph_len mod 2 ) != 0 ) { return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
while.ifte (exp2bexp (((var_e "ciph_len" \<e cst32 (Z2s _ 2)) \||e (var_e "ciph_len" \>e cst32 (Z2s _ 256))) \||e ((bopk_ne mod2n_e (var_e "ciph_len") 1) \!=e cst32_0)))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
comp_len = buf41 + sess_len + ciph_len;
"comp_len" <-* add_pe (var_e "buf") ((cst32 (Z2s _ 41) \+e var_e "sess_len") \+e var_e "ciph_len") ;
if( comp_len < 1 || comp_len > 16 )
{ return( POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ); }
while.ifte (exp2bexp ((var_e "comp_len" \<e cst32_1) \||e (var_e "comp_len" \>e cst32 (Z2s _ 16))))
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
(
"ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO ;
ret
)
(
for( i = 0; ssl->ciphersi != 0; i++ ) { ... }
"_goto_have_cipher_" <- cst32_0;
"i" <- cst32_0 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* (var_e "_ssl_ciphers_" \+e var_e "i") ;
while.while (exp2bexp ((var_e "_goto_have_cipher_" \=e cst32_0) \&&e (var_e "_ssl_ciphers_i_" \!=e cst32_0)))
(
"i" <- cst32_0 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* (var_e "_ssl_ciphers_" \+e var_e "i") ;
while.while (exp2bexp ((var_e "_goto_have_cipher_" \=e cst32_0) \&&e (var_e "_ssl_ciphers_i_" \!=e cst32_0)))
(
for( j = 0, p = buf + 41 + sess_len; j < ciph_len; j += 2, p += 2 ) { ... }
"j" <- cst32_0 ;
"p" <- ((var_e "buf" \+e cst32 (Z2s _ 41)) \+e var_e "sess_len") ;
while.while (exp2bexp ((var_e "_goto_have_cipher_" \=e cst32_0) \&&e (var_e "j" \<e var_e "ciph_len")))
(
"p" <- ((var_e "buf" \+e cst32 (Z2s _ 41)) \+e var_e "sess_len") ;
while.while (exp2bexp ((var_e "_goto_have_cipher_" \=e cst32_0) \&&e (var_e "j" \<e var_e "ciph_len")))
(
if( p0 == 0 && p1 == ssl->ciphersi ) ...
"_p0_" <-* var_e "p";
while.ifte (exp2bexp ((var_e "_p0_") \=e cst32_0))
(
"_p1_" <-* add_pe (var_e "p") cst32_1 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* add_pe (var_e "_ssl_ciphers_") (var_e "i") ;
while.ifte (exp2bexp (var_e "_p1_" \=e var_e "_ssl_ciphers_i_"))
(
while.ifte (exp2bexp ((var_e "_p0_") \=e cst32_0))
(
"_p1_" <-* add_pe (var_e "p") cst32_1 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* add_pe (var_e "_ssl_ciphers_") (var_e "i") ;
while.ifte (exp2bexp (var_e "_p1_" \=e var_e "_ssl_ciphers_i_"))
(
goto have_cipher;
"_goto_have_cipher_" <- cst32_1
)
(
"j" <- var_e "j" \+e cst32 (Z2s _ 2) ;
"p" <- var_e "p" \+e cst32 (Z2s _ 2)
)
)
(
"j" <- var_e "j" \+e cst32 (Z2s _ 2) ;
"p" <- var_e "p" \+e cst32 (Z2s _ 2)
)
) ;
"i" <- var_e "i" \+e cst32_1 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* add_pe (var_e "_ssl_ciphers_") (var_e "i")
) ;
while.ifte (exp2bexp (var_e "_goto_have_cipher_" \!=e cst32_0))
(
)
(
"j" <- var_e "j" \+e cst32 (Z2s _ 2) ;
"p" <- var_e "p" \+e cst32 (Z2s _ 2)
)
)
(
"j" <- var_e "j" \+e cst32 (Z2s _ 2) ;
"p" <- var_e "p" \+e cst32 (Z2s _ 2)
)
) ;
"i" <- var_e "i" \+e cst32_1 ;
"_ssl_ciphers_" <-* (var_e "ssl" .-> "ciphers") ;
"_ssl_ciphers_i_" <-* add_pe (var_e "_ssl_ciphers_") (var_e "i")
) ;
while.ifte (exp2bexp (var_e "_goto_have_cipher_" \!=e cst32_0))
(
ssl->session->cipher = ssl->ciphersi;
ssl->in_left = 0;
ssl->state++;
return( 0 );
(var_e "_ssl_session_0_" .-> "cipher") *<- var_e "_ssl_ciphers_i_" ;
(var_e "ssl" .-> "in_left") *<- cst32_0 ;
"_ssl_state_" <-* var_e "ssl" .-> "state" ;
(var_e "ssl" .-> "state") *<- var_e "_ssl_state_" \+e cst32_1 ;
"ret" <- cst32_0 ;
ret
)
(
(var_e "ssl" .-> "in_left") *<- cst32_0 ;
"_ssl_state_" <-* var_e "ssl" .-> "state" ;
(var_e "ssl" .-> "state") *<- var_e "_ssl_state_" \+e cst32_1 ;
"ret" <- cst32_0 ;
ret
)
(
return( POLARSSL_ERR_SSL_NO_CIPHER_CHOSEN );