AMdP

The AMdP project aims to improve the validation and security of medical devices, especially for end-of-life (EoL) devices that the original manufacturer no longer services.  For AMdP, Aarno Labs is maturing technologies that enable high-assurance and low-cost firmware patching of EoL medical devices to fix bugs and vulnerabilities that manufacturers will not address.  Additionally, Aarno Labs continues to develop relational analyses that can provide summary and detailed formal results elucidating the differences between firmware updates, either produced by binary patching or created by the original manufacturer.  

Our recent work, under the DARPA AMP program, has culminated in an advanced binary patching platform, included in CodeHawk, that reduces the complexity and cost of patching vulnerabilities in stripped binaries. By translating binaries into editable formats, our platform empowers typical software engineers, not just specialized reverse engineers, to efficiently address and fix security flaws. This platform reduces errors by using formal validation at every translation step.  Our platform provides assurance artifacts that prove a vulnerability is closed by a patch and that the patch has not altered critical operations.   Our system enables minimal, highly targeted changes that preserve the original binary’s testing and certification.

For example, recently, working with our Prime, STR, we found a serious vulnerability in a popular medical device.  Employing CodeHawk, we were quickly able to produce a statically validated and verified patch without vendor intervention, relying only on modifications to the stripped firmware.  The patch is expressed as changes to our validated C lifting of the firmware binary, and the changes are automatically enacted by our CodeHawk system.  There is no reasoning about the details of the underlying binary.  Furthermore, using our formal analysis, CodeHawk can prove that our patch closes the vulnerability and does not modify any correct (non-exploiting) behaviors.  This is all without relying on testing, which is ad hoc and best effort.  Furthermore, in this case, the original vendor did produce a patch, and we verify that their patch closes the vulnerability, but by employing our relational analysis, we show that their patch introduces new behaviors, features, and a possible vulnerability. 

The platform supports both automated hardening and developer-guided patching.  In our Binary Ninja IDE, developers modify a validated high-level C code lifting of a binary, and our tools makes the associated changes directly on the firmware binary.  Users receive real-time assurance feedback and produce binary patches rapidly without ever thinking about the low-level details of the binary. Our work showcases the potential for secure, cost-effective, and scalable solutions in sectors that require rapid, high-assurance updates to critical embedded systems.