Abstract
In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
An example of a very recent bug found in GCC: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=80180.
- 2.
The ARM and BIL transition systems are deterministic and live, thus the transition relations are total functions. For this reason we omit quantifiers over the states on the right hand side of transitions, since they always exist and are unique.
References
Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 209–224. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87873-5_18
Balliu, M., Dam, M., Guanciale, R.: Automating information flow analysis of low level code. In: SIGSAC Conference on Computer and Communications Security, pp. 1080–1091. ACM (2014)
Beringer, L., Petcher, A., Katherine, Q.Y., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: USENIX Security Symposium, pp. 207–221 (2015)
Bletsch, T., Jiang, X., Freeh, V.W., Liang, Z.: Jump-oriented programming: a new class of code-reuse attack. In: Symposium on Information, Computer and Communications Security, pp. 30–40. ACM (2011)
Böhme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 183–198. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_15
Boldo, S., Jourdan, J., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Symposium on Computer Arithmetic, pp. 107–115. IEEE (2013)
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). https://doi.org/10.1007/978-3-642-22110-1_37
Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny ARM hypervisor. In: Workshop on Trustworthy Embedded Devices, Co-located with CCS, pp. 3–12. ACM (2013)
Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 338–344. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_23
Fox, A.: L3: a specification language for instruction set architectures. http://www.cl.cam.ac.uk/~acjf3/l3/. Accessed 2015
Fox, A.C., Gordon, M.J., Myreen, M.O.: Specification and verification of ARM hardware and software. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 221–247. Springer, Boston (2010). https://doi.org/10.1007/978-1-4419-1539-9_8
Hasabnis, N., Sekar, R.: Lifting assembly to intermediate representation: a novel approach leveraging compilers. ACM SIGOPS Oper. Syst. Rev. 50(2), 311–324 (2016)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Operating systems principles, pp. 207–220. ACM (2009)
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. SIGPLAN Not. 49, 179–191 (2014). ACM
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 205–219. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_15
Arm Limited: ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (2013). http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0487a.h/index.html
Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Myreen, M.O., Curello, G.: Proof pearl: a verified bignum implementation in x86-64 machine code. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 66–81. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_5
Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, pp. 1–8. IEEE Press (2008)
Nethercote, N., Seward, J.: Valgrind: a program supervision framework. Electron. Notes Theor. Comput. Sci. 89(2), 44–66 (2003)
Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–482. ACM (2013)
Shacham, H.: The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86). In: Conference on Computer and Communications Security, pp. 552–561. ACM (2007)
Shoshitaishvili, Y., Wang, R., Salls, C., Stephens, N., Polino, M., Dutcher, A., Grosen, J., Feng, S., Hauser, C., Krügel, C., Vigna, G.: SOK: (state of) the art of war: offensive techniques in binary analysis. In: Symposium on Security and Privacy, pp. 138–157. IEEE (2016)
Song, D., et al.: BitBlaze: a new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 1–25. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89862-7_1
Vogels, F., Jacobs, B., Piessens, F.: A machine-checked soundness proof for an efficient verification condition generator. In: Symposium on Applied Computing, pp. 2517–2522. ACM (2010)
Acknowledgments
Partially funded by framework grant “IT 2010” from the Swedish Foundation for Strategic Research, and by the KTH CERCES Center for Resilient Critical Infrastructures, which is supported by the Swedish Civil Contingencies Agency.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Metere, R., Lindner, A., Guanciale, R. (2017). Sound Transpilation from Binary to Machine-Independent Code. In: Cavalheiro, S., Fiadeiro, J. (eds) Formal Methods: Foundations and Applications. SBMF 2017. Lecture Notes in Computer Science(), vol 10623. Springer, Cham. https://doi.org/10.1007/978-3-319-70848-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-70848-5_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-70847-8
Online ISBN: 978-3-319-70848-5
eBook Packages: Computer ScienceComputer Science (R0)