Finding security bugs in web applications using a catalog of access control patterns Near & Jackson, ICSE 2016
If you had a formal specification of the desired security attributes of your web application, and could map that to the source code, you’d be able to verify that it did indeed satisfy the specification. But let’s face it, not many developers of web apps have the time and inclination to go and build a formal spec.. In today’s paper from ICSE 2016 Near and Jackson explore a really interesting compromise. They do all the hard work of building formal models of seven common security patterns, and all the app developer has to do is provide a lightweight mapping from their application code to those patterns. The system has been implemented for Ruby on Rails apps, and while it won’t be able to capture every kind of security bug, it looks like a pretty useful return on investment from the developer’s perspective: of the top 50 most watched Rails apps on GitHub, 30 include some kind of access control; of those 30, eight of the them had security bugs (23 in total) found by the tool (called SPACE – Security PAttern CheckEr), that’s over 25%! One caveat here is that those top 50 apps seem to include a lot of starter projects and samples, and less real-world apps. You can find SPACE at http://www.cs.berkeley.edu/~jnear/space.
From my perspective, there are two interesting angles in this paper. One is simply the security pattern catalog, which though high level is broadly applicable to web apps in general. Then there’s the specific tool chain that automates the process for Rails apps.
A Security Pattern Catalog
Each pattern in our catalog models a common access control use case in web applications. Our catalog is based on the assumption that developers usually intend for a particular pattern to be applied uniformly to all uses of a given resource type – an assumption supported by our experience with real-world applications.
The overall approach is based on whitelisting, so the patterns say what is allowed, and everything else is denied.
- Ownership. This pattern models resources created by a user that ‘belong’ to that user. The owning user can read and write objects they own.
- Public objects are objects that can be read by anyone (e.g. blog posts in a blogging app).
- Authentication models a subset of users that are currently logged in, and provides read access to authenticated objects only for logged in users.
- Explicit permission – this pattern is used to model situations where the application explicitly represents permissions for a resource. Permit relations model giving permission to a user to perform a specific operation on a specific object.
- User profiles. A special case of ownership. Programmers frequently forget checks requiring that the user updating a user profile must be the owner of that profile. Now they won’t.
- Administrators. A special class of users that have full permissions on all objects.
- Explicit Roles. This pattern captures the specification of roles that can be assigned to users, and that allow or deny permission to perform operations.
Checking Rails apps using the catalog
The user needs to help define the mapping between their application resources and the security patterns, which are based on a Role-based access control (RBAC) model under the covers. Resource types themselves, and session management can be inferred automatically.
The map relation can be used to define public and permission objects, but we must define a separate mapping from field names of resources to the corresponding relations they represent in our security patterns.
Consider the MediumClone Rails app (which is a clone of Medium). The populated mapping looks like this, where FieldNames specifies application defined field names and mapfields maps these to pattern roles.:
(The user actually specifies the mapping in Ruby code, see an example in the next section).
SPACE extracts the data exposures from an application using symbolic execution, specializes the constraints on those exposures to the types of role-based access control using the mapping provided by the user, and exports the specialized constraints to an Alloy specification. The, SPACE uses the Alloy Analyzer – an automatic bounded verifier for the Alloy language – to compare the specialized constraints to our pattern catalog (which is also specified in Alloy).
Rather than building a standalone symbolic executor, the authors coerce Ruby’s standard interpreter into performing symbolic execution. This involves defining Ruby classes for symbolic objects and expressions and wiring them in using good old method_missing. SPACE also provides an implementation of the ActiveRecord API that ignores the real database and instead returns symbolic values. Finally, it transparently wraps the Rails rendering API to record the symbolic objects referenced when evaluating view templates.
A MediumClone example
Here’s the code for the user controller taking from the MediumClone app:
Notice that the correct_user filter is not applied to the update operation, so any logged in user can update any other user’s profile (violating pattern 5).
In our experience, this kind of mistake is common: the developer assumes the user will use the interface provided by the site (in this case, the edit page), and will not craft malicious requests to constructed URLs. Developers often fail to consider alternative pats not accessible through the interface, and therefore omit vital security checks.
The User type in the MediumClone app represents the User type in the RBAC pattern catalog. Posts are owned RBAC objects. The mapping the user needs to provide is specified simply as:
[code language=”ruby”]
Space.analyze do
mapping User: RABCUser,
Post: OwnedObject(user: owns)
end
[/code]
SPACE requires the mapping above and MediumClone’s source code – it needs no further input or guidance from the user.
SPACE will find the missing check and produce a counterexample to demonstrate the security vulnerability – see (a) below:
SPACE also finds a second bug whereby the PostController forgets to apply the signed_in_user before filter on the update action. A counterexample is shown in (b) above.