The SPDG generator paralegal-flow is driven by annotations that govern which function are analyzed and which parts of the source code end up in the extracted mode.
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.
analyze and Targeting#[paralegal::analyze] mainly governs the output.analyze is an annotation for functions and it instructs paralegal-flow to target this function, calculate its dataflow and include it in the system model. If you are missing a certain dataflow in the generated model chances are you forgot an analyze. Also note that Paralegal only ever analyzes a single function at a time even if a callee is also annotated with analyze! We perform no inlining of called functions and no cross-function analysis (yet).
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) { .. }
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();
...
}