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: 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.
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 nearterm 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: 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 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.