Abstract
We present Insight, a framework for binary program analysis and two tools provided with it: CFGRecovery and iii.
Insight is intended to be a full environment for analyzing, interacting and verifying executable programs. Insight is able to translate x86, x86-64 and msp430 binary code to our intermediate representation and execute it symbolically in an abstract domain where each variable (register, memory cell) is substituted by a formula representing all its possible values along the current execution path.
CFGRecovery aims at automatically rebuilding the program control flow based only on the executable file. It heavily relies on SMT solvers.
iii provides an interactive and a (Python) programmable interface to a coherent set of features from the Insight framework. It behaves like a debugger except that the execution traces that are examined are symbolic and cover a collection of possible concrete executions at once. For example, iii allows to perform an interactive reconstruction of the CFG.
Chapter PDF
Similar content being viewed by others
References
Balakrishnan, G., Gruian, R., Reps, T., Teitelbaum, T.: CodeSurfer/x86—A platform for analyzing x86 executables. In: Bodik, R. (ed.) CC 2005. LNCS, vol. 3443, pp. 250–254. Springer, Heidelberg (2005)
Balakrishnan, G., Reps, T.: WYSINWYX: What You See Is Not What You eXecute. Journal of ACM Transactions on Programming Languages and Systems (TOPLAS) 32 (2010)
Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: OTAWA: An open toolbox for adaptive WCET analysis. In: Min, S.L., Pettit, R., Puschner, P., Ungerer, T. (eds.) SEUS 2010. LNCS, vol. 6399, pp. 35–46. Springer, Heidelberg (2010)
Bardin, S., Herrmann, P.: OSMOSE: automatic structural testing of executables. Software Testing, Verification and Reliability 21(1), 29–54 (2011)
Bardin, S., Herrmann, P., Leroux, J., Ly, O., Tabary, R., Vincent, A.: The BINCOA framework for binary code analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 165–170. Springer, Heidelberg (2011)
Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: A binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 463–469. Springer, Heidelberg (2011)
Cifuentes, C.: Reverse Compilation Techniques. Ph.D. thesis, Queensland University of Technology, Department of Computer Science (1994)
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)
Franzn, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Proc. of Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 121–128. IEEE (2010)
Kinder, J., Veith, H.: Jakstab: A static analysis platform for binaries. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 423–427. Springer, Heidelberg (2008)
Kinder, J., Zuleger, F., Veith, H.: An abstract interpretation-based framework for control flow reconstruction from binaries. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 214–228. Springer, Heidelberg (2009)
Mycroft, A.: Type-based decompilation (or program reconstruction via type reconstruction). In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 208–223. Springer, Heidelberg (1999)
Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Zhenkai, K.M.G.a.L., James, N., Pongsin, P., Prateek, S.: BitBlaze: A new approach to computer security via binary analysis. In: Proc. of Int. Conf. on Information Systems Security (ICISS). LNCS, pp. 1–25. Springer, Heidelberg (2008)
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288–305. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fleury, E., Ly, O., Point, G., Vincent, A. (2015). Insight: An Open Binary Analysis Framework. In: Baier, C., Tinelli, C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science(), vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-46681-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46680-3
Online ISBN: 978-3-662-46681-0
eBook Packages: Computer ScienceComputer Science (R0)