Tools Developed at VLab
Modern web applications are frequently built using two software patterns: Model/View/Controller (MVC) and REpresentational State Transfer (REST). This means that the business logic of the application is organized in actions that update the state of the application and can be arbitrarily invoked by the user, and that the business logic is implemented in the model, isolated from the issues such as user navigation and response synthesis. It is paramount to ensure that the model schema and model state updates are correct as these errors may lead to unrecoverable corruption or loss of data. Our tool addresses this problem by extracting an ADS specification from a given Ruby on Rails application, which is an abstraction of both the data model schema and the updates that can be done to the data model state, and verifying it using a first order logic theorem prover. Invariants on the data store can be specified using our own Rails extension.
Most modern web applications are built using development frameworks based on the Model-View-Controller (MVC) pattern. In MVC-based web applications the data model specifies the types of objects used by the application and the relations among them. Since the data model forms the foundation of such applications, its correctness is crucial. We built a tool, iDaVer, that automatically performs data model verification for the MVC framework, Ruby on Rails. iDaVer has two modes of operation. The first is automated verification of user-specified properties. Properties to check about an application's data model are specified using templates. Templates facilitate property specification as well as the ability to seamlessly switch between the verification approaches offered by iDaVer. One approach is bounded verification using the Alloy formal language and a SAT Solver. The other is unbounded verification using the quantified theory of uninterpreted functions and an SMT Solver. The second mode of operation supported by iDaVer is automatic property inference and verification. Three categories of properties are inferred automatically and then verified using unbounded verification. For the properties that fail, repairs are generated that suggested fixes to the data model that establish the inferred properties.
Stranger (STRing AutomatoN GEneratoR) is a string analysis tool for PHP web applications that can be used to detect XSS and SQL vulnerabilities. Stranger uses Pixy as a front end and MONA automata package for automata manipulation. The tool takes a PHP program as input and automatically analyzes it and outputs the possible XSS and SQL injection vulnerabilities in the program. In addition to that, for each input that leads to a vulnerability, it outputs an automaton in a dot format that characterizes all possible string values for this input which may exploit the vulnerability, i.e., it outputs the vulnerability signature.
Singularity is a novel operating system developed by Microsoft Research. In order to improve the dependability of software systems, Singularity operating system uses process isolation. Singularity processes are not allowed to share memory to avoid situations where a buggy process crashes the whole system. Instead, all inter-process communication occurs via message passing over bidirectional conduits, called channels. Singularity processes are required to specify a channel contract that identifies the sequences of messages that can be sent through a given channel. Tune is a tool that analyzes Singularity channel contracts and verifies their properties. Singularity processes can deadlock even when they faithfully implement a channel contract. By analyzing the channel contracts, Tune can prevent such deadlocks and ensure that when processes faithfully implement a channel contract, the properties of the contract are preserved by the implementation.
Action Language is a specification language for reactive software systems that supports both synchronous and asynchronous compositions and hierarchical specifications. Action Language Verifier consists of 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an infinite state model checker which verifies CTL properties of Action Language specifications. Composite Symbolic Library is a symbolic manipulator for automated verification which combines different symbolic representations using an object oriented design. Currently, Composite Symbolic Library supports BDDs for representing boolean logic formulas, and polyhedral and automata representations for linear arithmetic formulas. An extension to Composite Symbolic Library implements shape analysis for checking properties of linked lists.
A tool for analyzing interactions among web services. It consists of: 1) An intermediate representation for web services which supports XML data manipulation; 2) Synchronizability analysis which determines if the asynchronous communication among web services can be synchronized without changing their interaction pattern; 3) Realizability analysis which determines if an interaction pattern can be realized by asynchronously communicating web services; 4) Translators from a subset of BPEL to the WSAT intermediate representation and from the WSAT intermediate representation to Promela, input language of the SPIN model checker.
NetStub is a framework for verification of distributed Java Applications. It is based on a set of stub classes that replace native methods used in network communication and enables verification of distributed Java applications by isolating their behavior from the network. The framework supports two modes of verification: unit verification and integration verification. Integration verification checks multiple interacting distributed application components by running them in a single JVM and simulating the behavior of the network within the same JVM via stub classes. Unit verification targets a single component of a distributed application and requires that the user write an event generator class that utilizes the API exported by the framework.