The Plume web-application stores various types of user submitted data. There should be a way for the user to delete their personal data if they decide to leave the platform, a mechanism similar as what is stipulated by the GDPR.

However when the developers added the functionality to comment to the application, they forgot to add the appropriate delete functionality to the controller responsible for a user deletion.

https://github.com/Plume-org/Plume/commit/19f18421bcd9cb9d1654de24f9a04747691036b7

impl User {
		#[paralegal::analyze]
		pub fn delete(&self, conn: &mut Connection) -> Result<()> {
				for blog in Blog::find_for_author(self, conn)? {
						blog.delete(conn)?;
				}
				for post_id in post_authors::all_their_posts_ids(self.id, conn)? {
						Post::get(conn, post_id)?.delete(conn)?;
				}
				// This should exist, but doesn't
				// for comment in Comment::list_by_author(conn, self.id)? {
				// 		comment.delete(&conn)?;
				// }
				diesel::delete(self, "user", conn)
		}
}

Paralegal would have prevented this bug. For this we formalize the GDPR-delete policy as follows:

let user_data_types = ctx.marked_type(marker!(user_data));

let found_deleter = ctx
    .controllers()
    .any(|(deleter_id, deleter)| {
        let delete_sinks = ctx
            .marked_sinks(deleter.data_sinks(), marker!(deletes));
        user_data_types.all(|&t| {
            let sources = ctx.srcs_with_type(deleter, t);
            ctx.any_flows_to(*deleter_id, &sources, &delete_sinks)
        })
    });
if !found_deleter {
    ctx.error("Could not find a function deleting all types");
}

Which corresponds to the following plain-English approximation of GDPR’s data deletion requirement:

There must exist at least one (user accessible) controller such that it contains a source for each type of user_data which flows into a sink that deletes the data.

This policy is defined in terms of markers (deletes and user_data), which are added by the developers to the code as shown below:

#[paralegal::marker(deletes)]
use diesel::delete;

#[paralegal::marker(userdata)]
pub struct Post { /* ... */ }
#[paralegal::marker(userdata)]
pub struct Blog { /* ... */ }
#[paralegal::marker(userdata)]
pub struct Comment { /* ... */ }

And when the policy is executed it reports the absence of an appropriate deleter endpoint, and succeeds once the commented-out code is enabled.

$ plume-policy path/to/repo-root
Could not find a function deleting all types
$ plume-policy path/to/repo-root -- --feature enable-delete-comments
Verification successful