Specifying Security Properties of Protocols in the Java Modeling Language: Achieving Code Level Assurance

We present a software tool for translating a protocol specification written in the Proverif cryptographic protocol specification language into Java Modeling Language specification statements that the final Java program is verified against. Compared to existing solutions that generate the completed program from the protocol specification, our tool allows more flexibility in the exact implementation details of the program.

Investigators: Luke Myers, Gary Leavens

Framing for Object-Oriented Programs

Investigate different methodology of specifying frame properties, including the universe type system, dynamic frames, implicit dynamic frames, region logic and separation logic.

Investigators: Yuyan Bao

CheckLT: Taint Checking for Mere Mortals

CheckLT is a program verification tool for Java which can help you use taint tracking to find defects in your software. CheckLT provides an easy to install verification toolset, a simple, non-invasive syntax for annotating programs, and a dynamically configurable security lattice.

Investigators: John L. Singleton

Project Homepage GitHub

Spekl: A Layered System for Specification Authoring, Sharing, and Usage

Specifications, Static checkers, Runtime Assertion Checkers, and SMT-solvers — these tools can be used to make your software better. However, getting them to work together is often difficult and error-prone. Spekl is a platform for streamlining the process of authoring, installing, and using specifications and formal methods tools.

Investigators: John L. Singleton, Gary Leavens

Specification and Verification of Aspect-Oriented Programs

The main focus of my research project is to extend and enhance some modular specification and verification features currently available for implicit invocation systems (like the ones in Ptolemy language) and apply similar features to aspect oriented languages (namely AspectJ).

Investigators: José Sánchez

Information Flow Security for Android Applications

Mobile applications are everywhere. They can record the innermost details of our day-to-day lives. But how can we ensure our mobile applications are safe?

The goal of the Information Flow Security for Android Applications project is answer this question. Our main approach is to develop tools and techniques for specifying and verifying the flow of information for applications running on the Android platform.

Investigators: Gary Leavens, David Naumann, David Cok, John L. Singleton

Project Homepage

Verily: Making Web Applications More Reasonable

The complexity of web application construction is increasing at an astounding rate. The very nature of developing for the web typically requires development across multiple application tiers in a variety of incompatible languages which can result in disjoint code bases. This lack of standardization introduces new challenges in the form of verification.

Verily is a new web framework for Java that supports the development of formally verified web applications. Verily introduces a new development paradigm called Continuously Verified Construction (CVC). Rather than requiring that programs be verified in separate a posteriori analysis, instead Continuously Verified Construction supports construction via a series of Recipes, essentially prescriptions for development which help a developer prove a particular set of properties about an application.

Investigators: John L. Singleton

Project Homepage