<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.
• Setting up your project for verification with Paralegal.
• Teaching you the concepts you need to know for reading, understanding and writing Paralegal policies, with a running example policy.

This guide explains the basics insofar 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

Compatibility: Paralegal has been tested on Linux (Ubuntu), MacOS and WSL. It should also work on Windows though.

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

The easiest way to install paralegal is by using the install script that automatically pulls the latest release

curl -fsSL <https://raw.githubusercontent.com/brownsys/paralegal/main/install.sh> | sh

On supported platforms (Linux x86_64, Linux aarch64 and MacOS aarch64) this downloads a precompiled binary (fast install). On unsupported platforms it will download the source files and install from sources (slow install). The script also supports options to force one or the other.

Verify the binaries are available on the PATH by running the following command

cargo paralegal-flow --help

Which should output something like

Usage: cargo-paralegal-flow [OPTIONS] [-- <CARGO_ARGS>...]

Options:
      --result-path <RESULT_PATH>  Where to write the resulting GraphLocation (default flow-graph.o)
      --strict                     Emit errors instead of warnings for potential soundness risks
      --target <TARGET>            Run paralegal only on this crate
      -h, --help                   Print help

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 is from the Cargo.toml of file-db-example, which uses a path dependency because it lives inside the paralegal repo. In your own project, depend on it via git instead, e.g. paralegal = { git = "<https://github.com/brownsys/paralegal>" } (optionally pinned with rev or tag).

# Cargo.toml (inside the paralegal repo)
[dependencies]
paralegal = { path = "../../crates/paralegal" }