Skip to content
This repository has been archived by the owner on Nov 9, 2023. It is now read-only.

Latest commit

 

History

History
98 lines (81 loc) · 5.17 KB

README.md

File metadata and controls

98 lines (81 loc) · 5.17 KB
Raw

ProTIP is a tool written in Prolog to evaluate the real connectivity of a PCIe network.

It is described in an article and a talk which can be found here: https://www.sstic.org/2017/presentation/protip/

Archiving

This project is not maintained anymore and has been archived on November 9th, 2023. No further work is expected to happen here.

Prerequisites

To use ProTIP, you need to install Swi-prolog. Not all versions have been tested, but problems have been encountered with versions below 7.

How to use the tool

Edit file input.pl so that it reflects the configuration you want to test. It contains an example configuration ready with hints as how to edit it. (Scrolling through dcg_state.pl can help too to understand the input format).

To get traces possible in your configuration, run swipl the_traces.pl <path_to_output_file>

To get all possible prefixes for unrealized traces, run : swipl enum.pl <path_to_output_file>

Basic architecture

The project architecture is roughly the following :

  • input.pl: inputs of the tool
  • dcg_state.pl: parser of the inputs
  • definitions.pl and abstract_functions.pl: low level predicates and helpers
  • pcie.pl: rules to hop through components
  • traces.pl: search algorithms to enumerate possible traces in the PCIe fabric described. This file contains the "key" predicates queried in the_traces.pl and enum.pl (which are just wrappers). The first one is the_traces(CpltTr,GluedTr), which is statisfied when CpltTr contains the list of complete traces and GluedTr the list of partial traces allowed by the configuration, to which a possible prefix is 'glued'. A trace is complete when it starts with an initial taglist of empty tag lists (i.e. no port is awaiting for completions), it is partial otherwise. We encourage to check out the paper to have details about the trace computations in the tool.
  • display.pl: display functions to gather results and output them in a file.

How to read outputs :

  • In an output file, one can find the list of traces that the tool has found to be possible in the input configuration.

  • All variables starting with _, of the form _G<random_number> or simply _ are automatically generated by the inference mechanisms in Prolog. In future work (very soon !!), we are going to give them names more amenable to human processing... (Same goes for displaying hexadecimal addresses... This is going to be done shortly). The variables with a given name are coherent all along a given trace : everytime you read, _G8 it designates the same variable ranging in the same set of possible values listed just below the trace).

  • The header of the file contains the listing of the elements of configuration analyzed. After that, each trace is an entry of the form :

    Trace : port number accepts reason of acceptation with a classification of the trace sequence of hops forming the trace and constraints : sequence of constaints

where :

  • the port number is the arbitrary physical port number attributed by the tool to the port in the configuration described in input.pl,
  • the trace classification is very rough : if the trace starts with a legitimate packet generation and continues as a series of writes (or a series of read followed by a series of matching completion), the trace is deemed a usual write (or read) trace. Otherwise, it starts with a generate event (typically non-conformant to the specification) and the trace is deemed a WEIRD TRACE TO BE EXAMINED.
    • the sequence of hops is formed as a sequence of hop rule application, so that a trigger event is linked to a result event by application of a rule, which is represented as follows : trigger event -> name of the rule -> resulting event and so on, chaining hops.
    • constraints define the possible finite domains in which the variables can take values for the trace to be possible.

In the article and talk published at SSTIC 2017, there is mention of our work on configuration requests. It is not ready to be pushed yet, but will be promptly.

How to help

We are interested in helping you understand the tool, its inner workings and outputs, and we strongly encourage you to ask for our help. We are also interested in your help in validating the tool outputs. It is difficult to check that everything that should be there is actually listed - we can notice that all that we expect is here, but something that we do not expect might go missing unnoticed. The more we try it out, the better the tool gets. Last but not least, we are interested in comments, feature requests and wish lists of functionalities to help us measure interest in this project and prioritize future work.

Disclaimer :

This tool is intended as an offline audit tool to get an idea about the security of a configuration. Though it is the ultimate ambition of the approach, it has not been tested out thoroughly enough to take absence of dangerous traces as a security guarantee ! However, it is important to us that it is an open source research project, so that we choose to open source it from the beginning, imperfect as it may be.