SBIR-STTR Award

An existing binary static analyzer will be enhanced to provide both exploit protections and anti-memory-tampering defenses via static rewriting rules. A binary static analyzer will accept the original binary and the rewriting rules and produce a new, protected binary. Formal theorem-proving methods will be used to verify that the security instrumentation does not alter correct execution of the program when not under attack.

Keywords:
Computer Security, Program Binaries, Static Analysis, Binary Rewriting, Embedded Systems.

An existing binary static analyzer will be enhanced to protect embedded systems binaries by rewriting the binaries with security instrumentation to enforce four separate defenses against various exploit classes. Formal analysis methods will be used to prove correctness of the security instrumentation, as well as to prove which functions in the binary require protections and which functions are safe from each exploit class.