Advertisement

The Spirit of Ghost Code

  • Jean-Christophe Filliâtre
  • Léon Gondelman
  • Andrei Paskevich
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

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 Judgment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full conference paper text

References

  1. 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. 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. 3.
    Jacobs, B., Piessens, F.: The VeriFast program verifier. CW Reports CW520, Department of Computer Science, K.U. Leuven (August 2008)Google Scholar
  4. 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. 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. 6.
    Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115, 38–94 (1992)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Pierce, B.C.: Types and Programming Languages. MIT Press (2002)Google Scholar
  8. 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. 9.
    Reynolds, J.C.: The craft of programming. Prentice Hall International series in computer science. Prentice Hall (1981)Google Scholar
  10. 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. 11.
    Kleymann, T.: Hoare logic and auxiliary variables. Formal Asp. Comput. 11(5), 541–566 (1999)CrossRefzbMATHGoogle Scholar
  12. 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. 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. 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. 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. 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. 17.
    Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25(1), 117–158 (2003) ACMGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Jean-Christophe Filliâtre
    • 1
    • 2
  • Léon Gondelman
    • 1
  • Andrei Paskevich
    • 1
    • 2
  1. 1.Lab. de Recherche en InformatiqueUniv. Paris-Sud, CNRSOrsayFrance
  2. 2.INRIA Saclay – Île-de-FranceOrsayFrance

Personalised recommendations

Cite paper