Skip to content

Latest commit

 

History

History
309 lines (255 loc) · 11.6 KB

USING.md

File metadata and controls

309 lines (255 loc) · 11.6 KB
Raw

FuzzM User's Guide

FuzzM (Fuzzing with Models) is a gray box model-based fuzzing framework that employs Lustre as a modeling and specification language and leverages the JKind model checker as a constraint solver. Fuzzing a target system with FuzzM requires the development of a Lustre model and a relay. The model defines the inputs to the system and specifies behaviors, in the form of properties, that the fuzzer is expected to attack. All of the vectors generated by the framework should satisfy at least one of the specified properties. The relay is responsible for interfacing with the target and for re-formatting FuzzM test vectors so that they can be transmitted to the target. A python relay class that knows how to receive vectors from the fuzzer is provided. Extending this class to interface with a specific target essential in applying this framework.

System Overview

FuzzM is a distributed framework consisting of the following components:

  • The FuzzM Engine
  • An AMQP Server
  • The Relay

The FuzzM engine generates fuzzing test vectors based on a Lustre model and sends them to the AMQP server. The AMQP server enables multiple producer/subscribers to generate or process the fuzzing data. The Relay is responsible for interfacing with the fuzzing target, pulling vectors from the AMQP server, reformatting the vectors, and then passing them on to the target.

The FuzzM Engine

The FuzzM engine is often started and stopped using Docker Compose. Once built, however, it is possible to invoke the fuzzer directly.

java -ea -jar FuzzM/fuzzm/fuzzm/bin/fuzzm.jar -fuzzm [Options] /path/to/file.lus

Or, using a UNIX script:

FuzzM/fuzzm/scripts/fuzzm [Options] /path/to/file.lus

The command line options for fuzzm are listed below:

usage: fuzzm [options] <input>
 -amqp <arg>      URL of AMQP server [null]
 -constraints     Treat Lustre properties as constraints [false]
 -help            print this message
 -no_vectors      Suppress test vector generation (debug) [false]
 -proof           Generate a validating proof script (debug) [false]
 -solutions <arg> Total number of constraint solutions to attempt (-1 = forever) [-1]
 -solver <arg>    Use Only Specified Solver [null]
 -throttle        Throttle vector generation (debug) [false]
 -version         display version information
 -wdir <arg>      Path to temporary working directory [.]

Several options are intended only for debugging purposes and are so indicated. The most commonly used options are:

  • -amqp This option is used to specify the URL of the AMQP server. If this option is not provided the fuzzer will not attempt to send test vectors.

  • -wdir This option is used to specify a location for use as a working directory for the fuzzer. The default is the current working directory.

  • -solver The solver option is used to limit the solver used by FuzzM. This is especially useful if the model contains features supported only by a limited subset of solvers. This option can appear several times on the command line to enable a set of solvers. The default is to use any of the solvers supported by JKind that are currently installed which may include SMTInterpol (default), Z3, CVC4, Yices, Yices2, and MathSAT.

The Model

The Lustre model drives the fuzzing process. Each test vector generated by the fuzzer will consist of an assignment of values to each of the inputs of the model. As a result, the inputs of the Lustre model should correspond in some way with the inputs of the target system. An example Lustre model is provided with the fsm demo here.

There are two inputs to the fsm model, 'length' and 'msg'.

node main(length: byte; msg: fsm_msg) returns ();

