Tools Developed at VLab
Stranger: An Automata Based PHP String Analysis Tool
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.
Tune: A Tool for Analyzing Singularity Channel Contracts
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 Verifier and Composite Symbolic Library
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.
Web Service Analysis Tool (WSAT)
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: A Framework for Verification of Distributed Java Applications
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.