NOTE: The examples in this directory were provided as benchmarks
by Sagar Chaki and the CMU MAGIC team.
We thank them for their support.

---


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

Have fun!

-- Team MAGIC

