Automated Code Repair to Ensure Memory Safety-2018-07-16 Meeting

Abstract

Goals and strategy. Goal: Repair code (both C source code and x86 binary) to enable a proof of memory safety. This entails formal reasoning in regards to: 1. The repaired program is memory-safe. 2. The repaired program is equivalent (modulo undefined behavior) to the original program. Strategy: 1. Translate original source code to a simple intermediate representation (IR), annotating the IR with tags that record how to convert it back to original code.2. Disassemble binary executables/libraries (using Pharos) to the same IR.3. Repair the IR (whole-program analysis, operating on output files from steps 1 and 2 above). 4. Convert repaired IR back to the original code as closely as possible.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 16, 2018
Accession Number
AD1083751

Entities

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Computer Programming
  • Computer Programs
  • Department Of Defense
  • Engineering
  • Governments
  • Guarantees
  • Instructions
  • Materials
  • Prototypes
  • Reasoning
  • Semantics
  • Side Effects
  • Software Development
  • Universities

Fields of Study

  • Engineering

Readers

  • Computer Programming and Software Development.
  • Database Systems and Applications
  • Facility/Structural Engineering.