Mutable objects, such as database connections cause overtaint

[JustusAdam]

Mutable objects introduce flows. Which can be unwanted when the mutable object doesn’t actually transport information, or if the information transport is captured in some other way.

Concretely this occurs with the backend object in websubmit. This object represents the database connection. Its semantics are explicitly modeled in the environment model. As a result the backend object may introduce flows that are not actually there.

fn submit(backend: Backend, lecture: u8, apikey: ApiKey, data: Submission) {
    backend.insert(
        "submissions", 
                vec![
                        ("lecture", lecture.into()), 
                        ("user", apikey.id.into()), 
                        ("data", submission)
                ]);

        let presenters = backend.select(
                "SELECT email FROM presenters where lecture = ?", 
                vec![lecture.into()]
        );
        
        email::send(presenters, format!("user {} submitted {}", user.name, submission));
}

This is a much reduced (and with some creative editing) example of what happens in websubmit. The problem that occurs here is that this flow means the send call is blessed, even if we do not teach our model what presenters are. The reason is that both insert and select take an &mut self. As a result insert creates a flow from apikey to backend and select creates a flow from backend to presenters and, due to transitivity, from apikey to presenters. Because apikeyis blessed (it represents the user itself) this means that presenters is blessed. Basically the system now thinks that presenters is the user’s email address.

This is of course mitigated once we do the “all sources” sort of properties, but it will still cause an issue for users, because it will be flagged as a potential source.