And welcome to the user guide for the Paralegal Rust verifier. Below you’ll find the Step-by-Step guide, which is recommended for anyone just starting out with Paralegal. It will guide you through installation steps and develop a first policy with you. Below that we also have a high-level introduction what Paralegal is all about, followed by a more comprehensive reference on the tools, concepts and workflows for using Paralegal.
Please report any issues with the tool or this guide on GitHub https://github.com/brownsys/paralegal/issues.
Paralegal is a static analyzer for Rust code that enforces custom policies on the dependence graph of the program. The central data structure is the Semantic Program Dependence Graph (SPDG). An ordinary PDG (Program Dependence Graph) reflects the data and control flow of a program. The Semantic PDG additionally carries markers that imbue the nodes of the graph with semantic meaning.
Markers are user-defined high-level concepts, such as disclosure, user data or externalization. Developers are responsible for understanding which functions and types embody the concepts described by the markers and attach them accordingly using annotations. They serve a dual purpose: focusing the SPDG extraction and providing a degree of separation between source code and policy.
Policies are user-defined predicates that reason about paths between marked nodes in the SPDG. For instance a policy writer may specify that any node marked input that reaches a node marked store may do so only transitively via a node marked encrypt. In this manner markers abstract away some of the low level detail of the application code and allow the policy writer to reason about the high-level concepts described by the markers instead.
Navigating the Paralegal Repository
Additional Paralegal Build Configuration
Dumping Intermediate Representations
For previously encountered issues that we know workarounds/fixes for: