 |
||
|
Advanced Search |
||
|
|||||
|
Formal Methods < Verification & Validation < Results Home
|
|
Click here to complete a short survey. The results of this survey will be used to help us improve the research program and this website.
Click here to view research projects that had new research results added in the last 90 days.
|
| A Feasibility Study for Static Analysis of Binary Executables | |
| Point of Contact |
Christoph Michael ccmich@cigital.com |
| Dates | January 2007 - December 2007 |
| Problem | Many critical systems use third-party or legacy software for which source code may not be available. In contrast, many modern static software analysis techniques like model checking are based on software source code. It would be appealing to apply similar techniques to binary executables. We propose to examine the feasibility of performing static software analysis on binary executables. |
| Objective | We propose to examine the feasibility of performing static software analysis on binary executables. During this feasibility study, we will construct a prototype system that can be used to check a specific set of properties in binary code, using dataflow analysis or model checking. Because of Cigital's past experience with software vulnerability scanning, the prototype will focus on security-related software properties. If the feasibility study is successful we will extend our approach to other areas, according to the requirements of NASA. We will also evaluate the success of the prototype. The main evaluation criterion for our prototype will be its ability to accurately detect seeded flaws in large executables, while at the same time avoiding false alarms. This is a standard criterion for success in software vulnerability scanning. In addition, we will evaluate the speed and robustness of the prototype on moderately large executable files. |
| Results |
SAS_07_Exec_Pres_Static_Analysis_Binary_Executables_Michael.ppt SAS_07_TechPres_Static_Anal_Binary_Execs_zip_Michael.zip A Feasibility Study for Static Analysis of Binary Executables Final Report.pdf |
| Keywords | Model checking, static analysis, binary code, third-party software, COTS, legacy code |
| Categories |
Quality Engineering Software Reliability Code Analysis Formal Methods Static Analysis |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |