A policy in Paralegal is anchored by markers, a collection of semantically meaningful categories. For example user_data or sensitive. Policies mention

The annotations are available from the paralegal library. Linking to the library is described in Project Setup and Example.

The marker-based annotation API revolves around attaching uninterpreted names (markers) to functions and types to give them meaning for the policy. Unlike other verifiers the interactions between those labeled entities should be figured out by the SDPG extractor with no additional help from the developer. As a result we require very few annotations and the tool does not interpret the names of the markers at all, though it uses the presence and absence of markers to optimize the SPDG extraction. The user is free to assign any meaning for the marker through their policy.

Marking

Markers are a mechanism that separates the concern of a policy from the low level details of the source code. Policies reason about high level concepts like user_data or disclosure, detached from which parts of the source code actually embody those concepts. Developers associate functions and types with a concept by applying marker annotations. Policies can then enforce certain flows for these functions and types by reasoning about their markers.

#[paralegal_flow::marker(marker_name)] is the most common annotation. It attaches a user defined, uninterpreted marker, in this case marker_name, to the annotated entity. This can be used for instance to annotate a type as containing sensitive data.

#[paralegal_flow::marker(sensitive)]
struct User {}

Markers can also be placed on functions:

#[paralegal_flow::marker(leaking, arguments = [1])]
fn send(recipients: &[String], content: &str) { .. }

arguments = [1,3] is a refined form of the marker annotation for functions. The label in this case is assigned to the arguments of this function at the call site. Arguments are referenced with 0 based indices.

Marking arguments instead of whole functions increases precision, for instance we can now distinguish between the part of the email being sent to the outside and the recipients it’s being sent to. This enables our policy to specify for instance that specifically the recipients must be authorized.

return is a refinement similar to arguments but in this case it attaches the marker to the value returned from the function.

Annotations can combine multiple refinements and each function or entity can have multiple annotations attached to it. This allows different markers to be, for instance, attached to different (or the same) argument.

#[paralegal_flow::marker(receiving, arguments = [0], return)]
#[paralegal_flow::marker(leaking, arguments = [1])]
fn send(recipients: &[String], content: &str) { .. }

Application of Markers on Types

Paralegal records types for controller inputs and return values in its output artifact, but only if those types are marked. Consider this example

#[paralegal_flow::marker(sensitive)]
struct User {}

fn get_user() -> User { ... }

#[paralegal_flow::analyze]
fn my_controller(user: User) {
	
	let another_user = get_user();

  ...
}

The User type is recorded as the type of argument 0 of the controller (e.g. the user) argument and as the type of the return value of get_user, e.g. the another_user variable.

The same also applies if the marked type is only a part of the overall type, though in this case the type emitted in the artifact is not the entire type, but the marked portion.