Retrofitting Security Policy to Late-Stage Software--Taming Giants Through Types and Wimps
Abstract
This proposal describes multiple thrusts of concerted research effort, each aiming to advance our knowledge and ourcapability to re"trofit security andperformance enhancements to existing late-stage software systems.TA1+2: Type-Directed Functionality Removal and" De-bloating Transformations.Our first proposed effort spans Technical Areas 1 and 2. At a high level, we propose to investigate no"vel decompilationand type inference techniques torecover the types of data structures from program binaries. Our key insight is th"at once high-level constructs such astypes and functions of a program binaryhave been successfully inferred, we can design unified" analyses and transformations that are applicable to programsgiven in either source or binary form. We will follow this paradigm to" design a type-directed functionality removal toolfor both source and binaries. In addition, we will also utilize our decompilation" and type inference capability to improvethe performance of legacy binaries through software re-optimization.TA3: Addition of Secu"rity Constructs.Observing our critical need for I/O channel isolation on commodity hardware, we propose to introduce this capabilit""ythrough (i) the implementation of a custom micro-hypervisor, and (ii) the security retrofitting of late-stage I/O software,which" includes vendor drivers that are delivered in either source or binaryform. Our idea is to leverage the proposed program analysis capability in TA 1 and 2 to insert novel inlined referencemonitors (IRMs) designed for I/O accessmediation for the drivers and then" formally verify the security properties of the IRMs with respect to the securitysemantics of our micro-hypervisor. Inaddition, we"" also propose to study the design and implementation of formally-verified cryptographic libraries, with theultimate goal of retrofi""tting them onto legacy systems.TA4: Verification.Finally, we also propose a number of supplementary verification tasks in order to"" gain assurance for the softwareartifacts produced by the tools in TechnicalAreas 1 through 3. In particular, we propose to formal""ly study the soundness and semantic preservation properties ofour program transformations in TA 1 and2, as well as the composition"al security properties of our proposed micro-hypervisor and the accompanying IRMs. Oneof our key insights is that successful verifi"cation often requires multiple iterative refinements, and thus we shoulddesign algorithms that can efficiently reuse relevant parti"al results from previous attempts.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Sep 29, 2017
- Source ID
- N000141712892
Entities
People
- Shan Leung Woo
Organizations
- Massachusetts Institute of Technology
- Office of Naval Research
- United States Navy