Software for which development artifacts are missing is increasingly common and difficult to avoid, including in embedded systems. The lack of development artifacts leaves doubt about whether the software possesses critical security properties and makes enhancement of the software extremely difficult. Embedded systems often have strict resource restrictions/constraints making the application of security enhancements especially difficult. In this paper, we present details of a system that is being developed to provide significant protection against security exploits of embedded systems. The system operates on binary programs. No source code or other development artifacts are required, and the typical size and time constraints of embedded systems are accounted for in the analysis and processing of subject binary programs. Formal verification of security properties is used to eliminate unnecessary security transformations, and transformations are applied by a highly efficient static binary rewriter.