The 'msg' input abstracts the actual UDP payload into named fields that are used in constructing the model. Note that the hierarchical names used here also appear as python dictionary keys in the relay code below (ie: 'length' and msg.buff[2]').

type fsm_msg = struct
{
  magic0 : byte;
  magic1 : byte;
  seq    : byte;
  cmd    : byte;
  buff   : byte[16]
};

Assertions are used in the model to establish the types (value bounds) on the inputs.

  --
  -- Value type constraints
  --
  assert(0 <= length     and length     <= 20);
  assert(0 <= msg.magic0 and msg.magic0 < 256);
  assert(0 <= msg.magic1 and msg.magic1 < 256);
  assert(0 <= msg.seq    and msg.seq    < 256);
  assert(0 <= msg.cmd    and msg.cmd    < 16);
  assert(0 <= msg.buff[ 0] and msg.buff[ 0] < 256);

The body of the Lustre model captures the expected behaviors of the target system. Compare the behavior below with the the fsm specification.

  --
  -- State Machine
  --
  next_st = (if (cmd_reset) then 0 else
             if (st0 and st0_ok) then (if (cmd_hello) then 1 else 0) else
             if (st1 and st1_ok) then (if (cmd_data)  then 2 else 1) else
             if (st2 and st2_ok) then (if (cmd_file)  then 3 else 2) else
             if (st3 and st3_ok) then (if (cmd_disco) then 4 else 3) else
             0);

  st = st0() -> (pre next_st);

Finally, properties are used to drive the fuzzer to explore target behaviors. Every test vector generated by the fuzzer will satisfy one of the properties specified in the Lustre file.

  fuzz_st0_ok   = FUZZ(st0_pre_ok and st0_ok);
  fuzz_st0_off0 = FUZZ(st0_pre_ok                                                                        );
  fuzz_st0_off1 = FUZZ(st0_pre_ok and               magic1_ok and seq_ok and st0_cmd_ok and st0_length_ok);
  fuzz_st0_off2 = FUZZ(st0_pre_ok and magic0_ok and               seq_ok and st0_cmd_ok and st0_length_ok);
  fuzz_st0_off3 = FUZZ(st0_pre_ok and magic0_ok and magic1_ok and            st0_cmd_ok and st0_length_ok);
  fuzz_st0_off4 = FUZZ(st0_pre_ok and magic0_ok and magic1_ok and seq_ok and st0_cmd_ok and st0_length_ok);
  fuzz_st0_off5 = FUZZ(st0_pre_ok and magic0_ok and magic1_ok and seq_ok and                st0_length_ok);
  fuzz_st0_off6 = FUZZ(st0_pre_ok and magic0_ok and magic1_ok and seq_ok and st0_cmd_ok                  );

  --%PROPERTY fuzz_st0_ok   ;
  --%PROPERTY fuzz_st0_off0 ;
  --%PROPERTY fuzz_st0_off1 ;
  --%PROPERTY fuzz_st0_off2 ;
  --%PROPERTY fuzz_st0_off3 ;
  --%PROPERTY fuzz_st0_off4 ;
  --%PROPERTY fuzz_st0_off5 ;
  --%PROPERTY fuzz_st0_off6 ;

The AMQP Server

An AMQP server is started along with the FuzzM engine when invoked via Docker Compose.

If running FuzzM manually, an AMQP server will need to be available to the fuzzer. RabbitMQ is an example of an open source AMQP server.

The Relay

The relay will typically extend the python base relay thread class provided with the FuzzM distribution. Several utility relays are provided in the relay base directory and two additional relays are provided in the examples directory, one in each of the fsm and tftp directories. The example below is from the fsm relay.

The fsm relay extends the relay base thread class FuzzMRelayBaseThreadClass. The relay base class implements methods that enable it to synchronize with the fuzzer and start receiving test vectors. Once synchronized, the main job of the user defined relay is to reformat each test vector and send them on to the target. This is accomplished by overriding the processTestVector() method. The fsm implementation below calls the user defined function formatVector() to reformat each FuzzM test vector and then transmits the formatted vector via UDP to the fsm target URL.

from relay_base_class import FuzzMRelayBaseThreadClass

class Relay(FuzzMRelayBaseThreadClass):
    """
    Extend the relay base thread class FuzzMRelayBaseThreadClass.  We
    override the processTestVector() method to perform an appropriate
    action for each new test vector.  In this case we reformat the test
    vector dictionary into a bytearray appropriate for UDP
    transmission to the target.
    """
    def __init__(self, host, target_ip, target_port):
        super(Relay, self).__init__(host)
        self.target_ip = target_ip
        self.target_port = int(target_port)
        self.sock = socket.socket(socket.AF_INET, socket.SOCK_DGRAM)
    
    def processTestVector(self,tv):
        """This method is called on every new test vector"""
        msg = formatVector(tv)
        self.sock.sendto(msg, (self.target_ip, self.target_port))

The user defined 'formatVector()' method from the fsm relay transforms the test vector (presented as a dictionary) into a bytearray suitable for UDP transmission. Note that the dictionary is indexed by strings that reflect the hierarchical names used in the Lustre model shown above. Structures and arrays are flattened into their primitive integer, Boolean (0 or 1), or rational (N/D) components. For reference, compare the code below to the fsm specification of the expected UDP payload.

def formatVector(test_vector):
    """Reformat test vector dictionary into an appropriate target payload"""
    length = int(test_vector['length'])
    if not (0 <= length and length <= 20):
        print("[Relay] Length field out of bounds [0,20] : " + str(length))
        print(test_vector)
        return bytearray(0)
    
    msg = bytearray(length)
    if (0 < length):
        msg[0] = int(test_vector['msg.magic0'])
    if (1 < length):
        msg[1] = int(test_vector['msg.magic1'])
    if (2 < length):
        msg[2] = int(test_vector['msg.seq'])
    if (3 < length):
        msg[3] = int(test_vector['msg.cmd'])
    for index in range(0,length-4):
        name = 'msg.buff[' + str(index) + ']'
        byte = int(test_vector[name])
        msg[4 + index] = byte
    
    return msg

The interface to the relay will vary with each application of FuzzM. Typically, however, the relay will at least need to know the URL of the AMQP server. The fsm relay accepts the URL of the AMQP server and the URL/port of the target. It starts the relay thread and then simply waits for it to end.

def main():
    parser = argparse.ArgumentParser(description="FSM Relay")
    parser.add_argument('-a', '--amqp',
                        required=True,
                        help="The address of the AMQP server")
    parser.add_argument('-t', '--target',
                        required=True,
                        help="The target URL")
    parser.add_argument('-p', '--port',
                        required=True,
                        help="The target port")
    args = parser.parse_args()
    
    ## Initialize the fuzzer relay
    fuzz_relay = Relay(args.fuzz, args.target_ip, args.target_port)
    ## Start the relay
    fuzz_relay.start()
    try:
        fuzz_relay.join()
    except KeyboardInterrupt:
        fuzz_relay.stop()
        fuzz_relay.join()
    return 0

Operation

Docker and Docker Compose are used to simplify the deployment of the FuzzM framework. To run the fsm example, go to the FuzzM/examples/fsm-model directory and type:

docker-compose up

To verify the operation of the fuzzer, connect a web browser to http://<docker host>:15672. If docker is running on your local machine, this would be http://localhost:15672

You will need to log in to the AMQP server as user guest with password guest. After logging in the web page should show activity in the AMQP queues that reflects fuzzing activity, as in the green bar on the graph in the image below.

Server

To terminate the fuzzing session, type:

docker-compose down