Affix: Binary Model Generation for Static Analysis
Static analysis and dynamic analysis are the yin and yang of program analysis. Static analysis has the benefit that it can reason about many, or all, runs of a program at once. However, to do that it must abstract aspects of the programs semantics. For large or complicated programs, the resulting imprecision can lead to an intolerable number of false-positive alarms. Dynamic analysis reasons about particular program executions precisely, using a (perhaps automatically generated) test suite. Doing so avoids false positives, but at the cost of false negatives (missed bugs), especially if the test suite is insufficiently diverse.
The complementary nature of these two techniques raises the question of how they can be best combined. In this experience report, we will talk about one promising approach: (1) use dynamic analysis on binary code, such as proprietary libraries, to infer behavioral models; and (2) use static analysis on source code, using the models to reason about interactions between source and binary code.
We have been experimenting with statically analyzing interesting programs using the Infer analysis tool [1], distributed by Facebook. We looked at how we might statically analyze binary components (e.g., non-standard libraries) of such programs by lifting them into SIL, the intermediate representa tion used by Infer. However, it turns out that opensource tools for binary code lifting and/or analysis— including BAP [2], McSema [3], angr [4], and others— do little or no abstraction recovery: local and global variables, function parameters, etc. are not present, and instead the code still resembles the original assembly. Past work on abstraction recovery [5] is partially effective in the best case, but far less so when obfuscations and/or optimizations are used to produce the binary.
Therefore we have begun to use dynamic analysis to produce Infer-compatible behavioral models for binary components. Since we know from the original source program what the API is for the missing binary, we can connect the observed behavior to the
API in order to construct a model based on tests. This permits treating the binary as a black, or gray, box. Executed tests can be over the entire, original program (of which the binary is a component), or over the binary directly, through a harness (which could be constructed semi-automatically). We are focusing on models that can assist reasoning about taint-based security properties, using binary-level dynamic taint tracking as a basis (several good frameworks are available). We are exploring the use of fuzz testing and symbolic execution as a basis of test generation.
Our talk will describe our overall experience using dynamic/static analysis over mixed source/binary programs, and the pitfalls and successes we have achieved. This is joint work with Ian Sweet, Anwar Mamat, and Bee Lavendar, also at Creative Computation, Inc.
References:
[1] C. Calcagno and D. Distefano, “Infer: An automatic program verifier for memory safety of c programs,” in NASA Formal Methods (M. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi, eds.), (Berlin, Heidelberg), pp. 459–465, Springer Berlin Heidelberg, 2011.
[2] D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, “Bap: A binary analysis platform,” in Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, (Berlin, Heidelberg), pp. 463–469, Springer-Verlag, 2011.
[3] T. of Bits, “Mcsema.” https://github.com/ trailofbits/mcsema, 2018
[4] Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Kruegel, and G. Vigna, “SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis,” in IEEE Symposium on Security and Privacy, 2016.
[5] K. Anand, M. Smithson, K. Elwazeer, A. Kotha, J. Gruen, N. Giles, and R. Barua, “A compiler-level intermediate representation based binary analysis and rewriting system,” in Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys ’13, (New York, NY, USA), pp. 295–308, ACM, 2013.
Michael W. Hicks is a Professor in the Computer Science department and the CTO of Correct Computation, Inc. He recently completed a three-year term as Chair of ACM SIGPLAN, the Special Interest Group in Programming Languages, and was the first Director of the University of Maryland's Cybersecurity Center (MC2). His research focuses on using programming languages and analyses to improve the security, reliability, and availability of software. He has explored the design of new programming languages and analysis tools for helping programmers find bugs and software vulnerabilities, and explored technologies to shorten patch application times by allowing software upgrades without downtime. Recently he has been looking at synergies between cryptography and programming languages, as well techniques involving random testing and probabilistic reasoning. He also led the development of a new security-oriented programming contest, "build-it, break-it, fix-it," which has been offered to the public and to students of his Coursera class on Software Security. He blogs at http://www.pl-enthusiast.net/.