Skip to main content
SpringerLink
Log in

On Trojan Horses of Thompson-Goerigk-Type, Their Generation, Intrusion, Detection and Prevention

  • Chapter
Concurrency, Compositionality, and Correctness

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5930))

  • 518 Accesses

Abstract

Trojan horses of Thompson-Goerigk-type are intended software errors very hidden in machine level compiler implementations although the latter have successfully passed Wirth’s strong compiler bootstrapping test and there have been done rigorous verification both of compiling specification and of high level compiler implementation. Thompson demonstrated these errors in 1984. This essay describes Goerigk’s contributions on how to generate, intrude, detect and prevent these most intricate errors which can even pass compiler certification test suites undetected. Target code inspection therefore is necessary. However, a full inspection usually is not feasible. Main research result described is how to slash down the amount of inspection necessary, while still getting a provably correct compiler. Project Verifix demonstrated this approach on a fully verified, realistic compiler for a realistic high level language.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bauer, F.L.: Einladung zur Mathematik. Deutsches Museum, München (1999)

    Google Scholar 

  2. BSI – Bundesamt für Sicherheit in der Informationstechnik. BSI-Zertifizierung. BSI 7119, Bonn (1994)

    Google Scholar 

  3. BSI – Bundesamt für Sicherheit in der Informationstechnik. OCOCAT-S Projektausschreibung (1996)

    Google Scholar 

  4. Chirica, L.M., Martin, D.F.: Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Languages and Systems 8(2), 185–214 (1986)

    Article  MATH  Google Scholar 

  5. Dold, A., von Henke, F., Goerigk, W.: A Completely Verified Realistic Bootstrap Compiler. Int. J. of Foundations of Computer Science 14(4), 659–680 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  6. Dold, A., von Henke, F.W., Vialard, V., Goerigk, W.: A Mechanically Verified Compiler Specification for a Realistic Compiler. Ulmer Informatik-Berichte Nr. 2002-03, Univ. Ulm, 67 pgs. (2002)

    Google Scholar 

  7. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  8. Dold, A.: Formal Software Development using Generic Development Steps. Logos-Verlag, Berlin, Dissertation, Univ. Ulm, 235 pgs. (2000)

    Google Scholar 

  9. Fagan, M.E.: Advances in software inspections. IEEE Transactions on Software Engineering, SE-12(7), 744–751 (1986)

    Google Scholar 

  10. Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., von Henke, F., Hoffmann, U., Langmaack, H., Pfeiffer, H., Ruess, H., Zimmermann, W.: Compiler Correctness and Implementation Verification: The Verifix Approach. In: Proc. Poster Sess. CC 1996–Internat. Conf. on Compiler Construction, ida, TR-Nr. R-96-12 (1996)

    Google Scholar 

  11. Glesner, S., Goos, G., Zimmermann, W.: Verifix: Konstruktion und Architektur verifizierender Übersetzer. Informationstechnik 46(5) (2004)

    Google Scholar 

  12. Goerigk, W., Gaul, T., Zimmermann, W.: Correct Programs without Proof? On Checker-Based Program Verification. In: Proceedings ATOOLS 1998 Workshop on Tool Support for System Specification, Development and Verification, Malente. Advances in Computing Science. Springer, Heidelberg (1998)

    Google Scholar 

  13. Goerigk, W., Hoffmann, U.: The Compiler Implementation Language ComLisp, Technical Report Verifix/CAU/1.7, CAU Kiel (June 1996)

    Google Scholar 

  14. Goerigk, W., Hoffmann, U.: The Compiling Specification from ComLisp to Executable Machine Code. Technical Report Nr. 9713, Institut für Informatik, CAU Kiel, 106 pgs. (December 1998)

    Google Scholar 

  15. Goerigk, W., Hoffmann, U.: Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 122–136. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Goerigk, W., Hoffmann, U.: Compiling ComLisp to Executable Machine Code: Compiler Construction. Technical Report Nr. 9812, Institut für Informatik, CAU Kiel, 170 pgs. (October 1998)

    Google Scholar 

  17. Goerigk, W., Hoffmann, U.: Proof Protocols for the Translation from ComLisp to Transputer-Code (1998), http://www.informatik.uni-kiel.de/~wg/-Verifix/proof-protocols/i.ps with i = l1, l2, l3, l4, s2, s3, s4, c3, c4, t4

  18. Goerigk, W.: On Trojan Horses in Compiler Implementations. In: Saglietti, F., Goerigk, W. (eds.) Proc. des Workshops Sicherheit und Zuverlässigkeit softwarebasierter Systeme, IsTec Report ISTec-A.367, Garching (August 1999) ISBN 3-00-004872-3

    Google Scholar 

  19. Goerigk, W.: Compiler Verification Revisited. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)

    Google Scholar 

  20. Goerigk, W.: Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof. In: Kaufmann, M., Moore, J.S. (eds.) Proceeding of the ACL2’ 2000 Workshop, Univ. of Texas, Austin, Texas, U.S.A. (October 2000)

    Google Scholar 

  21. Goerigk, W.: Trusted Program Execution. Habilitation thesis. Techn. Faculty, CAU zu Kiel, 161 pgs. (May 2000)

    Google Scholar 

  22. Goodenough, J.B., Gerhart, S.L.: Toward a theory of test data selection. IEEE Transactions on Software Engineering 1(2), 156–173 (1975)

    Article  MathSciNet  Google Scholar 

  23. Goerigk, W., Langmaack, H.: Will Informatics be able to Justify the Construction of Large Computer Based Systems? Inst. f. Informatik u. Prakt. Math., Univ. Kiel, Ber. 2015, 64 pgs. (2001); Appeared as Part I: Realistic Correct Systems Implementation, 28 pgs., and Part II : Trusted Compiler Implementation, 24 pgs. International Journal on Problems in Programming, Kiev, Ukraine (2003), http://www.informatik.uni-kiel.de/~wg/Berichte/-Kiev-Instituts-bericht-2001.ps.gz

  24. Goos, G., Zimmermann, W.: Verification of Compilers. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 201–231. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. Gaul, T., Zimmermann, W., Goerigk, G.: Construction of Verified Software Systems with Program-Checking: An Application to Compiler Back-ends. In: Pnueli, A., Traverso, P. (eds.) Proc. FloC 1999 International Workshop on Runtime Result Verification, Trento, Italy (1999)

    Google Scholar 

  26. Hoare, C.A.R.: The Verifying Compiler: A Grand Challenge for Computing Research. J. ACM 50(1), 63–69 (2003)

    Article  MATH  Google Scholar 

  27. Hoffmann, U.: Compiler Implementation Verification through Rigorous Syntactical Code Inspection. PhD thesis, Technische Fakultät der CAU zu Kiel, Inst. f. Informatik u. Prakt. Math., Ber. 9814, Kiel, 127 pgs. (1998)

    Google Scholar 

  28. Langmaack, H.: Softwareengineering zur Zertifizierung von Systemen: Spezifikations-, Implementierungs-, Übersetzerkorrektheit. Informationstechnik und Technische Informatik it+ti 39(3), 41–47 (1997)

    Google Scholar 

  29. Langmaack, H.: Contribution to Goodenough’s and Gerhart’s Theory of Software Testing and Verification. Relation between Strong Compiler Test and Compiler Implementation Verification. In: Freksa, C., Jantzen, M., Valk, R. (eds.) Foundations of Computer Science. LNCS, vol. 1337, pp. 321–335. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  30. Langmaack, H.: What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer? ENTCS 141(2), 5–32 (2005)

    Google Scholar 

  31. Langmaack, H., Wolf, A.: Reading and Printing in Constructing Fully Verified Compilers. Inst. Inf.Prakt. Math., Chr.-Albr.-Univ.Kiel, Ber. 0306, 113 pgs. (2003)

    Google Scholar 

  32. Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. Kluwer Academic Press, Dordrecht (1996)

    Google Scholar 

  33. Pofahl, E.: Methods Used for Inspecting Safety Relevant Software. In: Cullyer, W.J., Halang, W.A., Krämer, B.J. (eds.) High Integrity Programmable Electronic Systems. Dagstuhl, Sem.-Rep. 107, p. 13 (1995)

    Google Scholar 

  34. Steele Jr., G.L.: Common LISP. The Language. Digital Press, Badford (1984)

    MATH  Google Scholar 

  35. Thompson, K.: Reflections on Trusting Trust. Communications of the ACM 27(8), 761–763 (1984); Also in ACM Turing Award Lectures: The First Twenty Years 1965-1985. ACM Press, New York (1987), and in Computers Under Attack: Intruders, Worms, and Viruses. ACM Press, New York (1990)

    Google Scholar 

  36. Wirth, N.: Compilerbau, eine Einführung. B.G.Teubner, Stuttgart (1977)

    Google Scholar 

  37. ZSI-Zentralstelle für Sicherheit in der Informationstechnik. IT-Evaluationshandbuch. Bundesanzeiger Verlagsgesellschaft, Köln (1989)

    Google Scholar 

  38. ZSI-Zentralstelle für Sicherheit in der Informationstechnik. IT-Evaluationshandbuch. Bundesanzeiger Verlagsgesellschaft, Köln (1990)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik der, Christian-Albrechts-Universität zu Kiel, Olshausenstr. 40, D-24098, Kiel, Germany

    Hans Langmaack

Authors
  1. Hans Langmaack
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Bell Laboratories, 600 Mountain Ave., 07974, Murray Hill, NJ, USA

    Dennis Dams

  2. Computer Science Department, University of Bremen, P.O. Box 330440, 28334, Bremen, Germany

    Ulrich Hannemann

  3. Faculty of Mathematics and Natural Sciences, Department of Computer Science, University of Oslo, P.O. Box 1080, 0316, Blindern, Oslo, Norway

    Martin Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Langmaack, H. (2010). On Trojan Horses of Thompson-Goerigk-Type, Their Generation, Intrusion, Detection and Prevention. In: Dams, D., Hannemann, U., Steffen, M. (eds) Concurrency, Compositionality, and Correctness. Lecture Notes in Computer Science, vol 5930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11512-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11512-7_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11511-0

  • Online ISBN: 978-3-642-11512-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation