| |||||
SSH Control Flow Properties These benchmark files have been generated by Sagar Chaki. Each of these benchmarks check that a certain sequence of library routine calls can never be executed. There are twenty benchmark files. Sixteen are derived from the OpenSSL server code while the remaining four are from the OpenSSL client code. Names of the server benchmarks begin with "s3_srvr" while those of the client benchmarks begin with "s3_clnt". Each server benchmark checks the impossibility of a certain sequence of library routine calls by the top-level function "ssl3_accept". Essentially a variable called "blastFlag" is used to encode a state machine that executes along with the code and records the sequence of library calls being made. If the offending sequence is detected, the state machine causes the code to jump to a label called "ERROR". BLAST can therefore be used to check for the unreachability of this "ERROR" label. For example the benchmark "s3_srvr.blast.1.c" checks for the absence of the following sequence of library calls: ssl3_get_client_hello -> ssl3_send_server_hello -> ssl3_send_change_cipher_spec -> ssl3_get_finished -> ssl3_send_finished -> ssl3_send_finished In a likewise manner, the client benchmarks check for absence of library call sequences by the top-level routine "ssl3_connect".
Requirements
Instructions |