1180747 - Confine and document security-sensitive bits of code in TC

Status: RESOLVED FIXED

(Taskcluster :: General, defect)

Description

[Dustin J. Mitchell [:dustin] (he/him)]

TC has a strong security model, but its implementation is spread thinly across the codebase: creation of credentials, user authentication for temp credentials, interpretation of credentials on API calls, and verification of scopes at various points in the execution of a task (or a worker or a service or whatever).

This makes it difficult to understand or reason about security questions: to prove a security assertion, I need to know and trust a half-dozen codebases.

I'd like to see:

 1. A list of code that handles authentication, credentials, scopes, secrets, etc.

 2. A reasonably formal description of the invariants each bit of code maintains ("The scopes listed in the created task are satisfied by the scopes associated with the credentials used to authenticate the API request")

It might be easiest to auto-generate this from the code, so the invariants and the code can live together, but still be discoverable in one place.

Comment 1

[Armen [:armenzg]]

This is great to see! +2^10

Comment 2

[Dustin J. Mitchell [:dustin] (he/him)]

I made the list (it's in my notebook, and is probably already out of date, or will be soon, so I won't transcribe it).

Things are a little more centralized than I had feared: for the most part, taskcluster-base handles the scope checking, and other code either sets `scopes` in an API declaration, creates temporary credentials using authorizedScopes to limit access (even for use internally), or calls scopeMatch.

The API declarations are already easily machine-parsed (they're in the API definition).  scopeMatch is easy to grep for.  The tricky bits in terms of any kind of automated code interpretation are the permanent and temporary credentials used within each service, and linking all of these together.

I'm not yet convinced that it's impossible to extract a complete set of logical propositions from the code, and feed those into a simple theorem-prover, against which we could make negative assertions.  I need to play around with it by hand for a bit to see if that's a fruitful course.  It's quite likely the answer is "no" but it will be fun :)

For the record, I'm not proposing to prove the code itself is correct -- I expect this will take propositions from specially-formatted comments in many cases.  It will be up to the programmers to ensure the nearby code does not falsify the propositions.

Comment 3

[Dustin J. Mitchell [:dustin] (he/him)]

I played around with the idea of using a declarative programming language like Prolog to represent the deductive rules underlying the scope system.  It turns out that, at least with regular old Prolog, these are fairly difficult to describe, and it's difficult to come up with useful queries that are not trivially true.  Furthermore, in most cases we would want to write negative queries (X can *not* cause Y to occur), when really all a declarative language can deliver is "given the available information, it cannot be shown that X can cause Y to occur".  Which isn't very strong.

So, a fun stroll down memory lane, but I think I've taken this as far as I can.