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.