Abstract
Automatically generating proofs of safety properties for software is important as software becomes safety-critical, e.g., in medical devices and automobiles. While current techniques can automatically prove safety properties for machine code, they either: (i) do not support user-mode programs in an operating system, (ii) do not support realistic program features such as system calls, or (iii) have been demonstrated only on programs of limited sizes. We present AUSPICE-R, which automates safety-property proof generation for user-mode ARM machine code containing system calls, and greatly improves the scalability of automated safety-property proof generation. AUSPICE-R uses an axiomatic approach to model system calls, and leverages idioms in compiled code to optimize its proof automation. We demonstrate AUSPICE-R on (i) simple working versions of common text utilities that perform I/O, and (ii) embedded programs for the Raspberry Pi single-board-computer containing hardware I/O. AUSPICE-R automatically proves safety up to 12\(\times \) faster, and supports programs 3\(\times \) larger, than prior techniques.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Application Binary Interface for the ARM Architecture. http://bit.ly/22OaMai
Linux Programmer’s Manual: Syscalls. http://bit.ly/1VChJMY
The ARM-THUMB Procedure Call Standard (2000). http://bit.ly/1NbOQhT
As Gadgets Shrink, ARM Still Reigns As Processor King, September 2013. http://onforb.es/19LIzgd
ARM Architecture Reference Manual: ARMv7-A and ARMv7-R edition (2014)
Abadi, M., Budiu, M., Erlingsson, U., Ligatti, J.: Control-flow Integrity. In: ACM CCS (2005)
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_20
Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19718-5_1
Blackham, B., Heiser, G.: Sequel: a framework for model checking binaries. In: IEEE RTAS (2013)
Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI (2011)
Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, October 2009
Guthaus, M., et al.: MiBench: a free, commercially representative embedded benchmark suite. In: IEEE WWC Workshop (2001)
Jia, N.: Detecting human falls with a 3-axis digital accelerometer (2009). http://bit.ly/23fXhFE
Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015)
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Miller, C., Valasek, C.: Remote exploitation of an unaltered passenger vehicle. http://bit.ly/1Xk71rn
Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272–286. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75698-9_18
Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568–582. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_44
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS (2002)
Goel, S., et al.: Simulation and formal verification of x86 machine-code programs that make system calls. In: FMCAD (2014)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71067-7_6
Tan, J., Tay, H., Drolia, U., Gandhi, R., Narasimhan, P.: PCFIRE: towards provable preventative control-flow integrity enforcement for realistic embedded software. In: EMSOFT (2016)
Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: AUSPICE: \(\underline{\rm {Au}}\)tomatic \(\underline{\rm {S}}\)afety \(\underline{\rm {P}}\)roperty verif\(\underline{\rm {ic}}\)ation for unmodified \(\underline{\rm {E}}\)xecutables. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 202–222. Springer, Heidelberg (2016). doi:10.1007/978-3-319-29613-5_12
Wahbe, R., Lucco, S., Anderson, T., Graham, S.: Efficient software-based fault isolation. In: SOSP (1993)
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI (2011)
Zhao, L., Li, G., Sutter, B.D., Regehr, J.: ARMor: fully verified software fault isolation. In: EMSOFT (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P. (2016). AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)