Rubicon

Bounded Checking for Rails Apps


What is Rubicon?

Rubicon is a library for Ruby, Rails, and RSpec that lets you write formal specifications of the behavior of your web apps. In addition to the standard RSpec language, Rubicon gives you the quantifiers of first-order logic, so your specifications cover all possible objects of the given type, and mock objects are no longer needed. The specification below checks that privacy is handled correctly when a Contact is displayed:

describe ContactsController do
  it "should not display other users' private contacts or opportunities" do
    User.forall do |u|
      Contact.forall do |c|
        Opportunity.forall do |o|
          set_current_user(u)
          get :show, :id => c.id

          ((c.access == 'private') &
           (c.user != u)).implies do
            assigns[:contact].should_not == c
          end

          ((o.access == 'private') &
           (o.user != u)).implies do
            assigns[:contact].opportunities should_not
              include o
          end
        end
      end
    end
  end
end

Download

A prototype implementation of Rubicon is available as a Ruby Gem here.

After installing the gem and adding it to your app's Gemfile, you should write the following at the top of your Rails spec file:

require File.expand_path(File.dirname(__FILE__) + '/../spec_helper')
require 'rubicon'

And then run the analysis this way:

bundle exec rspec filename.rb

Tutorial

A tutorial covering the basics of setting up and using Rubicon is available here.