GrammaTech, Inc. | Date: 2015-07-21
Certain example embodiments described herein relate to techniques for automatically protecting, or hardening, software against exploits of memory-corruption vulnerabilities. The techniques include arranging a plurality of guard regions in the memory in relation to data objects formed by the application program, identifying an access by the application program to a guard region arranged in the memory as a disallowed access, and modifying the execution of the application program in response to the identifying, the modifying being in order to prevent exploitation of the memory and/or to correctly execute the application program.
Agency: Department of Defense | Branch: Navy | Program: STTR | Phase: Phase II | Award Amount: 497.91K | Year: 2015
Software provides critical functionality to the DoD, as well as to the communications, banking, and logistics industries we rely on. Runtime monitoring is now routinely applied to quickly identify and limit attacks. However, monitors have difficulty distinguishing good behavior from bad because intended application behavior varies widely. This proposal describes SMAC (Scenario-based Modeling & Checking), a tool for collecting models of intended behavior that will inform a runtime monitor.SMAC is a suite of tools designed to facilitate creation of models in SMEDL (Scenario-based Meta-Event Description Language). In Phase I, we developed SMEDL as a special-purpose language for capturing high-level security policies (or models of behavior). Phase I also resulted in a design for tools to create, edit and automatically generate SMEDL. SMEDL models can then be used to configure an existing runtime monitor technology. Phase II will implement this design, resulting in a complete framework for supplementing normal application development with fine-grain secure runtime monitoring.
Agency: Department of Defense | Branch: Navy | Program: STTR | Phase: Phase I | Award Amount: 80.00K | Year: 2015
Cyber physical systems are ubiquitous in the modern world; they control transportation, energy, military, medical, and manufacturing infrastructures. Cyber resiliency remains a problem in these systems that rely on both functional and real-time specifications to meet physical, and often safety-critical, goals. We propose a system that integrates existing software strengthening tools (e.g., automated program repair and software hardening) with practical static real-time specification checking to enhance the functional robustness of the target systems while ensuring continued schedulability and real-time specification adherence. The underlying techniques will benefit in a dual fashion: we propose enhancements to the scalability and extensibility of static runtime calculation and consequently will improve upon state-of-the-art software strengthening techniques (in terms of program validation and performance), thus expanding their applicability to operate on the targeted cyber physical systems. The resulting framework will help to guard against both known and unknown vulnerabilities in these critical systems while accounting for schedulability, thus enhancing their cyber resiliency in practice.
Agency: NSF | Branch: Standard Grant | Program: | Phase: Secure &Trustworthy Cyberspace | Award Amount: 978.19K | Year: 2013
Both sound software verification techniques and heuristic software
flaw-finding tools benefit from the presence of software annotations
that describe the behavior of software components. Function summaries
(in the form of logical annotations) allow modular checking of software
and more precise reasoning. However, such annotations are difficult to
write and not commonly produced by software developers, despite their
benefits to static analysis.
The Crowdsourcing Annotations project will address this deficiency by
encouraging software-community-based crowd-sourced generation of
annotations. This effort will be supported by tools that generate, use,
and translate the annotations; the results of annotation efforts will be
shared through openly available repositories. We will also use pilot
projects to demonstrate and encourage the use of annotations and static
analysis. The project will leverage and interact with the Software Assurance Marketplace (SWAMP)
projects collection of static analysis tools and example software. Some
of the technical challenges are developing uniform styles and languages
for annotations, reliably validating crowd-sourced submissions, merging
annotations and the corresponding source code, version control, and
integration with typical software development environments. The social
challenges are also important: designing and implementing a
crowd-sourcing infrastructure in a way that enhances and motivates
community and individual technical and social benefits.
Agency: National Aeronautics and Space Administration | Branch: | Program: SBIR | Phase: Phase II | Award Amount: 750.00K | Year: 2014
Accurate safety analysis of software suffers from a lack of appropriate tools for software developers. Current automated tools require approximate analyses; fully-assured verification with formal methods is expert-intensive. A key to improvement is machine-checkable specifications for software modules. Specifications are also needed to express the intent of software. Further, to scale to wide use, engineers who are not formal methods experts must have usable tools, as automated as possible, integrated into their usual software development environments (IDEs). Our proposal, SPEEDY, is a user experience (UX) design for convenient generation, manipulation, and checking of specifications, directly in a common IDE (Eclipse). The tool's design integrates automated specification suggestion using current tools and published techniques. The tool also enables checking and debugging specifications directly in the IDE, with information presented in the context of the source code. The proposal targets C/C++ programs, particularly for embedded software development. Phase I of SPEEDY assessed current specification languages and prototyped the key UX mechanisms: we are now confident that they can be implemented in the Eclipse IDE. We also integrated several analysis tools, demonstrating that SPEEDY can obtain specification suggestions from external sources. We assessed many specification suggestion algorithms, selecting some to be implemented and evaluated on realistic software in Phase II. Phase I also prototyped the integrating specification checking tools and specification debugging features. We demonstrated SPEEDY on NASA software from the NASA open software site. The Phase II proposal presents a plan for scaling up the successful Phase I prototype in many dimensions: more language features; more sophisticated user guidance in generating and debugging specifications; more specification suggestion algorithms; scaled up to realistic program size.
Agency: Department of Defense | Branch: Defense Advanced Research Projects Agency | Program: SBIR | Phase: Phase II | Award Amount: 1.00M | Year: 2014
Recent studies have shown that embedded systems are extremely vulnerable to security attacks. Some published exploits include remote hijacking of the electronic systems in a modern car and using IP phones and smart televisions to perform covert surveillance of their owners. In this project, we are building a system that removes known vulnerabilities from embedded software and adds protections to prevent exploits of undiscovered vulnerabilities; by integrating with vulnerability detection technology, we will largely automate vulnerability patching, although without formal specifications, some human review will be necessary. Our system uses static rewriting of the software binaries either prior to or after deployment and will integrate with and complement other GrammaTech tools developed under various DoD contracts. The proposed system will operate directly on software binaries, even in the absence of source code or symbol information, applying both to newly developed software and legacy software. The system will be retargetable to different instruction sets to accommodate a variety of embedded systems platforms. To ensure that added protections do not break the functionality of a program, the proposed system will verify that the rewritten program is semantically equivalent to the original program, except for the corrected flaws.
Agency: Department of Defense | Branch: Air Force | Program: SBIR | Phase: Phase I | Award Amount: 150.00K | Year: 2015
ABSTRACT:Trusted platform module(TPM) devices provide the core root of trust for modern computer systems. These devices are used for secure, trusted, and measured boot approaches as well as to secure data for user applications such as Microsoft's Bitlocker technology. However, more and more systems are now virtualized in the cloud. Currently hypervisor technologies either do not provide guests with the needed TPM functionality, or provide a limited and insecure virtual TPM approach. GrammaTech proposes the development of a secured virtual TPM server technology, which can be leveraged by all hypervisor systems to provide guests with virtual TPM instances. The approach will leverage hardware enforced isolation mechanisms and the physical TPM of the system to ensure guests have exclusive access to an assigned virtual TPM. In addition, by creating an interface for QEMU, many common hypervisors will be immediately able to leverage the technology. During this development, GrammaTech will be seeking to combine this technology with both existing hypervisors and GrammaTech's own secure hypervisor technology. Our approach has the advantage of the flexibility to be applied anywhere, while providing a new level of security to the virtual TPM.BENEFIT:GrammaTech will provide a virtual TPM server technology be added to most virtualization systems. The benefits of our approach are adaptability and security. The developed technology will be applied to both existing hypervisor solutions and GrammaTech's secure hypervisor solution to provide additionally security capabilities guests of cloud systems. This will enable new security measures to be taken to protect guest systems including secure boot and measured root of trust for users of cloud technology.
Agency: Department of Defense | Branch: Army | Program: SBIR | Phase: Phase I | Award Amount: 150.00K | Year: 2015
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 bugs 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. GrammaTech proposes the Chase project, 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 can use the results to help prioritize which crashes deserve particular attention.
Agency: Department of Defense | Branch: Air Force | Program: SBIR | Phase: Phase II | Award Amount: 750.00K | Year: 2015
ABSTRACT:The ANTSS project will develop an integrated suite of automated tools that assist the analysis and review of critical software, particularly for independent verification and validation. The tool set combines dynamic test tools (test management, test suite quality measurement, automated test generation) and static program analysis tools (code compliance checking, tools that find program flaws and vulnerabilities, automated code summarization, and automated checking of the consistency of code and requirements). These tools can operate standalone, but ANTSS also integrates them with the SysML modeling layer that underpins requirements management and modeling tools. A centralized location for all requirements, test results, and analysis results enables easy assessment and reporting of the thoroughness of requirements and their validation. The project will use many existing, openly available tools directly, will enhance others, and will incorporate current research in some areas (automated test generation, function summarization, and consistency checking). The ANTSS framework will be implemented as command-line tools and in the Eclipse IDE. The overall goal is to improve the efficiency and accuracy of code understanding and verification by automating processes that are either mundane or require detailed analysis, serving as an assistant to human review and system understanding.BENEFIT:The ANTSS project will improve the efficiency and cost-effectiveness of software verification and validation, both for independent V&V of already built software and during conventional software development projects. The ANTSS tool suite will integrate automated dynamic testing and static program analysis with requirements management and system modeling so that the impact of test and analysis results on requirements and the validity of the overall system will be immediately clear. Furthermore tools that measure test suite quality, check software compliance with programming language style and restrictions, or find program vulnerabilities or potential safety flaws will be integrated with one another. Finally, ANTSS will include state-of-the-art techniques for software summarization, checking consistency of code and formal requirements, and automated test generation. These technologies will assist the human reviewer by providing detailed logical analysis of software in a way that complements human insight and understanding. ANTSS will be commercialized using GrammaTech?s standard product development processes and personnel, as has been done for other successful research transitions in the past. Commercialized tools and features will become part of GrammaTech?s CodeSonar product line and will be marketed to safety- and security-critical software development and review organizations, which overlaps significantly with GrammaTech?s current customer base.
Agency: Department of Defense | Branch: Office of the Secretary of Defense | Program: SBIR | Phase: Phase II | Award Amount: 1.29M | Year: 2014
A modern computer system consists of a complex combination of applications cooperating with the operating system and each other to accomplish a mission. Components of the system are subject to disruption from accidental malfunctions and deliberate attacks