<aside> 💡 If you encounter any issues with this setup please open an issue in GitHub with the documentation label.

</aside>

This is an opinionated “probably what you want” guide for getting started with Paralegal. It will take you through

• Installing the Paralegal library and rustc plugin.
• Show you how to set up your project for verification with Paralegal.
• Explore an example policy to teach you the concepts you need to know for reading, understanding and writing Paralegal policies.

This guide explains the basics in so far as they are necessary for the example policy. For advanced use cases and comprehensive documentation see: Documentation by Topic. Each section in this guide also links to further reading in the detailed documentation.

Installation

Prerequisites: Paralegal requires that you have installed rustup and that the directory in which cargo installs binaries is on your PATH.

Start by cloning the https://github.com/brownsys/dfpp repository.

git clone <https://github.com/brownsys/paralegal>

Change into the cloned directory and install the cargo and rustc plugins

cd paralegal
cargo install --locked --path crates/paralegal-flow

This will make the cargo paralegal-flow command available which is responsible for extracting dependence graphs (SPDGs) from the code you want to analyze.

The repository also contains the library crates crates/paralegal-spdg which defines the Rust types describing the dependence graphs and crates/paralegal-policy a framework for writing policies in.

Project Setup and Example

The repository provides an example project guide/file-db-example with all the setup required for both the crate-under-analysis as well as the policy. file-db-example represents a part of an application that stores user data (images and text documents). For simplicity this application stores those objects simply as files on disk. Images in img, documents in doc. The code in main.rs models the deletion logic of the application which is tasked with deleting all objects related to a user. In the next section we’ll formalize this deletion policy and check it with Paralegal.

The codebase under analysis should link against the paralegal library. This library provides the macros necessary for Markers and Annotations. The example on the left is from the Cargo.toml of file-db-example, in other projects you should adjust the path according to your installation location of paralegal.

// Cargo.toml
[dependencies]
paralegal = { path = "../../crates/paralegal" }

You may also want to add the files on the right to your .gitignore.

flow-graph.json
analysis_result.frg
analysis_result.info.json