Principled Security Analysis of the Firmware Binaries via Guaranteed Formal Verification and Scalable Dynamic Monitoring

Consequently, to protect the mobile/IoT platforms against complex security attacks, there is a need for effective analysis of mobile/IoT firmware. Such a solution is currently missing in the market. In this DHS SBIR effort, we will develop BINSEC, a mobile/IoT firmware binary security analysis framework. To ensure acceptable scalability, usability, and universality across different firmware binary formats, BINSEC will use a combination of advanced binary reverse engineering, malware analysis, programming languages techniques, formal methods, and dynamic vulnerability assessment algorithms to generate accurate and human-perceivable reports in a timely manner.The anticipated ultimate outcome of our project will be an IoT firmware binary security analysis framework (BINSEC) that has the following features: i) universal: unlike the existing limited technologies, BINSEC will support a variety of common and widely-used IoT device ISAs, and binary formats through its code lifting procedures and use of common intermediate representation; ii) scalable: BINSEC will provide security analysis results in a timely manner for complex firmware binaries through its optimizations and use of parallel processing; iii) usable: BINSEC's human perceivable reports and interface will make it easy-to-use by security analysts without deep binary analysis knowledge requirements; iv) efficient: BINSEC will be leverage static and dynamic techniques to ensure the performance of its analysis across various firmware versions of the same device as well as the accuracy of its binary vulnerability assessment results; v) holistic: BINSEC will corroborate its firmware analysis results with network traces (e.g., invocation of the malicious code identified in the firmware).