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

Award Information
Agency: Department of Homeland Security
Branch: N/A
Contract: 70RSAT18C00000022
Agency Tracking Number: FY18.1-H-SB018.1-008-0005-I
Amount: $149,999.26
Phase: Phase I
Program: SBIR
Solicitation Topic Code: H-SB018.1-008
Solicitation Number: FY18.1
Solicitation Year: 2018
Award Year: 2018
Award Start Date (Proposal Award Date): 2018-05-02
Award End Date (Contract End Date): 2018-11-01
Small Business Information
155 Washington St, Apt 1907, 1907, Jersey City, NJ, 07302-4588
DUNS: 080633032
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Saman Zonouz
 Professor and CEO
 (217) 721-8280
Business Contact
 Saman Zonouz
Title: Founder and CEO
Phone: (217) 721-8280
Research Institution
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).

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government