Research in Software Assurance
GrammaTech's research in software assurance is focused on techniques and technologies that enable teams to develop safe, reliable, and secure software applications.
Automated Exploitability Reasoning
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.
The U.S. Army
Analysis Tools for System Surety
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:
- The ability to automatically trace requirements and manage change across the application life-cycle tool chain, including into software coding and formal verification
- An integrated suite of tools supporting program analysis and test management for both C and Fortran
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.
The U.S. Air Force
Calculating and Understanding Resource Bounds to Detect Space/Time Vulnerabilities (STAC)
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.
U.S. Defense Advanced Research Projects Agency (DARPA)
Pliny: An End-to-End Framework for Big Code Analytics (MUSE)
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.
The U.S. Defense Advanced Research Projects Agency (DARPA)
Specification Editing and Discovery Assistant for C/C++ Software Development (SPEEDY)
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:
- Having machine-checkable specifications enables more automation of sound verification and less approximation in heuristic problem detection.
- User interface features and underlying automation will aid all developers in generating, editing, and checking specifications.
- The architecture will apply to both source code analysis alone and also to unified source and machine code verification for embedded systems.
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.
Neptune: A System for Extensible Machine-Code Analysis
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.