Agency: Department of Defense | Branch: Navy | Program: SBIR | Phase: Phase I | Award Amount: 79.98K | Year: 2015
For many programs, it would be desirable to fail fast in the face of attack in order to preserve confidentiality and integrity. We propose a tool to statically rewrite binaries to increase their fragility, adding this fail-fast property. We will operate on binaries to maximize the number of programs we can protect. Binary rewriting can be applied to any program without cooperation from the compiler, thus supporting programs written in multiple languages or composed from components from different vendors where source may not be available.
Our defenses are designed to protect against information disclosure and control flow hijacking attacks. These defenses will introduce fragility to hinder attacks both before they can inject a malicious payload as well as during active attacks. These defenses turn invalid or undefined behaviors in source programs into fail-stop conditions at run time. Nothing we propose relies on particular software or hardware platform features, and is thus suitable for embedded as well as more traditional server platforms. With prior experience in both binary analysis and verification, Galois is well-positioned to develop high-assurance semantics preserving binary transformations.
Agency: Department of Commerce | Branch: National Institute of Standards and Technology | Program: SBIR | Phase: Phase I | Award Amount: 99.91K | Year: 2015
Galois will build a practical, efficient, modular, deductive code verifier and verification methodology for multithread C11 software. The verifier will take code written to the C11 standard, suitably annotated with function contracts, assertions, program/data invariants, ghost data/code, and any platform-specific assumptions beyond those guaranteed by the standard, and will prove that the code meets its specifications in any suitable concurrent context. The most innovative aspect of the verifier lies in the method for reasoning about C11 weak memory atomics, the most important feature of C11. This approach allows the use of traditional forms of program reasoning using assertions about the global state (e.g. in pre/postconditions, loop and data invariants, etc.). This is done with the help of separation logic, which provides a natural approach to guaranteeing that threads interact with each other in a reasonable way. If our software is going to be used to verify high-assurance programs, the system should be high assurance as well. Therefore, the verifier will be written in the Coq proof assistant language, using the proof assistant to show the correctness of the implementation.
Agency: Department of Defense | Branch: Navy | Program: SBIR | Phase: Phase II | Award Amount: 491.64K | Year: 2013
It is all too common for a project to create software that is hard to maintain, inefficient, bug-ridden, late, and over-budget. Software flaws resulting from this current state of affairs are no longer an inconvenience but are the primary source of software security vulnerabilities. Motivated by a desire to increase our ability to reduce software flaws, we propose a new kind of programmer assistant tool, PICT (Programmer Intent Capture Tool). PICT augments the programmer's toolbox by enabling programmers to describe code properties that can express a wide range of programmer intentions: from low level code assertions to high level design decisions. PICT analyzes and displays these properties continuously during software development. PICT will interactively capture code properties and allow for the managing, analysis, and display of these properties during software development. The tool is designed to provide feedback about global analyses of the program, display feedback continuously, use and work with external code analysis tools, be unobtrusive to the programmer, and distinguish inferred properties from intended properties.
Agency: Department of Defense | Branch: Air Force | Program: SBIR | Phase: Phase I | Award Amount: 149.99K | Year: 2015
ABSTRACT:Computer network defense tools are plagued with an excessive amount of information, frequently in the form of false positives. Rather than attempt to train automated tools to detect attack events more reliably, we propose to build upon existing 'honey-net' technologies to interfere with the reconnaissance phases of an adversary's attack. We will build upon our existing CyberChaff (TM) technology which can host hundreds of virtual 'chaff nodes' on a commodity system. The additions proposed in this SBIR will improve the plausibility of the virtual systems to attackers using passive and active techniques to examine a network.BENEFIT:Virtual honey-nets are a new approach to network security that is beginning to appear in research and prototype phases from assorted sources. Galois is positioned to take advantage of this growth of interest by leveraging our existing CyberChaff (TM) tools. The additional passive and active deceptive techniques proposed here will augment our current licensable technologies to add additional appeal to existing partners and potential clients.
Agency: Department of Defense | Branch: Navy | Program: SBIR | Phase: Phase II | Award Amount: 493.47K | Year: 2014
Modular software development helps enable application developers to quickly write sophisticated applications. However, in most instances only a small fraction of the functionality included in a particular software component is needed. Not only is there a performance cost, but the prevalence of security vulnerabilities suggests that even unused functionality in binaries and shared libraries can be dangerous. We propose to build a new tool, called Reopt, that is capable of optimizing compiled binaries to a particular target platform. As part of this effort, Galois will develop a binary disassembler capable of generating LLVM bytecode from binary machine code. This will allow us to use LLVM-based optimizers to recompile the binary program. In addition, Galois will be working with SRI International as a subcontractor. SRI has developed a prototype tool, Occam, that optimizes binaries through aggressive inlining and partial evaluation. Also as part of this effort, Galois will be working with Zephyr Software on a tool to integrate portions of the original binary with the newly optimized code to create a new optimized binary.
Agency: Department of Homeland Security | Branch: | Program: SBIR | Phase: Phase II | Award Amount: 749.86K | Year: 2014
To meet the critical security needs of the Department of Homeland Security and others, we propose two methods for providing a secure root of trust for mobile devices. One method is designed to integrate as easily into existing systems, while the other requires deeper integration but provides correspondingly stronger security. The keys to our work are practicality and integration: practicality to ensure our system applies to current and near-term mobile devices, and integration to allow for a smooth transition path to mobile device manufacturers. In the proposal we describe not only the technical path to implementation for these two approaches, but also the business, legal, and political steps required to bring root of trust technology to market. Once in place, root of trust technology can be used as a strong basis for implementing other key mobile security solutions, such as secure data at rest, secure data in transit, secure authentication, and mobile device management.
Agency: Department of Defense | Branch: Air Force | Program: SBIR | Phase: Phase II | Award Amount: 993.95K | Year: 2012
Many hardware trojans depend on (a) the ability of an attacker to have an accurate model of the target system and of key software used on that system and (b) identification of one or more deterministic trigger conditions with low observability (i.e., conditions that evade detection by traditional scan- or ATPG-based testing methodologies but that can be exercised on demand via external stimuli). We call this class of trojans deterministic, externally-triggered (DET) trojans. This work introduces a class of software-based general purpose countermeasures to the DET class of trojans. We propose a tool by which the software engineer can transform the source code of system and application software to automatically obfuscate communication channels. The tool takes as input two things: (a) the source code of communicating software components, and (b) a specification of obfuscating transformations on the communications; from these the tool automatically generates the source code transformed with the obfuscations. The resulting system does not adhere to the behavioral model assumed when building the trojan. Thus an adversary's assault is rendered less effective via"attack incompatibility": trigger conditions have been altered such that the malicious behavior cannot be reliably instigated.
Agency: Department of Defense | Branch: Air Force | Program: SBIR | Phase: Phase II | Award Amount: 992.40K | Year: 2013
Unmanned vehicles are becoming an increasingly valuable tool within the Department of Defense, and related technologies are beginning to appear in commercial systems. As their utilization grows, these unmanned systems will become a significant target for cyber attack. Indeed, existing Defense Department unmanned aerial vehicles (UAVs) have already been subjected to attack by various adversaries. One of the primary reasons that our cyber adversaries have had such success is due to the use of deception in their operations. For instance, among APT adversaries, their standard means of gaining an initial foothold is through social engineering: a target is fooled into giving away personal information that the adversary exploits to gain access to a target resource. Deception plays a role in virtually any cyberattack simply for the reason that it works, and the historical evidence bears this out. The very effectiveness of deception suggests that it should be considered as a means to fight back against cyber adversaries. Our response to the challenge of applying deception to the domain of cyberattacks on UAVs is the creation of a platform called ADIDRUS --'Adversarial Dectection, Inference, and Deceptive Response for Unmanned Systems'. ADIDRUS is designed to be a platform-agnostic, software-based solution that incorporates all three of the tactics above into a system that hardens UAVs against attacks through the use of adversarial reasoning models and deceptive tactics turned against the adversary.
Agency: Department of Defense | Branch: Defense Advanced Research Projects Agency | Program: SBIR | Phase: Phase I | Award Amount: 149.56K | Year: 2015
We propose to build a high-level Domain Specific Language (DSL) for graph processing. This DSL, Language For Processing Graphs (LPG), will be embedded in Python and can be compiled to multiple parallel architectures. By using a high-level architecturally-neutral DSL, we gain two things: (1) we can develop programs more quickly, and (2) our programs will not be tied to any specific parallel architecture. When it comes to code generation, the high-level nature of LPG is a two-edged sword: on the one hand, there is a greater semantic gap to bridge; but on the other hand, there will be more possibilities to perform powerful transformations and optimizations. To support better code generation, LPG allows the programmer to add annotations that describe the characteristics of graph data (e.g., sparsity, weight-distribution, problem-size, etc.). Python is already used extensively in the data-analytics community. Embedding LPG in Python means that it is instantly accessible to a large community of users and developers can exploit the extensive Python ecosystem including libraries and tools for plotting and data visualization.
Agency: Department of Defense | Branch: Air Force | Program: STTR | Phase: Phase I | Award Amount: 149.97K | Year: 2015
ABSTRACT: The kinds of capability advancements we anticipate include scalable support for multi-vehicle scenarios with concurrent executions, co-existence of adversarial and cooperative assets, timing and synchronization constraints, heterogeneous sets of specifications (e.g., prioritization over soft vs. hard constraints), and fault-tolerance. The tool development will focus on an open-source software package, which aims (i) to bridge the model-based protocol synthesis artifacts with the low-level implementations and the underlying communication and networking backbone while preserving the correctness guarantees, and (ii) to systematically and manageably interface operators/designers to autonomy protocols through a dedicated domain specific language (DSL). The DSL will provide specification templates, operator tools, and type-checking to detect specification errors before synthesis. We propose to explore techniques to overcome issues in scalability and simplifying specifications. We also propose to develop approaches to assist in certification as well as provide validation that the design and implementation are correct. We will validate our theoretical advances in a real-world testbed, using a small quadcopter unpiloted air system developed by Galois. BENEFIT: We anticipate new approaches to specify and synthesize missions for multi-vehicle scenarios as well as artifacts to ensure the controller implementations are correct. Furthermore, our approach raises the level of abstraction for mission planners. Our proposal will provide the technology to increase the autonomy of multi-vehicle missions as well as the confidence in the missions specified.