NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

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.

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)).
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).

PolarSSL Data Structures


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.

The ClientHello Parsing Program



Definition ssl_parse_client_hello : @while.cmd cmd0 bexp := (
  
  
ssl_context *ssl;

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
  (
  
buf = ssl->in_hdr;
  "buf" <-* var_e "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
  )
  (

  
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_") ;

  
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
  )
  (

  
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
  (

  
buf = ssl->in_msg;
  "buf" <-* (var_e "ssl" .-> "in_msg") ;

  
  "_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") ;

  
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
  )
  (

  
ssl->major_ver = SSL_MAJOR_VERSION_3;
  (var_e "ssl" .-> "major_ver") *<- SSL_MAJOR_VERSION_3 ;

  
ssl->minor_ver = (buf5 <= SSL_MINOR_VERSION_2) ? buf5 : SSL_MINOR_VERSION_2;
  "_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 ;

  
ssl->max_major_ver = buf4; ssl->max_minor_ver = buf5;
  var_e "ssl" .-> "max_major_ver" *<- var_e "_buf4_" ;
  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
  )
  (

  
sess_len = buf38;
  "sess_len" <-* add_pe (var_e "buf") (cst32 (Z2s _ 38)) ;

  
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
  )
  (

  
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_") ;

 
ciph_len = ( buf39 + sess_len << 8 ) | ( buf40 + sess_len );
  "_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_")) ;
  (

  
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
  )
  (

  
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
  )
  (

  
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)))
  (

    
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")))
    (

      
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_"))
        (

        
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))
  (

  
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
  )
  (
  
return( POLARSSL_ERR_SSL_NO_CIPHER_CHOSEN );
    "ret" <- POLARSSL_ERR_SSL_NO_CIPHER_CHOSEN ;
    ret
  ))))))))))))))))).

Local Close Scope string_scope.

End PolarSSL.