Tools Developed at VLab
Profit
Profit is a black-box test profiling tool for networked programs for side-channel vulnerability detection and quantification. It works by sniffing the network traffic produced by test runs of target programs, extracting information out of packet metadata as commonly used features such as packet sizes, timings, flags and finding the side-channel vulnerability by calculating the information leakage using Shannon entropy or using machine learning methods to train a model that can find the secret using the traces.
Automata Based Counter (ABC)
The Automata Based Counter (ABC) is a string and numeric constraint solver and model counter. Given a constraint formula written in the SMT-LIB standard, ABC constructs a multi-track deterministic finite-state automaton (DFA) characterizing the set of solutions which satisfy the given formula. ABC supports both string and numeric constraints and their combinations. The constructed DFA overapproximates the set of solutions for formulas with non-regular string constraints, and can precisely capture the set of solutions to linear integer arithmetic constraints. In addtion, ABC produces symbolic representation of the number of strings and integers within a length bound, k, that satisfy a set of constraints. ABC can also output the number of satisfying solutions given a bound.
PAth Complexity analyzer (PAC)
PAC is a tool for computing path complexity of programs.
SemRep
SemRep is Semantic Differential Repair tool for input validation and sanitization code. The tool analyzes and repairs validation and sanitization functions against each other. The tool does not need any manual specification or intervention. It takes two functions as Dependency Graphs then it looks for differences in validation and sanitization operations for string variables. If a difference is found, the tool suggests a set of three patch functions that can be used to fix the difference. One application for the tool is to fix differences between a sanitizer function on the client-side and the corresponding one on the server. The tool is language agnostic and can be used with Java, PHP or ASP.NET web applications. To achieve this, the tool requires sanitizer functions to be converted into an intermediate dependency graph format.
LibStranger
LibStranger is an Automata-Based Symbolic String Analysis Library. You can use LibStranger to solve string constraints and/or compute pre and post-images of string manipulation operations such as concatenation and replacement. It can handle complex regular-expression based replace operations such as PHP's preg_replace and approximate these operations in the presence of unbounded loops with high precision and smooth performance. In addition, LibStranger provides fast and precise modeling for common string functions such as trim, substring, toUpperCase and toLowerCase and complex sanitization functions such as PHP's addslashes and htmlspecialchars. LibStranger stands for STRing AutomatoN GEneratoR Library.
Abstract Data Store Library (ADSL)
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 Abstract Data Store (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.
iDaVer: an Integrated DAta model VERifier
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: 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.