Software Assurance

GrammaTech, along with teammates Fraunhofer USA and Secure Decisions, propose to develop and implement a repeatable methodology for testing, evaluating, and modernizing existing open-source static-analysis tools. The selected tools, targeting multiple programming languages, will be greatly improved by this effort and the updated tools will be open-sourced. It is our position that commercial participation is critical for long-term adoption and viability of open-source static-analysis tools.

Our overall STAMPOut framework will prioritize tests, evaluation effort, and tool improvements based on the needs of the targeted languages, application domains, and strengths of the tools in question. We will improve static-analysis tools across multiple important languages, including static and dynamic languages.

Sponsored by:

Department of Homeland Security (DHS)

Fuzzing techniques will often produce a large enough number of crashing inputs for the program under test that it is important to prioritize them in terms of impact. One natural axis of a bug's impact is whether it can be used in a security exploit. Determining whether a crash is exploitable, however, is a complex and multi-layered problem. Within this project, GrammaTech is developing Chase, a tool suite for automatically triaging crashes reported in a program depending on the degree to which a crash appears indicative of an exploitable security vulnerability. In the long term, Chase will combine information about the crash itself, analyses to determine what data values are particularly important, computations of how much influence the attacker has over those important values (i.e., channel capacity), fault localization techniques, static analysis for "proving" unexploitability, taint analysis, automatic exploit generation, and domain-specific knowledge about exploitability. Chase will analyze a stripped binary in the context of a particular crashing input, compute or record the above information, and produce an estimate of the likelihood that the bug is exploitable. Users of Chase will be able to use the results to help prioritize which crashes deserve particular attention.

These tools will be able to be used standalone, but many of the tools and techniques will be useful for ranking warnings from static analysis tools such as GrammaTech's CodeSonar. CodeSonar is a leading commercial tools for finding program vulnerabilities and will be an intended transition target for this technology. In addition to this specific application, we will be advancing technology for symbolic execution, fault localization, and other analyses, which will benefit other projects and application areas as well.

Sponsored by:

The U.S. Army

This project will improve both requirements management and program analysis tools for critical software development and V & V. First, building from existing products and technology, GrammaTech will construct an integrated tool suite of program analysis and test management tools: checking compliance against software coding standards, checking for safety and security programming flaws, verifying software against formally expressed requirements, managing automated test execution and generation, and measuring test coverage. Tools that exist for C programs will be enhanced, adapted, and integrated, as needed, for the critical-software domain. Corresponding tools for Fortran programs generally do not exist and will be designed and prototyped to provide analogous functionality. Second, the requirements tracking and change management tool chain will be enhanced with automated consistency and change checking, based on a SysML infrastructure. In particular, we will connect formal verification tools, which are currently not integrated into requirements management processes, to other requirements management tools. The result will be an integrated tool suite that provides better requirements and test management and contains improved tools for C and Fortran program analysis, enabling engineers to be more efficient and more accurate in creating and certifying critical software.

The project will generate these new capabilities, as assistants to human creativity and insight in producing critical software systems:

We will be able to integrate the technology resulting from this project into CodeSonar, our current program-analysis product line, and make it available to existing and new customers developing embedded software systems.

Sponsored by:

The U.S. Air Force

The STAC program seeks to enable analysts with the ability to identify two important classes of vulnerabilities that are based on an application's usage of space and time. GrammaTech is building technology to automatically detect these vulnerabilities.

The first type, Algorithmic Complexity Vulnerabilities, allow an attacker to create inputs that can cause excessive resource consumption, frequently used to mount Denial-of-Service (DoS) attacks that disrupt a software application's responsiveness. The second type, Side-Channel Leaks, allow an attacker to infer confidential information by observing an application's usage of time and space.

GrammaTech's technology will detect these classes of vulnerabilities in Java bytecode, without requiring access to program source code. GrammaTech will also collaborate with researchers at Yale University, who will contribute recent breakthroughs in amortized resource-bound analysis, as well as researchers at the University of Wisconsin-Madison, who will contribute seminal work in shape analysis, enabling the combined technology to capture the dependence of resource use on linked data structures.

Sponsored by:

U.S. Defense Advanced Research Projects Agency (DARPA)

Mining and Understanding Software Enclaves (MUSE) is an initiative that seeks to gather hundreds of billions of lines of publicly available open-source computer code to mine in an effort to create a searchable database of properties, behaviors, and vulnerabilities. PLINY is a joint effort among GrammaTech, Rice University, the University of Texas-Austin, and the University of Wisconsin-Madison.

GrammaTech’s role in the PLINY project focuses on analyzing code to extract program elements that represent computational paradigms, as well as identifying syntactic and semantic features that characterize the program elements. Accurate identification and characterization of program elements is essential to enabling organization and search of PLINY’s code database. GrammaTech’s CodeSonar static analysis tool will be at the center of the effort to generate features. CodeSonar provides extraordinary scalability, an ability to analyze diverse code samples, and an analysis engine with proven capabilities for discovering subtle program properties. For more information about the PLINY project, visit DARPA’s MUSE page.

Sponsored by:

The U.S. Defense Advanced Research Projects Agency (DARPA)

GrammaTech is developing a specification editing and discovery tool (SPEEDY) for C/C++. The tool will assist software developers with modular formal verification tasks by providing active user interface guidance in writing and editing software specifications, integrated into a common, open IDE (Eclipse). Built on an architecture that will unify source and machine code verification, the tool will provide automated suggestions of specifications for given contexts. It will be packaged as a plug-in to Eclipse's C/C++ development environment.

This innovation is significant for the following reasons:

The resulting tool will facilitate the use of formal methods by all software developers, improving efficiency and accuracy. The resulting specifications will also serve as machine-readable documentation of the software, simplifying and accelerating the task of independent V&V.

Sponsored by:

NASA

The VET (Vetting Commodity IT Software and Firmware) program seeks to help U.S. government agencies address the threat of malicious code and hidden “backdoor” access in commodity IT devices. Mobile phones, network routers, computer workstations, and other networked devices can be secretly modified to function in unintended ways or spy on users. To address this danger, GrammaTech will be developing a tool that tackles this supply-chain risk-management issue for software and firmware.

GrammaTech’s tool will automatically discover malicious functionality in these devices. The technology will take in two inputs: software in binary form and a list of properties to check in the software, in order to ensure a secure system. It will then run a series of sound analyses of the binary code to check all of the required properties, and produce a set of reports of potential property violations, or prove that all of the properties hold.

The deep technical challenges inherent in the VET project require solutions that must surpass present state-of-the-art machine-code analysis technologies. For instance, current static analyses are either scalable but heuristic (unsound), or sound but unscalable to the program sizes needed for VET. To achieve the project goals, GrammaTech will be developing sound, yet scalable binary-analysis techniques. Additionally, analyses are often tied to specific properties to be checked and developed only for a specific instruction set. GrammaTech’s technology will be able to check broad collections of properties and it will be readily retargetable to new instruction sets.

Sponsored by:

The U.S. Defense Advanced Research Projects Agency (DARPA)