ADSL - Abstract Data Store Library

ADSL is a gem for formal verification of Ruby on Rails models. Simply include it in your Gemfile, write a few invariants (rules) about ActiveRecord data that you wish to verify (for example, that at any given moment, every Address has a User) and run rake verify!

Besides the verification algorithm, this tool includes a DSL for specifying invariants. The syntax should feel natural to any Rails user. Look at /examples.

This tool is distributed as a Ruby gem and is uploaded to RubyGems.org. It requires Z32 and Spass3 to run. Install it and give it a try!

Installation

This gem is tested on 64 bit Linux. OS-X compatibility not tested, give it a try and tell us if it works! Windows is not supported at this moment.

• Ruby 2.0.0 or later required, along with Rails 3.2. The gem has limited support for 1.9.3 and Rails 4. We suggest using the Ruby Version Manager to manage this installation.
• Download and install Z3 and make sure its executable (z3) on your $PATH
• Download and install Spass and make sure its executable (SPASS) on your $PATH
• Install the ADSL gem by running gem install adsl. If you receive an error while generating documentation for ‘activesupport’ run gem install rdoc adsl instead.

Usage

rake verify <options>

Or, to just observe the extracted model,

rake adsl_translate

The gem also adds an executable adsl that can be used for more fine tuned options. Use adsl --help to look at options.

Development

Source Repository

The ADSL gem is currently hosted at github. The github web page is http://github.com/Bocete/adsl. You can download the source using our public git clone URL:

git://github.com/Bocete/adsl.git

Issues and Bug Reports

Feature requests and bug reports can be made at https://github.com/Bocete/adsl/issues

Publications

• Ivan Bocic and Tevfik Bultan. “Symbolic Model Extraction for Web Application Verification.” ICSE 2017
• Ivan Bocic and Tevfik Bultan. “Finding Access Control Bugs in Web Applications with CanCheck.”. ASE 2016
• Ivan Bocic and Tevfik Bultan. “Efficient Data Model Verification with Many-Sorted Logic”. ASE 2015
• Ivan Bocic and Tevfik Bultan. “Coexecutability for Efficient Verification of Data Model Updates.”. ICSE 2015
• Ivan Bocic and Tevfik Bultan. “Data Model Bugs.”. NFM 2015
• Ivan Bocic and Tevfik Bultan. “Inductive Verification of Data Model Invariants for Web Applications.”. ICSE 2014

License

Rake is available under a Lesser GPL (LGPL) license.

Warranty

This software is provided “as is” and without any express or implied warranties, including, without limitation, the implied warranties of merchantibility and fitness for a particular purpose.