The policies described in this page utilize the ‣ mechanism but the high level concepts are applicable. A migration to the Graph query engine is underway.
In this example the privacy properties are recorded in props.frg, which automatically includes analysis_result.frg. To check the properties, simply run racket props.frg.
https://github.com/JustusAdam/beavered-websubmit
Use the dfpp-experiments branch.
The properties for which checks are currently implemented are:
GDPR-style deletes. There is one controller that deletes every data item the user has provided to the system. This is actually not checked for literally every item, but at least every type that can make its way into the database. (data_is_deleted)
Storing data in the database must be associated to a user. This is necessary for e.g. the deletion to work. (stores_are_safe)
Data is only sent to authorized parties, e.g. the user themselves or users authorized for a particular purpose. (outputs_to_authorized_all and only_send_to_allowed_sources, both check the same but are implemented slightly differently)
This is the most complex property and works as follows: A function which sends data to the outside has one or more arguments annotated as sink and one or more arguments annotated as scopes. sink marks the data which will be sent and scopes the data which describes/determines the recipients.
The property states that if a value marked as sensitive can flow into sink, then each dataflow path that leads into scopes must begin as, or flow through a function call (or arguments) that returns a value or a type labeled with one of a set of authorization markers.
only_send_to_allowed_sources uses the safe_source marker. In the comprehensive version it also uses safe_source_with_bless and bless to ensure all values being added to a vector of recipients are authorizedoutputs_to_authorized_all uses auth_witness, cfg_value and presenter in anticipation that we may later decide to differentiate between them or when they are valid.