Automated Code Repair to Ensure Memory Safety-2018-07-16 Meeting
Carnegie Mellon University Software Engineering Institute Pittsburgh United States
Pagination or Media Count:
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 executableslibraries 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.
- Computer Programming and Software