The Spirit of Ghost Code
Abstract
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.
Keywords
Type System Recursive Function Primitive Type Type Soundness Typing JudgmentReferences
- 1.Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)CrossRefGoogle Scholar
- 2.Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)CrossRefGoogle Scholar
- 3.Jacobs, B., Piessens, F.: The VeriFast program verifier. CW Reports CW520, Department of Computer Science, K.U. Leuven (August 2008)Google Scholar
- 4.Filliâtre, J.C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)Google Scholar
- 5.Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. SIGPLAN Not. 28(6), 237–247 (1993)CrossRefGoogle Scholar
- 6.Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115, 38–94 (1992)CrossRefMathSciNetGoogle Scholar
- 7.Pierce, B.C.: Types and Programming Languages. MIT Press (2002)Google Scholar
- 8.Jones, C.B., Roscoe, A., Wood, K.R.: Reflections on the Work of C.A.R. Hoare, 1st edn. Springer Publishing Company, Incorporated (2010)Google Scholar
- 9.Reynolds, J.C.: The craft of programming. Prentice Hall International series in computer science. Prentice Hall (1981)Google Scholar
- 10.Lucas, P.: Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory, Vienna (June 1968)Google Scholar
- 11.Kleymann, T.: Hoare logic and auxiliary variables. Formal Asp. Comput. 11(5), 541–566 (1999)CrossRefzbMATHGoogle Scholar
- 12.Zhang, Z., Feng, X., Fu, M., Shao, Z., Li, Y.: A structural approach to prophecy variables. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 61–71. Springer, Heidelberg (2012)CrossRefGoogle Scholar
- 13.Schmaltz, S.: Towards the Pervasive Formal Verification of Multi-Core Operating Systems and Hypervisors Implemented in C. PhD thesis, Saarland University, Saarbrcken (2013)Google Scholar
- 14.Leino, K.R.M., Moskal, M.: Co-induction simply. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 382–398. Springer, Heidelberg (2014)CrossRefGoogle Scholar
- 15.Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM 20(2), 504–513 (1977)CrossRefzbMATHGoogle Scholar
- 16.Pottier, F., Conchon, S.: Information flow inference for free. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montréal, Canada, pp. 46–57 (September 2000)Google Scholar
- 17.Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25(1), 117–158 (2003) ACMGoogle Scholar