Module Bap_primus.Std

The Primus Framework

Overview

Primus is a microexecution framework that can be used to implement CPU and full system emulators, symbolic executors, static fuzzers, policy checkers, tracers, quickcheck-like test suites, and other analyses that rely on program evaluation.

The core of Primus is the Primus Machine monad transformer that implements the observable non-deterministic computation. The core functionality is extended by libraries and components. A Primus library doesn't change the behavior of the Primus Machine, but it extends the set of operations available to components and other libraries. The core libraries are:

The behavior of the Primus Machine is defined by the components that comprise that machine. A particular build of the Machine is called a system. A system could be seen as an Primus application and as an application it could be run.

To summarize, components use libraries to implement analysis, that is as a system and could be run to obtain the results of the analysis or to observe its side-effects.

The next few sections will elaborate on certain features of the Primus framework.

Observations

An important part of the Primus Machine computational model is that it is extensible through the user callbacks. The callbacks are inserted at predefined extension points, called observations. Observations are made during a computation, e.g., when an Interperter evaluates a binary operation it posts an observation, that includes the operation operands and the computed value. All parties interested in this observation are invoked and they then can change the state of the machine using other machine operations, post their own observations, and, in general can do anything that the Primus Machine allows, since an observer callback is a Primus Machine computation.

To list all known observations use the bap primus-observations command or use the Primus.Observation.list function.

Non-determinism

Primus implements a non-deterministic computaion model (here non-deterministic is used in a sense of the non-deterministic Turning Machine, when on each step of execution the computation can have more than one outcome). Non-determinism in Primus is implemented by forking the Machine on each non-deterministic computation, so that each machine observes the world deterministically.

Two non-deterministic operations are provided: fork that creates a clone of the current machine and its state but with different identifier and switch that switches between machines.

At any point of time there could be many forks of the machine, but only one will be active. A component that is responsible for selecting a machine fork that is currently active is called scheduler. Since there are few different scheduling strategies avaiable, there are also a few schedulers.

Components and Systems

Components are the main building blocks of the Primus machine. Components subscribe to the observations provided by Primus libraries and other components. The attached callbacks changes the behavior of the Machine thusaffecting its semantics. A particular composition of components is called a system. Therefore a system is a Primus application that could be run. The Primus Framework provides an extenisble repository of Primus systems and components, that could be queried using bap primus-systems and bap primus-components commmands.

A new system could be easily defined in a file with the .asd extension using a simple system definition language (inspired by the Common Lisp ASDF language). When that file is put in the system search directory (or in the current working directory of the process that runs the Primus Framework) it will be added automatically to the systems repository. It is also possible to define and register a system programmatically, using the Primus.System interface.

A new component could be added to the components repository using Primus.Components.register or Primus.Components.register_generic. The main difference between regular components (also called analyses) and generic components is that the latter work with any instantiation of the Primus Monad Transofmer (recall that Primus Machine is not a monad, but a monad transformer, i.e., it is a monad constructor that creates infinitely many Primus Machine monads) and the former works only with the Primus.Analysis monad, which is a concrete instance of the Primus Machine monad parameterized with the Knowledge monad, i.e., Primus.Machine.Make(Knowledge). A regular component is a Primus computation that also has full access to the knowledge base. A generic component is a functor that creates a computation, which can only access Primus Machine operations.

The legacy Primus.Machine.add_component interface is also provided to enable backward compatibility with the old way of defining the Primus machine in which there was only one system, Primus.Machine.Main that was built using the add_component function and the system composition was defined by the command line parameters. This old style is fully supported (but deprecated) and the old main system is available under the bap:legacy-main name.

Running the Machine

To run the specified system, either use Primus.System.run to run it in the Knowledge monad or use Primus.System.Generic.run to run the Machine in the monad some other monad.

It is also possible to create a Primus.Job and enqueue it in the Primus Jobs queue with the Primus.Jobs.enqueue function. This queue could be run either directly with Primus.Jobs.run or using the run plugin.

module Primus : sig ... end

The Primus Framework inteface.