About the Project

About the Project

The goal of Annotations for All is to improve software by encouraging developers to contribute software annotations and by enhancing annotation tools.

We recognize that the problem of unsafe/insecure software can’t be solved by just one group of people, so we have created Annotations for All to serve as a useful space for the software development community at large. By tackling the challenge together, we can make a bigger dent in solving this troubling issue.

Specifically, we'd like to focus on widely-used software libraries, since annotating and checking them will have the most widespread benefit.

In addition to aggregating annotation contributions and assessing the current state of annotation practices, we will also sponsor pilot projects and create new tools (and improve existing ones) that help developers write annotations.

To learn more about how you can contribute to Annotations for All, click here.


NSF

About the National Science Foundation:

This work is funded by NSF Grant No. ACI-1314674, titled TTP: Medium: Crowd Sourcing Annotations, issued under the Transition to Practice perspective of the Secure and Trustworthy Cyberspace (SaTC) program solicitation (NSF 12-596). As a Transition to Practice project, our focus is more on moving existing technology into practice than on developing new technology per se.

GrammaTech, Inc. was selected to receive this funding and carry out the project. The Principal Investigator is Dr. David Cok, the Vice President of Technology at GrammaTech. Results of the project will be openly published and any new tools that are developed will be made available under open source licenses.

GrammaTech

About GrammaTech:

GrammaTech’s tools are used by software developers worldwide, spanning a myriad of embedded software industries including avionics, government, medical, military, industrial control, and other applications where reliability and security are paramount.

Originally spun out of Cornell’s computer science labs, GrammaTech is now both a leading research center for software security and a commercial vendor of software-assurance tools and advanced cyber-security solutions. With both static and dynamic analysis tools that analyze source code and binary executables, GrammaTech continues to advance the science of superior software analysis, providing technology for developers to produce safer software.

David Cok

About the PI:

David Cok is an experienced researcher in software analysis, with a particular interest in moving technology into industrial practice. At GrammaTech, he has led numerous research projects in the field of program analysis, for various applications including concolic execution, program metrics, invariant inference, and binary analysis. Prior to GrammaTech, he worked in the Kodak Research Labs on applications of machine learning, automated reasoning, and image processing.

In the Open Source world, he contributes to the Java Modeling Language (JML), to SMTLIB, and to the SMT competitions. In previous work, he converted an early static analysis tool, ESC/Java, into ESC/Java2, bringing it up-to-date with Java and the Java Modeling Language. Dr. Cok is currently working on OpenJML, which will bring the corresponding functional verification capability to current Java.